# HG changeset patch
# User wenzelm
# Date 1309024987 -7200
# Node ID df80747342cb69bad780cf184a2401baad40c1e7
# Parent  156c822f181a44533c4803fb2a6692305aed104c
proper tokens only if session is ready;

diff -r 156c822f181a -r df80747342cb src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jun 25 19:38:35 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Jun 25 20:03:07 2011 +0200
@@ -129,6 +129,7 @@
     _phase = new_phase
     phase_changed.event(new_phase)
   }
+  def is_ready: Boolean = phase == Session.Ready
 
   private val global_state = new Volatile(Document.State.init)
   def current_state(): Document.State = global_state.peek()
diff -r 156c822f181a -r df80747342cb src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Jun 25 19:38:35 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Jun 25 20:03:07 2011 +0200
@@ -161,39 +161,48 @@
     override def markTokens(context: TokenMarker.LineContext,
         handler: TokenHandler, line: Segment): TokenMarker.LineContext =
     {
-      val symbols = Isabelle.system.symbols
-      val syntax = Isabelle.session.current_syntax()
-
-      val ctxt =
-        context match {
-          case c: Line_Context => c.context
-          case _ => Scan.Finished
+      val context1 =
+        if (Isabelle.session.is_ready) {
+          val symbols = Isabelle.system.symbols
+          val syntax = Isabelle.session.current_syntax()
+    
+          val ctxt =
+            context match {
+              case c: Line_Context => c.context
+              case _ => Scan.Finished
+            }
+          val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
+          val context1 = new Line_Context(ctxt1)
+    
+          val extended = extended_styles(symbols, line)
+    
+          var offset = 0
+          for (token <- tokens) {
+            val style = Isabelle_Markup.token_markup(syntax, token)
+            val length = token.source.length
+            val end_offset = offset + length
+            if ((offset until end_offset) exists extended.isDefinedAt) {
+              for (i <- offset until end_offset) {
+                val style1 =
+                  extended.get(i) match {
+                    case None => style
+                    case Some(ext) => ext(style)
+                  }
+                handler.handleToken(line, style1, i, 1, context1)
+              }
+            }
+            else handler.handleToken(line, style, offset, length, context1)
+            offset += length
+          }
+          handler.handleToken(line, JEditToken.END, line.count, 0, context1)
+          context1
         }
-      val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
-      val context1 = new Line_Context(ctxt1)
-
-      val extended = extended_styles(symbols, line)
-
-      var offset = 0
-      for (token <- tokens) {
-        val style = Isabelle_Markup.token_markup(syntax, token)
-        val length = token.source.length
-        val end_offset = offset + length
-        if ((offset until end_offset) exists extended.isDefinedAt) {
-          for (i <- offset until end_offset) {
-            val style1 =
-              extended.get(i) match {
-                case None => style
-                case Some(ext) => ext(style)
-              }
-            handler.handleToken(line, style1, i, 1, context1)
-          }
+        else {
+          val context1 = new Line_Context(Scan.Finished)
+          handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
+          handler.handleToken(line, JEditToken.END, line.count, 0, context1)
+          context1
         }
-        else handler.handleToken(line, style, offset, length, context1)
-        offset += length
-      }
-      handler.handleToken(line, JEditToken.END, line.count, 0, context1)
-
       val context2 = context1.intern
       handler.setLineContext(context2)
       context2