[ jEdit-devel ] Advanced TokenMarker and TextAreaPainter

[Makarius <mak...@sk...>]

Dear jEdit enthusiasts,

this is a continuation of the thread 
http://marc.info/?l=jedit-devel&m=128268660001354&w=2 from Aug/Sep 2010 
about "Proper use of TokenMarker and LineContext".  The present mail is 
merely an informative report.  Further questions and proposals for the 
official jEdit code base will come a bit later :-)


My project is still the same: producing a sophisticated "Prover IDE" with 
jEdit is main editor component, while the plugins and auxiliary modules 
are implemented in Scala/JVM.  The prover in the background provides rich 
semantic information that accumulates as a large markup tree within the 
JVM.  The tree is used as "model" behind the jEdit buffer and textview, to 
draw a variety of GUI metaphors to illustrate the formal content to the 
user, who is editing formal theories interactively.

Last fall I have managed to integrate everything into a version that was 
sufficiently usable to impress users in two short university courses given 
to doctoral students and researchers of formal logic.  (These people only 
knew vi and Emacs before, and where thinking that Java was evil and 
Eclipse sucks.  I do agree with the Eclipse part, though :-)

See also http://www.lri.fr/~wenzel/Isabelle2011-Paris/ to get an idea, 
especially the screenshot from Nov-2010 
http://www.lri.fr/~wenzel/Isabelle2011-Paris/Seq.png


In the last few weeks I've spent considerable time to learn more about 
details of TokenMarker, TokenHandler, Chunk, TextPainter (as of 
jedit-4.3.2).  Since 4.4.1 is now released, I've gone through the critical 
parts again and noticed that there is actually ongoing activity in some of 
these spots.  So its high time to give some feedback of what I have done 
and learned about these internals so far.

The updated screenshot http://www.lri.fr/~wenzel/test/Seq.png refers to 
http://isabelle.in.tum.de/repos/isabelle/rev/bf7400573617 from today, it 
already uses jedit-4.4.1.

Comparing this with the old screenshot above, there is now more 
information painted over and under the text, without the heavy overloading 
of the TokenMarker process that I had experienced before (because Chunks 
are reproduced from the first changed line, and a global 
buffer.propertiesChanged is deadly to the cache).  I have now improved my
token marker and text painter components as follows 
http://isabelle.in.tum.de/repos/isabelle/file/bf7400573617/src/Tools/jEdit/src/token_markup.scala 
http://isabelle.in.tum.de/repos/isabelle/file/bf7400573617/src/Tools/jEdit/src/text_area_painter.scala

* The new TokenMarker is "static".  It respects the jEdit policy about 
chunk caching and linear reparsing, which means it only depends on the 
actual line text and context.  (The LineContext records state of open 
quotes or comment brackets.  Its "equals" method is defined to ensure that 
the "interning" within the jEdit cache does not lead to memory leaks.)

Inspecting the jEdit sources more closely, I've understood that the key 
purpose of Chunk is to determine font metrics, which are then used in 
TextArea.xyToOffset and offsetToXY all the time.  While the metrics 
(notably font style) have to be static, without consulting the external 
process and its dynamic change of information, anything else can be 
changed later when painting happens (text color etc.).

* Text painting is now much more ambitious than before.  I have replaced 
the main TextAreaPainter.PainText by my own version, in order to be able 
to take the color information from the current version of my background 
model.  The practical result of that can be seen in the screenshots: the 
LITERAL tokens of quoted strings like "conc Empty ys = ys" are now painted 
with blue and black sub-chunks.  (The color scheme indicates the logical 
scope of formal entities: black, blue, brown, green etc.)

I've found the screen-oriented invocation model via 
TextAreaExtension.paintScreenLineRange very convenient.  It avoids the 
bottle neck of line-oriented token marking.  By passing the full 
Graphics2D context with full region information, it is also very flexibile 
and allows to draw whatever can be imagined.

For example, I have now used drawRect with alpha channel to indicate 
"sub-expressions" within the text.  E.g. see the grey markup of "'a seq => 
'a seq => 'a seq" as logical "type" in the screenshot.  Painting with 
transparency preserves the detailed coloring of the text nicely.


I have also devised some tricks to paint sub/superscripts and bold face 
into the text, which is important for mathematical formulas. Here is a 
simple example: http://www.lri.fr/~wenzel/test/styles.png

This works as follows:

   o Certain unicode symbols within the text buffer are interpreted as
     control characters for chainging font styles.

   o Control characters are painted with "hidden" style, which is a 1 point
     font of full height (using affine font transformations of
     java.awt.Font).

   o The controlled text is painted with derived jEdit token styles,
     that are cooked from the normal user-specified jEdit styles
     (produced by SyntaxUtilities.loadStyles).

   o The standard "caret" is masked by a suitable Clip on the gfx context.
     Instead I paint the text in reverse colors using Java text attributes.
     Thus the change of metrics for sub/superscripts is observed (see
     screenshot), and the "hidden" part is draw as a vertical line
     segment of 1 pixel width, so users can understand the meaning of
     invisible control symbols better.

When such styled text is pasted into other swing components, say the jEdit 
search box, it is displayed as literal arrow symbols with plain text like 
this: "A⇣1 + B⇡2 = ❙C.


Overall, I am impressed how far jEdit could be stretched with only very 
small "patches" of the official sources: 
http://isabelle.in.tum.de/repos/isabelle/file/bf7400573617/src/Tools/jEdit/patches

This is where I hope to get some feedback from jEdit experts on this list.

I will also produce some more topical (shorter) mails about certain fine 
points to be discussed.


 	Makarius