[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PATCH] Add user content APIs for WebKit Xwidgets
From: |
Po Lu |
Subject: |
Re: [PATCH] Add user content APIs for WebKit Xwidgets |
Date: |
Mon, 24 Oct 2022 08:30:29 +0800 |
User-agent: |
Gnus/5.13 (Gnus v5.13) |
Qiantan Hong <qthong@stanford.edu> writes:
> Applying to all related Xwidgets sound like a good idea. I think we should
> formalize the "group of related Xwidgets" as some kind of object? Maybe
> a record type implemented in Lisp, or a pseudo vector (which I don't know
> much about how to implement). An alternative is to expose content manager
> as a pseudovector, which will in fact have 1-to-1 correspondence with "related
> group", but I like related group more because it feels like a nicer
> abstraction.
I don't think that is necessary. There should at most be a function
that returns a list of all related xwidgets.
Pseudovector types are a limited resource. There can only be 64 at any
given time, so it would be a good idea not to waste them on such
trivialities.
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, (continued)
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Qiantan Hong, 2022/10/16
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Po Lu, 2022/10/16
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Qiantan Hong, 2022/10/16
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Po Lu, 2022/10/16
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Po Lu, 2022/10/16
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Qiantan Hong, 2022/10/23
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Po Lu, 2022/10/23
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Qiantan Hong, 2022/10/23
- Re: [PATCH] Add user content APIs for WebKit Xwidgets,
Po Lu <=
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Qiantan Hong, 2022/10/24
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Po Lu, 2022/10/24
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Qiantan Hong, 2022/10/24
- Re: [PATCH] Add user content APIs for WebKit Xwidgets, Po Lu, 2022/10/24
- Re: [PATCH] Add user extension APIs for WebKit Xwidgets, Richard Stallman, 2022/10/16
- Re: [PATCH] Add user extension APIs for WebKit Xwidgets, Alan Mackenzie, 2022/10/16
- Re: [PATCH] Add user extension APIs for WebKit Xwidgets, Richard Stallman, 2022/10/18
- Re: [PATCH] Add user extension APIs for WebKit Xwidgets, Eli Zaretskii, 2022/10/17
- Re: [PATCH] Add user extension APIs for WebKit Xwidgets, Jean Louis, 2022/10/17
- Re: [PATCH] Add user extension APIs for WebKit Xwidgets, Richard Stallman, 2022/10/19