Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Aug 23 17:35:47 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Mon Aug 23 17:45:06 2010 +0200
@@ -259,61 +259,63 @@
       // FIXME proper synchronization / thread context (!??)
       val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
 
-      val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
-      val line = if (prev == null) 0 else previous.line + 1
-      val context = new Document_Model.Token_Markup.LineContext(line, previous)
+      Isabelle.buffer_read_lock(buffer) {
+        val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
+        val line = if (prev == null) 0 else previous.line + 1
+        val context = new Document_Model.Token_Markup.LineContext(line, previous)
 
-      val start = buffer.getLineStartOffset(line)
-      val stop = start + line_segment.count
-      val range = Text.Range(start, stop)
-      val former_range = snapshot.revert(range)
+        val start = buffer.getLineStartOffset(line)
+        val stop = start + line_segment.count
+        val range = Text.Range(start, stop)
+        val former_range = snapshot.revert(range)
 
-      /* FIXME
-      for (text_area <- Isabelle.jedit_text_areas(buffer)
-            if Document_View(text_area).isDefined)
-        Document_View(text_area).get.set_styles()
-      */
+        /* 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)
+        def handle_token(style: Byte, offset: Text.Offset, length: Int) =
+          handler.handleToken(line_segment, style, offset, length, context)
 
-      val syntax = session.current_syntax()
-      val token_markup: PartialFunction[Text.Info[Any], Byte] =
-      {
-        case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
-        if syntax.keyword_kind(name).isDefined =>
-          Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
+        val syntax = session.current_syntax()
+        val token_markup: PartialFunction[Text.Info[Any], Byte] =
+        {
+          case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
+          if syntax.keyword_kind(name).isDefined =>
+            Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
 
-        case Text.Info(_, XML.Elem(Markup(name, _), _))
-        if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
-          Document_Model.Token_Markup.token_style(name)
-      }
+          case Text.Info(_, XML.Elem(Markup(name, _), _))
+          if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
+            Document_Model.Token_Markup.token_style(name)
+        }
 
-      var next_x = start
-      for {
-        (command, command_start) <- snapshot.node.command_range(former_range)
-        info <- snapshot.state(command).markup.
-          select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL)
-        val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start)
-        if abs_stop > start && abs_start < stop  // FIXME abs_range overlaps range (redundant!?)
+        var next_x = start
+        for {
+          (command, command_start) <- snapshot.node.command_range(former_range)
+          info <- snapshot.state(command).markup.
+            select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL)
+          val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start)
+          if abs_stop > start && abs_start < stop  // FIXME abs_range overlaps range (redundant!?)
+        }
+        {
+          val token_start = (abs_start - start) max 0
+          val token_length =
+            (abs_stop - abs_start) -
+            ((start - abs_start) max 0) -
+            ((abs_stop - stop) max 0)
+          if (start + token_start > next_x)  // FIXME ??
+            handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
+          handle_token(info.info, token_start, token_length)
+          next_x = start + token_start + token_length
+        }
+        if (next_x < stop)  // FIXME ??
+          handle_token(Token.COMMENT1, next_x - start, stop - next_x)
+
+        handle_token(Token.END, line_segment.count, 0)
+        handler.setLineContext(context)
+        context
       }
-      {
-        val token_start = (abs_start - start) max 0
-        val token_length =
-          (abs_stop - abs_start) -
-          ((start - abs_start) max 0) -
-          ((abs_stop - stop) max 0)
-        if (start + token_start > next_x)  // FIXME ??
-          handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
-        handle_token(info.info, token_start, token_length)
-        next_x = start + token_start + token_length
-      }
-      if (next_x < stop)  // FIXME ??
-        handle_token(Token.COMMENT1, next_x - start, stop - next_x)
-
-      handle_token(Token.END, line_segment.count, 0)
-      handler.setLineContext(context)
-      context
     }
   }