On Fri, 5 Oct 2012, Christian Sternagel wrote:
- Now that the output panel is based on the same technology as the main
buffer, would it be feasible to include also the output panel when a
search on "all buffers" is done.
I am not as ambitious at the moment. A plain Firefox-style search box
like a regular jEdit buffer would be the next step, but I don't know yet
how it needs to be wired up.
Rich_Text_Area shares the larger part of the display engine and buffer
content management with regular jEdit buffers, but the latter is a bit
more than that. My approach imitates existing jEdit plugins like Minimap
or FoldViewer, and it shares few similar limitations with them.
Concerning the collection of official jEdit buffers and the nodes in the
formal document model of PIDE, there are some further conceptual issues
still waiting. For example, when you hypersearch over the all buffers,
you get an order according to file names. It would be more practical to
get a topological order according to the logical structure, especially
when doing systematic replacements while continous checking happens.
So instead of injecting output panels into the jEdit buffer collection, it
might be better to hijack jEdit's hypersearch and let it operate on the
formal document model instead, with some nodes having also an actual jEdit
buffer by accident. This would also avoid the problem of "swamping" the
jEdit buffer space with lots of imported theory files when opening some
file in a large application or library.
- An old story (but maybe now it's easier to realize?): It would also be
great if copy/paste would work the same as for the main buffer (e.g., on
linuxen: select with mouse to copy and press middle mouse button to
paste); currently only C+c/C+v works
That is just a cheap imitation of the Lobo keyhandler, while using the
proper jEdit clipboard now (with its additional history and registers).
See
http://isabelle.in.tum.de/repos/isabelle/annotate/21f77309d93a/src/Tools/jEdit/src/pretty_text_area.scala#l138
Anything beyond that requires more understanding how jEdit maps key/mouse
events to its actions that operate on a buffer/textarea. There is rather
complex infrastructure for that in jEdit.
BTW, the Unix/X11-style middle-mouse-button copy/paste is a special
mechanism of jEdit implemented on top of regular Java/Swing concepts.
More basic Java applications don't have that, and users of Windows / Mac
OS probably won't know that it could be convenient for them.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
