builtin sub/superscript styles for jedit-4.3.2;
authorwenzelm
Tue Jun 14 17:24:23 2011 +0200 (2011-06-14 ago)
changeset 433907ee98a3802af
parent 43389 328dcc5cc43f
child 43391 986860aa51ac
child 43402 b35ff420d720
builtin sub/superscript styles for jedit-4.3.2;
src/Tools/jEdit/patches/scriptstyles
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_markup.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/patches/scriptstyles	Tue Jun 14 17:24:23 2011 +0200
     1.3 @@ -0,0 +1,30 @@
     1.4 +diff -r jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
     1.5 +60c60
     1.6 +< 		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
     1.7 +---
     1.8 +> 		return (token == Token.END) ? "END" : TOKEN_TYPES[(token >= ID_COUNT) ? 0 : token];
     1.9 +diff -r jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    1.10 +196a197,207
    1.11 +> 	 * Style with sub/superscript font attribute.
    1.12 +> 	 */
    1.13 +> 	public static SyntaxStyle scriptStyle(String family, int size, int script)
    1.14 +> 	{
    1.15 +> 		Font font = new Font(family, 0, size);
    1.16 +> 		java.util.Map attributes = new java.util.HashMap();
    1.17 +> 		attributes.put(java.awt.font.TextAttribute.SUPERSCRIPT, new Integer(script));
    1.18 +> 		return new SyntaxStyle(Color.black, null, font.deriveFont(attributes));
    1.19 +> 	}
    1.20 +> 	
    1.21 +> 	/**
    1.22 +206c217
    1.23 +< 		SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT];
    1.24 +---
    1.25 +> 		SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT + 2];
    1.26 +209c220
    1.27 +< 		for(int i = 1; i < styles.length; i++)
    1.28 +---
    1.29 +> 		for(int i = 1; i < Token.ID_COUNT; i++)
    1.30 +225a237,239
    1.31 +> 		styles[Token.ID_COUNT] = scriptStyle(family, size, -1);
    1.32 +> 		styles[Token.ID_COUNT + 1] = scriptStyle(family, size, 1);
    1.33 +> 
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Jun 14 15:58:01 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Jun 14 17:24:23 2011 +0200
     2.3 @@ -25,36 +25,6 @@
     2.4  {
     2.5    object Token_Markup
     2.6    {
     2.7 -    /* extended token styles */
     2.8 -
     2.9 -    private val plain_range: Int = Token.ID_COUNT
    2.10 -    private val full_range: Int = 3 * plain_range
    2.11 -    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    2.12 -
    2.13 -    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    2.14 -    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    2.15 -
    2.16 -    private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
    2.17 -    {
    2.18 -      import scala.collection.JavaConversions._
    2.19 -      val script_font =
    2.20 -        style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
    2.21 -      new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
    2.22 -    }
    2.23 -
    2.24 -    def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    2.25 -    {
    2.26 -      val new_styles = new Array[SyntaxStyle](full_range)
    2.27 -      for (i <- 0 until plain_range) {
    2.28 -        val style = styles(i)
    2.29 -        new_styles(i) = style
    2.30 -        new_styles(subscript(i.toByte)) = script_style(style, -1)
    2.31 -        new_styles(superscript(i.toByte)) = script_style(style, 1)
    2.32 -      }
    2.33 -      new_styles
    2.34 -    }
    2.35 -
    2.36 -
    2.37      /* line context */
    2.38  
    2.39      private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
    2.40 @@ -197,12 +167,6 @@
    2.41          val start = buffer.getLineStartOffset(line)
    2.42          val stop = start + line_segment.count
    2.43  
    2.44 -        /* FIXME
    2.45 -        for (text_area <- Isabelle.jedit_text_areas(buffer)
    2.46 -              if Document_View(text_area).isDefined)
    2.47 -          Document_View(text_area).get.set_styles()
    2.48 -        */
    2.49 -
    2.50          def handle_token(style: Byte, offset: Text.Offset, length: Int) =
    2.51            handler.handleToken(line_segment, style, offset, length, context)
    2.52  
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 15:58:01 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 17:24:23 2011 +0200
     3.3 @@ -69,24 +69,6 @@
     3.4  
     3.5    /** token handling **/
     3.6  
     3.7 -  /* extended token styles */
     3.8 -
     3.9 -  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
    3.10 -
    3.11 -  def extend_styles()
    3.12 -  {
    3.13 -    Swing_Thread.require()
    3.14 -    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
    3.15 -  }
    3.16 -  extend_styles()
    3.17 -
    3.18 -  def set_styles()
    3.19 -  {
    3.20 -    Swing_Thread.require()
    3.21 -    text_area.getPainter.setStyles(styles)
    3.22 -  }
    3.23 -
    3.24 -
    3.25    /* visible line ranges */
    3.26  
    3.27    // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
     4.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Tue Jun 14 15:58:01 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Tue Jun 14 17:24:23 2011 +0200
     4.3 @@ -185,6 +185,8 @@
     4.4    private val token_style: Map[String, Byte] =
     4.5    {
     4.6      import Token._
     4.7 +    val SUBSCRIPT: Byte = ID_COUNT
     4.8 +    val SUPERSCRIPT: Byte = ID_COUNT + 1
     4.9      Map[String, Byte](
    4.10        // embedded source text
    4.11        Markup.ML_SOURCE -> COMMENT3,
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Jun 14 15:58:01 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Jun 14 17:24:23 2011 +0200
     5.3 @@ -373,11 +373,7 @@
     5.4          }
     5.5  
     5.6        case msg: PropertiesChanged =>
     5.7 -        Swing_Thread.now {
     5.8 -          Isabelle.setup_tooltips()
     5.9 -          for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
    5.10 -            Document_View(text_area).get.extend_styles()
    5.11 -        }
    5.12 +        Swing_Thread.now { Isabelle.setup_tooltips() }
    5.13          Isabelle.session.global_settings.event(Session.Global_Settings)
    5.14  
    5.15        case _ =>