# HG changeset patch
# User wenzelm
# Date 1308065063 -7200
# Node ID 7ee98a3802af513cc7a01fabe6878949672c54bd
# Parent  328dcc5cc43f57e2ab5cd2594a1b3473f03757a6
builtin sub/superscript styles for jedit-4.3.2;

diff -r 328dcc5cc43f -r 7ee98a3802af src/Tools/jEdit/patches/scriptstyles
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/scriptstyles	Tue Jun 14 17:24:23 2011 +0200
@@ -0,0 +1,30 @@
+diff -r jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
+60c60
+< 		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
+---
+> 		return (token == Token.END) ? "END" : TOKEN_TYPES[(token >= ID_COUNT) ? 0 : token];
+diff -r jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+196a197,207
+> 	 * Style with sub/superscript font attribute.
+> 	 */
+> 	public static SyntaxStyle scriptStyle(String family, int size, int script)
+> 	{
+> 		Font font = new Font(family, 0, size);
+> 		java.util.Map attributes = new java.util.HashMap();
+> 		attributes.put(java.awt.font.TextAttribute.SUPERSCRIPT, new Integer(script));
+> 		return new SyntaxStyle(Color.black, null, font.deriveFont(attributes));
+> 	}
+> 	
+> 	/**
+206c217
+< 		SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT];
+---
+> 		SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT + 2];
+209c220
+< 		for(int i = 1; i < styles.length; i++)
+---
+> 		for(int i = 1; i < Token.ID_COUNT; i++)
+225a237,239
+> 		styles[Token.ID_COUNT] = scriptStyle(family, size, -1);
+> 		styles[Token.ID_COUNT + 1] = scriptStyle(family, size, 1);
+> 
diff -r 328dcc5cc43f -r 7ee98a3802af src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Jun 14 15:58:01 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Jun 14 17:24:23 2011 +0200
@@ -25,36 +25,6 @@
 {
   object Token_Markup
   {
-    /* extended token styles */
-
-    private val plain_range: Int = Token.ID_COUNT
-    private val full_range: Int = 3 * plain_range
-    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
-
-    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
-    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
-
-    private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
-    {
-      import scala.collection.JavaConversions._
-      val script_font =
-        style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
-      new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
-    }
-
-    def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
-    {
-      val new_styles = new Array[SyntaxStyle](full_range)
-      for (i <- 0 until plain_range) {
-        val style = styles(i)
-        new_styles(i) = style
-        new_styles(subscript(i.toByte)) = script_style(style, -1)
-        new_styles(superscript(i.toByte)) = script_style(style, 1)
-      }
-      new_styles
-    }
-
-
     /* line context */
 
     private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
@@ -197,12 +167,6 @@
         val start = buffer.getLineStartOffset(line)
         val stop = start + line_segment.count
 
-        /* FIXME
-        for (text_area <- Isabelle.jedit_text_areas(buffer)
-              if Document_View(text_area).isDefined)
-          Document_View(text_area).get.set_styles()
-        */
-
         def handle_token(style: Byte, offset: Text.Offset, length: Int) =
           handler.handleToken(line_segment, style, offset, length, context)
 
diff -r 328dcc5cc43f -r 7ee98a3802af src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 15:58:01 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 17:24:23 2011 +0200
@@ -69,24 +69,6 @@
 
   /** token handling **/
 
-  /* extended token styles */
-
-  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
-
-  def extend_styles()
-  {
-    Swing_Thread.require()
-    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
-  }
-  extend_styles()
-
-  def set_styles()
-  {
-    Swing_Thread.require()
-    text_area.getPainter.setStyles(styles)
-  }
-
-
   /* visible line ranges */
 
   // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
diff -r 328dcc5cc43f -r 7ee98a3802af src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Tue Jun 14 15:58:01 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Tue Jun 14 17:24:23 2011 +0200
@@ -185,6 +185,8 @@
   private val token_style: Map[String, Byte] =
   {
     import Token._
+    val SUBSCRIPT: Byte = ID_COUNT
+    val SUPERSCRIPT: Byte = ID_COUNT + 1
     Map[String, Byte](
       // embedded source text
       Markup.ML_SOURCE -> COMMENT3,
diff -r 328dcc5cc43f -r 7ee98a3802af src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Jun 14 15:58:01 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Jun 14 17:24:23 2011 +0200
@@ -373,11 +373,7 @@
         }
 
       case msg: PropertiesChanged =>
-        Swing_Thread.now {
-          Isabelle.setup_tooltips()
-          for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
-            Document_View(text_area).get.extend_styles()
-        }
+        Swing_Thread.now { Isabelle.setup_tooltips() }
         Isabelle.session.global_settings.event(Session.Global_Settings)
 
       case _ =>