Menu
▾
▴
[ jEdit-devel ] [ jedit-Patches-3512122 ] Extended font styles
|
From: SourceForge.net <no...@so...> - 2012-03-29 13:18:58
|
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: 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: 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 |