[prev in list] [next in list] [prev in thread] [next in thread]
List: jedit-devel
Subject: [ jEdit-devel ] Advanced TokenMarker and TextAreaPainter
From: Makarius <makarius () sketis ! net>
Date: 2011-06-22 16:29:53
Message-ID: alpine.LNX.1.10.1106221711480.26024 () atbroy100 ! informatik ! tu-muenchen ! de
[Download RAW message or body]
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
------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev
--
-----------------------------------------------
jEdit Developers' List
jEdit-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/jedit-devel
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic