1.1 --- a/Admin/isatest/settings/cygwin-poly-e	Tue Jun 01 15:59:01 2010 +0200
     1.2 +++ b/Admin/isatest/settings/cygwin-poly-e	Tue Jun 01 17:36:53 2010 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  # -*- shell-script -*- :mode=shellscript:
     1.5  
     1.6 -  POLYML_HOME="/home/isatest/homebroy/home/polyml/polyml-5.3.0"
     1.7 +  POLYML_HOME="/home/isatest/polyml-5.3.0"
     1.8    ML_SYSTEM="polyml-5.3.0"
     1.9    ML_PLATFORM="x86-cygwin"
    1.10    ML_HOME="$POLYML_HOME/$ML_PLATFORM"

     2.1 --- a/src/Pure/General/secure.ML	Tue Jun 01 15:59:01 2010 +0200
     2.2 +++ b/src/Pure/General/secure.ML	Tue Jun 01 17:36:53 2010 +0200
     2.3 @@ -13,7 +13,8 @@
     2.4    val use_text: use_context -> int * string -> bool -> string -> unit
     2.5    val use_file: use_context -> bool -> string -> unit
     2.6    val toplevel_pp: string list -> string -> unit
     2.7 -  val open_unsynchronized: unit -> unit
     2.8 +  val Isar_setup: unit -> unit
     2.9 +  val PG_setup: unit -> unit
    2.10    val commit: unit -> unit
    2.11    val bash_output: string -> string * int
    2.12    val bash: string -> int
    2.13 @@ -54,7 +55,9 @@
    2.14  val use_global = raw_use_text ML_Parse.global_context (0, "") false;
    2.15  
    2.16  fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
    2.17 -fun open_unsynchronized () = use_global "open Unsynchronized";
    2.18 +
    2.19 +fun Isar_setup () = use_global "open Unsynchronized;";
    2.20 +fun PG_setup () = use_global "structure ThyLoad = Thy_Load;";
    2.21  
    2.22  
    2.23  (* shell commands *)

     3.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jun 01 15:59:01 2010 +0200
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jun 01 17:36:53 2010 +0200
     3.3 @@ -245,6 +245,7 @@
     3.4            Unsynchronized.set initialized);
     3.5          sync_thy_loader ();
     3.6         Unsynchronized.change print_mode (update (op =) proof_generalN);
     3.7 +       Secure.PG_setup ();
     3.8         Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
     3.9  
    3.10  end;

     4.1 --- a/src/Pure/ROOT.ML	Tue Jun 01 15:59:01 2010 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Tue Jun 01 17:36:53 2010 +0200
     4.3 @@ -305,11 +305,9 @@
     4.4  structure PrintMode = Print_Mode;
     4.5  structure SpecParse = Parse_Spec;
     4.6  structure ThyInfo = Thy_Info;
     4.7 +structure ThyLoad = Thy_Load;
     4.8  structure ThyOutput = Thy_Output;
     4.9  structure TypeInfer = Type_Infer;
    4.10  
    4.11  end;
    4.12  
    4.13 -structure ThyLoad = Thy_Load;  (*Proof General legacy*)
    4.14 -
    4.15 -

     5.1 --- a/src/Pure/System/isar.ML	Tue Jun 01 15:59:01 2010 +0200
     5.2 +++ b/src/Pure/System/isar.ML	Tue Jun 01 17:36:53 2010 +0200
     5.3 @@ -138,7 +138,7 @@
     5.4  
     5.5  fun toplevel_loop {init = do_init, welcome, sync, secure} =
     5.6   (Context.set_thread_data NONE;
     5.7 -  Secure.open_unsynchronized ();
     5.8 +  Secure.Isar_setup ();
     5.9    if do_init then init () else ();
    5.10    if welcome then writeln (Session.welcome ()) else ();
    5.11    uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar sync)) ());

     6.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Jun 01 15:59:01 2010 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Jun 01 17:36:53 2010 +0200
     6.3 @@ -19,6 +19,7 @@
     6.4  
     6.5  import org.gjt.sp.jedit.gui.RolloverButton
     6.6  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
     6.7 +import org.gjt.sp.jedit.syntax.SyntaxStyle
     6.8  
     6.9  
    6.10  object Document_View
    6.11 @@ -78,6 +79,24 @@
    6.12    private val session = model.session
    6.13  
    6.14  
    6.15 +  /* extended token styles */
    6.16 +
    6.17 +  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
    6.18 +
    6.19 +  def extend_styles()
    6.20 +  {
    6.21 +    Swing_Thread.assert()
    6.22 +    styles = Isabelle_Token_Marker.extend_styles(text_area.getPainter.getStyles)
    6.23 +  }
    6.24 +  extend_styles()
    6.25 +
    6.26 +  def set_styles()
    6.27 +  {
    6.28 +    Swing_Thread.assert()
    6.29 +    text_area.getPainter.setStyles(styles)
    6.30 +  }
    6.31 +
    6.32 +
    6.33    /* commands_changed_actor */
    6.34  
    6.35    private val commands_changed_actor = actor {

     7.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Tue Jun 01 15:59:01 2010 +0200
     7.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Tue Jun 01 17:36:53 2010 +0200
     7.3 @@ -11,13 +11,46 @@
     7.4  import isabelle._
     7.5  
     7.6  import org.gjt.sp.jedit.buffer.JEditBuffer
     7.7 -import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, ParserRuleSet}
     7.8 +import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, ParserRuleSet, SyntaxStyle}
     7.9 +import org.gjt.sp.jedit.textarea.TextArea
    7.10  
    7.11 +import java.awt.Font
    7.12 +import java.awt.font.TextAttribute
    7.13  import javax.swing.text.Segment;
    7.14  
    7.15  
    7.16  object Isabelle_Token_Marker
    7.17  {
    7.18 +  /* extended token styles */
    7.19 +
    7.20 +  private val plain_range: Int = Token.ID_COUNT
    7.21 +  private val full_range: Int = 3 * plain_range
    7.22 +  private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    7.23 +
    7.24 +  def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    7.25 +  def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    7.26 +
    7.27 +  private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
    7.28 +  {
    7.29 +    import scala.collection.JavaConversions._
    7.30 +    val script_font =
    7.31 +      style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
    7.32 +    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
    7.33 +  }
    7.34 +
    7.35 +  def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    7.36 +  {
    7.37 +    val new_styles = new Array[SyntaxStyle](full_range)
    7.38 +    for (i <- 0 until plain_range) {
    7.39 +      val style = styles(i)
    7.40 +      new_styles(i) = style
    7.41 +      new_styles(subscript(i.toByte)) = script_style(style, -1)
    7.42 +      new_styles(superscript(i.toByte)) = script_style(style, 1)
    7.43 +    }
    7.44 +    new_styles
    7.45 +  }
    7.46 +
    7.47 +
    7.48    /* line context */
    7.49  
    7.50    private val rule_set = new ParserRuleSet("isabelle", "MAIN")
    7.51 @@ -122,6 +155,13 @@
    7.52      def to: Int => Int = model.to_current(document, _)
    7.53      def from: Int => Int = model.from_current(document, _)
    7.54  
    7.55 +    for (text_area <- Isabelle.jedit_text_areas(model.buffer)
    7.56 +          if Document_View(text_area).isDefined)
    7.57 +      Document_View(text_area).get.set_styles()
    7.58 +
    7.59 +    def handle_token(style: Byte, offset: Int, length: Int) =
    7.60 +      handler.handleToken(line_segment, style, offset, length, context)
    7.61 +
    7.62      var next_x = start
    7.63      for {
    7.64        (command, command_start) <- document.command_range(from(start), from(stop))
    7.65 @@ -137,7 +177,7 @@
    7.66          ((abs_stop - stop) max 0)
    7.67      }
    7.68      {
    7.69 -      val byte =
    7.70 +      val token_type =
    7.71          markup.info match {
    7.72            case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
    7.73              Isabelle_Token_Marker.command_style(kind)
    7.74 @@ -146,15 +186,14 @@
    7.75            case _ => Token.NULL
    7.76          }
    7.77        if (start + token_start > next_x)
    7.78 -        handler.handleToken(line_segment, 1,
    7.79 -          next_x - start, start + token_start - next_x, context)
    7.80 -      handler.handleToken(line_segment, byte, token_start, token_length, context)
    7.81 +        handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
    7.82 +      handle_token(token_type, token_start, token_length)
    7.83        next_x = start + token_start + token_length
    7.84      }
    7.85      if (next_x < stop)
    7.86 -      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
    7.87 +      handle_token(Token.COMMENT1, next_x - start, stop - next_x)
    7.88  
    7.89 -    handler.handleToken(line_segment, Token.END, line_segment.count, 0, context)
    7.90 +    handle_token(Token.END, line_segment.count, 0)
    7.91      handler.setLineContext(context)
    7.92      context
    7.93    }

     8.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Jun 01 15:59:01 2010 +0200
     8.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Jun 01 17:36:53 2010 +0200
     8.3 @@ -228,6 +228,11 @@
     8.4          }
     8.5  
     8.6        case msg: PropertiesChanged =>
     8.7 +        Swing_Thread.now {
     8.8 +          for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
     8.9 +            Document_View(text_area).get.extend_styles()
    8.10 +        }
    8.11 +
    8.12          Isabelle.session.global_settings.event(Session.Global_Settings)
    8.13  
    8.14        case _ =>