[isabelle-dev] Isabelle/jEdit output panel

[Makarius]

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