Menu
▾
▴
[ jEdit-devel ] [ jedit-Patches-3512122 ] Extended font styles
|
From: SourceForge.net <no...@so...> - 2012-03-29 15:44:46
|
Patches item #3512122, was opened at 2012-03-27 15:39 Message generated for change (Comment added) made by jarekczek You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=300588&aid=3512122&group_id=588 Please note that this message will contain a full copy of the comment thread, including the initial issue submission, for this request, not just the latest update. Category: texteditor Group: None >Status: Pending >Resolution: Rejected Priority: 5 Private: No Submitted By: Makarius (makarius) Assigned to: Nobody/Anonymous (nobody) Summary: Extended font styles Initial Comment: The idea is to make a bit more out of the jEdit model for font styles, in a minimally intrusive fashion. Advanced plugins can install a StyleExtender (at most one for the running jEdit process!); whenever jEdit reconstructs the style array for mapping its Byte indices to actual font styles, it is silently extended according to the given method for that. For example, adding bold, super/sub-script variants for the user-specified styles. The change has been tested for about 12 months in jEdit 4.4.1 .. 4.5.1 as used for the Isabelle/jEdit plugin, see also http://isabelle.in.tum.de/repos/isabelle/file/d317a71f24d5/src/Tools/jEdit/src/token_markup.scala#l85 Beyond some fine-tuning of such received jEdit functionality, one might consider more ambitious changes to overhaul the style model, especially to overcome the 7bit address range. ---------------------------------------------------------------------- >Comment By: Jarek Czekalski (jarekczek) Date: 2012-03-29 08:44 Message: Actually I have more doubts about this patch. I posted today on jedit-devel, so that we could continue on mailing list. In general there is no feature request to describe what is really needed before starting the implementation. And the greatest concern: if I write another plugin which gives another style extensions for another mode, I couldn't use it because only one style extender is possible. This imo disqualifies this patch, because it is addressed at a single need and not for the general capability extension. Anyway as I said in the email - the idea seems reasonable. Here is the link to the discussion which I hope to continue on mailing list: http://jedit.9.n6.nabble.com/jEdit-devel-jedit-Patches-3512122-Extended-font-styles-tp4668159p4668159.html ---------------------------------------------------------------------- Comment By: Makarius (makarius) Date: 2012-03-29 08:28 Message: The _styleExtender is my was to indicate a private variable; I am not a Java expert myself, I have seen it occasionally in some other code. ---------------------------------------------------------------------- Comment By: Makarius (makarius) Date: 2012-03-29 08:25 Message: styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size)); this is indeed somehow coming out of the blue in this patch; for some reason the 0 entry was left unitialized, but gets assigned to the above before being used for rendering. I've been using it practically for a long time without encountering any surprises. I can investigate this in further if you want. ---------------------------------------------------------------------- Comment By: Makarius (makarius) Date: 2012-03-29 06:19 Message: (Meta comment: I am assuming that this is to be discussed at the tracker, not the mailing list.) Styles in jEdit work via a certain interplay of the following modules: org/gjt/sp/jedit/syntax/Token.java org/gjt/sp/jedit/syntax/TokenMarker.java org/gjt/sp/jedit/syntax/TokenHandler.java org/gjt/sp/jedit/syntax/Chunk.java When a new edit mode is initialzed, a TokenMarker is created that knows how to chop the text into Tokens/Chunks, with an associated "id" (7-bit integer). The latter is turned into an actual font style by using the id as index for the TextAreaPainter.styles array (accessed via method TextAreaPainter.getStyles). The style array is produced in certain situations by jEdit when properties change, according to the user properties given via the "Syntax Highlighting" dialog. This defines the slots 0..18 in the array (Token.ID_COUNT = 19). My StyleExtender allows to augment this programatically by further styles, say to produce bold, sub-, super-script variants from what the user has given, although the 7 bit address range of style ids limits this a bit. A mode-specific TokenMarker is required to produce such extended style index bytes in practice -- the standard ones by jEdit will always stay in the original interval. The occasional index restriction (token % Token.ID_COUNT) in the patch ensures that extended indexes are truncated in the sense of the original table in org/gjt/sp/jedit/syntax/Token.java. For example, a subscript Token.DIGIT produced by my token marker will be reduced to a normal Token.DIGIT when the StyleEditor looks at it. The user then edits that style, causing a propertiesChanged event, and the StyleExtender recovers the subscript version of it -- so it all fits together nicely. ---------------------------------------------------------------------- Comment By: Jarek Czekalski (jarekczek) Date: 2012-03-29 06:18 Message: Let me also add the rest of my remarks: 1. This line seems unrelated to the discussed functionality: + styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size)); 2. class members (_styleExtender) should be all in one place, commented with javadoc 3. StyleExtender is a public class designed to be used by plugins in a particular way. This should also be commented with javadoc with explanations on how to use it. 4. When jedit accepts external data and treats it as internal (styles array) it should perform a check for validity. The array should be non-null and have a particular size. If an array is invalid it should be rejected and the reason logged. 5. What is the meaning of _ in front of styleExtender? Looks like a convention I'm not familiar with. Should we add its description to coding style wiki? ---------------------------------------------------------------------- Comment By: Jarek Czekalski (jarekczek) Date: 2012-03-29 00:18 Message: How many styles will StyleExtender return? The question is connected with a change I don't understand: + return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT]; I am a style newbie. If this question is dumb you may ignore it and wait for someone else :) I just try to help after the mess I caused. ---------------------------------------------------------------------- Comment By: Jarek Czekalski (jarekczek) Date: 2012-03-28 23:39 Message: I'm sorry. Overlooked the other files in the patch. It applies cleanly on 450 for example. ---------------------------------------------------------------------- Comment By: Jarek Czekalski (jarekczek) Date: 2012-03-27 23:44 Message: This patch is not for our trunk StyleEditor.java file. What is it for? http://jedit.svn.sourceforge.net/viewvc/jedit/jEdit/trunk/org/gjt/sp/jedit/gui/StyleEditor.java?revision=17391&view=markup We don't have the following line in it: private SyntaxUtilities(){} ---------------------------------------------------------------------- You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=300588&aid=3512122&group_id=588 |
