Menu
▾
▴
[ jEdit-devel ] [ jedit-Patches-3512122 ] Extended font styles
|
From: SourceForge.net <no...@so...> - 2012-03-29 13:19:05
|
Patches item #3512122, was opened at 2012-03-27 15:39 Message generated for change (Comment added) made by makarius 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: Open Resolution: None 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: 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 |
