# HG changeset patch
# User wenzelm
# Date 1275406613 -7200
# Node ID 8e1e27a3b3613df4ebed6daec5b8f3f65b314e03
# Parent  b3ff14122645ece1c195c7cd587896359fc6cf79# Parent  04d2521e79b0d44c3790b360636b9a1745e0c8e7
merged

diff -r b3ff14122645 -r 8e1e27a3b361 Admin/isatest/settings/cygwin-poly-e
--- a/Admin/isatest/settings/cygwin-poly-e	Tue Jun 01 15:59:01 2010 +0200
+++ b/Admin/isatest/settings/cygwin-poly-e	Tue Jun 01 17:36:53 2010 +0200
@@ -1,6 +1,6 @@
 # -*- shell-script -*- :mode=shellscript:
 
-  POLYML_HOME="/home/isatest/homebroy/home/polyml/polyml-5.3.0"
+  POLYML_HOME="/home/isatest/polyml-5.3.0"
   ML_SYSTEM="polyml-5.3.0"
   ML_PLATFORM="x86-cygwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
diff -r b3ff14122645 -r 8e1e27a3b361 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Tue Jun 01 15:59:01 2010 +0200
+++ b/src/Pure/General/secure.ML	Tue Jun 01 17:36:53 2010 +0200
@@ -13,7 +13,8 @@
   val use_text: use_context -> int * string -> bool -> string -> unit
   val use_file: use_context -> bool -> string -> unit
   val toplevel_pp: string list -> string -> unit
-  val open_unsynchronized: unit -> unit
+  val Isar_setup: unit -> unit
+  val PG_setup: unit -> unit
   val commit: unit -> unit
   val bash_output: string -> string * int
   val bash: string -> int
@@ -54,7 +55,9 @@
 val use_global = raw_use_text ML_Parse.global_context (0, "") false;
 
 fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
-fun open_unsynchronized () = use_global "open Unsynchronized";
+
+fun Isar_setup () = use_global "open Unsynchronized;";
+fun PG_setup () = use_global "structure ThyLoad = Thy_Load;";
 
 
 (* shell commands *)
diff -r b3ff14122645 -r 8e1e27a3b361 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jun 01 15:59:01 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jun 01 17:36:53 2010 +0200
@@ -245,6 +245,7 @@
           Unsynchronized.set initialized);
         sync_thy_loader ();
        Unsynchronized.change print_mode (update (op =) proof_generalN);
+       Secure.PG_setup ();
        Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
 
 end;
diff -r b3ff14122645 -r 8e1e27a3b361 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jun 01 15:59:01 2010 +0200
+++ b/src/Pure/ROOT.ML	Tue Jun 01 17:36:53 2010 +0200
@@ -305,11 +305,9 @@
 structure PrintMode = Print_Mode;
 structure SpecParse = Parse_Spec;
 structure ThyInfo = Thy_Info;
+structure ThyLoad = Thy_Load;
 structure ThyOutput = Thy_Output;
 structure TypeInfer = Type_Infer;
 
 end;
 
-structure ThyLoad = Thy_Load;  (*Proof General legacy*)
-
-
diff -r b3ff14122645 -r 8e1e27a3b361 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Tue Jun 01 15:59:01 2010 +0200
+++ b/src/Pure/System/isar.ML	Tue Jun 01 17:36:53 2010 +0200
@@ -138,7 +138,7 @@
 
 fun toplevel_loop {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
-  Secure.open_unsynchronized ();
+  Secure.Isar_setup ();
   if do_init then init () else ();
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar sync)) ());
diff -r b3ff14122645 -r 8e1e27a3b361 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Jun 01 15:59:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Jun 01 17:36:53 2010 +0200
@@ -19,6 +19,7 @@
 
 import org.gjt.sp.jedit.gui.RolloverButton
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.syntax.SyntaxStyle
 
 
 object Document_View
@@ -78,6 +79,24 @@
   private val session = model.session
 
 
+  /* extended token styles */
+
+  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
+
+  def extend_styles()
+  {
+    Swing_Thread.assert()
+    styles = Isabelle_Token_Marker.extend_styles(text_area.getPainter.getStyles)
+  }
+  extend_styles()
+
+  def set_styles()
+  {
+    Swing_Thread.assert()
+    text_area.getPainter.setStyles(styles)
+  }
+
+
   /* commands_changed_actor */
 
   private val commands_changed_actor = actor {
diff -r b3ff14122645 -r 8e1e27a3b361 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Tue Jun 01 15:59:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Tue Jun 01 17:36:53 2010 +0200
@@ -11,13 +11,46 @@
 import isabelle._
 
 import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, ParserRuleSet}
+import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, ParserRuleSet, SyntaxStyle}
+import org.gjt.sp.jedit.textarea.TextArea
 
+import java.awt.Font
+import java.awt.font.TextAttribute
 import javax.swing.text.Segment;
 
 
 object Isabelle_Token_Marker
 {
+  /* 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 rule_set = new ParserRuleSet("isabelle", "MAIN")
@@ -122,6 +155,13 @@
     def to: Int => Int = model.to_current(document, _)
     def from: Int => Int = model.from_current(document, _)
 
+    for (text_area <- Isabelle.jedit_text_areas(model.buffer)
+          if Document_View(text_area).isDefined)
+      Document_View(text_area).get.set_styles()
+
+    def handle_token(style: Byte, offset: Int, length: Int) =
+      handler.handleToken(line_segment, style, offset, length, context)
+
     var next_x = start
     for {
       (command, command_start) <- document.command_range(from(start), from(stop))
@@ -137,7 +177,7 @@
         ((abs_stop - stop) max 0)
     }
     {
-      val byte =
+      val token_type =
         markup.info match {
           case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
             Isabelle_Token_Marker.command_style(kind)
@@ -146,15 +186,14 @@
           case _ => Token.NULL
         }
       if (start + token_start > next_x)
-        handler.handleToken(line_segment, 1,
-          next_x - start, start + token_start - next_x, context)
-      handler.handleToken(line_segment, byte, token_start, token_length, context)
+        handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
+      handle_token(token_type, token_start, token_length)
       next_x = start + token_start + token_length
     }
     if (next_x < stop)
-      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
+      handle_token(Token.COMMENT1, next_x - start, stop - next_x)
 
-    handler.handleToken(line_segment, Token.END, line_segment.count, 0, context)
+    handle_token(Token.END, line_segment.count, 0)
     handler.setLineContext(context)
     context
   }
diff -r b3ff14122645 -r 8e1e27a3b361 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Jun 01 15:59:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Jun 01 17:36:53 2010 +0200
@@ -228,6 +228,11 @@
         }
 
       case msg: PropertiesChanged =>
+        Swing_Thread.now {
+          for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
+            Document_View(text_area).get.extend_styles()
+        }
+
         Isabelle.session.global_settings.event(Session.Global_Settings)
 
       case _ =>