# HG changeset patch
# User haftmann
# Date 1275458505 -7200
# Node ID e7544b9ce6afd87019fcc668d4b012c1c660a700
# Parent  8e8e5f9d1441a15fea628503e1f5940382d6ffa3# Parent  8365cbc313492de0a67639767b74c56bc8c7bae7
merged

diff -r 8365cbc31349 -r e7544b9ce6af Admin/isatest/settings/cygwin-poly-e
--- a/Admin/isatest/settings/cygwin-poly-e	Tue Jun 01 17:25:00 2010 +0200
+++ b/Admin/isatest/settings/cygwin-poly-e	Wed Jun 02 08:01:45 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 8365cbc31349 -r e7544b9ce6af src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/General/secure.ML	Wed Jun 02 08:01:45 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 8365cbc31349 -r e7544b9ce6af src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Jun 02 08:01:45 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 8365cbc31349 -r e7544b9ce6af src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/ROOT.ML	Wed Jun 02 08:01:45 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 8365cbc31349 -r e7544b9ce6af src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/System/isar.ML	Wed Jun 02 08:01:45 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 8365cbc31349 -r e7544b9ce6af src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/display.ML	Wed Jun 02 08:01:45 2010 +0200
@@ -129,7 +129,7 @@
 
     fun prt_cls c = Syntax.pretty_sort ctxt [c];
     fun prt_sort S = Syntax.pretty_sort ctxt S;
-    fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
+    fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
     fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
     val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
diff -r 8365cbc31349 -r e7544b9ce6af src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/sorts.ML	Wed Jun 02 08:01:45 2010 +0200
@@ -26,7 +26,7 @@
   val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
   type algebra
   val classes_of: algebra -> serial Graph.T
-  val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
+  val arities_of: algebra -> (class * sort list) list Symtab.table
   val all_classes: algebra -> class list
   val super_classes: algebra -> class -> class list
   val class_less: algebra -> class * class -> bool
@@ -105,15 +105,14 @@
 
   arities: table of association lists of all type arities; (t, ars)
     means that type constructor t has the arities ars; an element
-    (c, (c0, Ss)) of ars represents the arity t::(Ss)c being derived
-    via c0 <= c.  "Coregularity" of the arities structure requires
-    that for any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that
-    c1 <= c2 holds Ss1 <= Ss2.
+    (c, Ss) of ars represents the arity t::(Ss)c.  "Coregularity" of
+    the arities structure requires that for any two declarations
+    t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2.
 *)
 
 datatype algebra = Algebra of
  {classes: serial Graph.T,
-  arities: (class * (class * sort list)) list Symtab.table};
+  arities: (class * sort list) list Symtab.table};
 
 fun classes_of (Algebra {classes, ...}) = classes;
 fun arities_of (Algebra {arities, ...}) = arities;
@@ -225,9 +224,9 @@
     Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
     Pretty.string_of_arity pp (t, Ss', [c']));
 
-fun coregular pp algebra t (c, (c0, Ss)) ars =
+fun coregular pp algebra t (c, Ss) ars =
   let
-    fun conflict (c', (_, Ss')) =
+    fun conflict (c', Ss') =
       if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
         SOME ((c, c'), (c', Ss'))
       else if class_le algebra (c', c) andalso not (sorts_le algebra (Ss', Ss)) then
@@ -236,19 +235,18 @@
   in
     (case get_first conflict ars of
       SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
-    | NONE => (c, (c0, Ss)) :: ars)
+    | NONE => (c, Ss) :: ars)
   end;
 
-fun complete algebra (c0, Ss) = map (rpair (c0, Ss)) (c0 :: super_classes algebra c0);
+fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
 
-fun insert pp algebra t (c, (c0, Ss)) ars =
+fun insert pp algebra t (c, Ss) ars =
   (case AList.lookup (op =) ars c of
-    NONE => coregular pp algebra t (c, (c0, Ss)) ars
-  | SOME (_, Ss') =>
+    NONE => coregular pp algebra t (c, Ss) ars
+  | SOME Ss' =>
       if sorts_le algebra (Ss, Ss') then ars
-      else if sorts_le algebra (Ss', Ss) then
-        coregular pp algebra t (c, (c0, Ss))
-          (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars)
+      else if sorts_le algebra (Ss', Ss)
+      then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
       else err_conflict pp t NONE (c, Ss) (c, Ss'));
 
 in
@@ -265,7 +263,7 @@
   algebra |> map_arities (insert_complete_ars pp algebra arg);
 
 fun add_arities_table pp algebra =
-  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, map snd ars));
+  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
 
 end;
 
@@ -310,16 +308,17 @@
   in make_algebra (classes', arities') end;
 
 
-(* algebra projections *)
+(* algebra projections *)  (* FIXME potentially violates abstract type integrity *)
 
 fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
   let
     val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
-    fun restrict_arity tyco (c, (_, Ss)) =
-      if P c then case sargs (c, tyco)
-       of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
-          |> map restrict_sort))
-        | NONE => NONE
+    fun restrict_arity t (c, Ss) =
+      if P c then
+        (case sargs (c, t) of
+          SOME sorts =>
+            SOME (c, Ss |> map2 (curry (inter_sort algebra)) sorts |> map restrict_sort)
+        | NONE => NONE)
       else NONE;
     val classes' = classes |> Graph.subgraph P;
     val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
@@ -355,7 +354,7 @@
     fun dom c =
       (case AList.lookup (op =) (Symtab.lookup_list arities a) c of
         NONE => raise CLASS_ERROR (No_Arity (a, c))
-      | SOME (_, Ss) => Ss);
+      | SOME Ss => Ss);
     fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);
   in
     (case S of
@@ -380,11 +379,8 @@
   in uncurry meet end;
 
 fun meet_sort_typ algebra (T, S) =
-  let
-    val tab = meet_sort algebra (T, S) Vartab.empty;
-  in Term.map_type_tvar (fn (v, _) =>
-    TVar (v, (the o Vartab.lookup tab) v))
-  end;
+  let val tab = meet_sort algebra (T, S) Vartab.empty;
+  in Term.map_type_tvar (fn (v, _) => TVar (v, (the o Vartab.lookup tab) v)) end;
 
 
 (* of_sort *)
@@ -425,9 +421,9 @@
           in
             S |> map (fn c =>
               let
-                val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
+                val Ss' = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
                 val dom' = map (fn ((U, d), S') => weaken U d S' ~~ S') ((Us ~~ dom) ~~ Ss');
-              in class_relation T (type_constructor (a, Us) dom' c0, c0) c end)
+              in type_constructor (a, Us) dom' c end)
           end
       | derive (T, S) = weaken T (type_variable T) S;
   in derive end;
diff -r 8365cbc31349 -r e7544b9ce6af src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Wed Jun 02 08:01:45 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 8365cbc31349 -r e7544b9ce6af src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Wed Jun 02 08:01:45 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 8365cbc31349 -r e7544b9ce6af src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Jun 02 08:01:45 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 _ =>