more explicit treatment of Swing thread context;
Document_Model.snapshot: require Swing thread;

--- a/src/Pure/System/swing_thread.scala	Sat Aug 07 14:45:26 2010 +0200
+++ b/src/Pure/System/swing_thread.scala	Sat Aug 07 16:15:52 2010 +0200
@@ -46,8 +46,9 @@
 
   private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
   {
-    val listener =
-      new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
+    val listener = new ActionListener {
+      override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
+    }
     val timer = new Timer(time_span, listener)
     timer.setRepeats(false)
 

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 14:45:26 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 16:15:52 2010 +0200
@@ -151,7 +151,7 @@
 
   def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
   {
-    Swing_Thread.assert()
+    Swing_Thread.require()
     val model = new Document_Model(session, buffer, thy_name)
     buffer.setProperty(key, model)
     model.activate()
@@ -160,7 +160,7 @@
 
   def apply(buffer: Buffer): Option[Document_Model] =
   {
-    Swing_Thread.assert()
+    Swing_Thread.require()
     buffer.getProperty(key) match {
       case model: Document_Model => Some(model)
       case _ => None
@@ -169,7 +169,7 @@
 
   def exit(buffer: Buffer)
   {
-    Swing_Thread.assert()
+    Swing_Thread.require()
     apply(buffer) match {
       case None => error("No document model for buffer: " + buffer)
       case Some(model) =>
@@ -209,8 +209,10 @@
 
   /* snapshot */
 
-  def snapshot(): Change.Snapshot =
-    Swing_Thread.now { session.current_change().snapshot(thy_name, edits_buffer.toList) }
+  def snapshot(): Change.Snapshot = {
+    Swing_Thread.require()
+    session.current_change().snapshot(thy_name, edits_buffer.toList)
+  }
 
 
   /* buffer listener */
@@ -246,7 +248,7 @@
       val start = buffer.getLineStartOffset(line)
       val stop = start + line_segment.count
 
-      val snapshot = Document_Model.this.snapshot()
+      val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
 
       /* FIXME
       for (text_area <- Isabelle.jedit_text_areas(buffer)

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat Aug 07 14:45:26 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat Aug 07 16:15:52 2010 +0200
@@ -46,7 +46,7 @@
 
   def init(model: Document_Model, text_area: TextArea): Document_View =
   {
-    Swing_Thread.assert()
+    Swing_Thread.require()
     val doc_view = new Document_View(model, text_area)
     text_area.putClientProperty(key, doc_view)
     doc_view.activate()
@@ -55,7 +55,7 @@
 
   def apply(text_area: TextArea): Option[Document_View] =
   {
-    Swing_Thread.assert()
+    Swing_Thread.require()
     text_area.getClientProperty(key) match {
       case doc_view: Document_View => Some(doc_view)
       case _ => None
@@ -64,7 +64,7 @@
 
   def exit(text_area: TextArea)
   {
-    Swing_Thread.assert()
+    Swing_Thread.require()
     apply(text_area) match {
       case None => error("No document view for text area: " + text_area)
       case Some(doc_view) =>
@@ -86,14 +86,14 @@
 
   def extend_styles()
   {
-    Swing_Thread.assert()
+    Swing_Thread.require()
     styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
   }
   extend_styles()
 
   def set_styles()
   {
-    Swing_Thread.assert()
+    Swing_Thread.require()
     text_area.getPainter.setStyles(styles)
   }
 
@@ -118,7 +118,7 @@
 
   def full_repaint(snapshot: Change.Snapshot, changed: Set[Command])
   {
-    Swing_Thread.assert()
+    Swing_Thread.require()
 
     val buffer = model.buffer
     var visible_change = false
@@ -148,54 +148,56 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
     {
-      Swing_Thread.now {
-        val snapshot = model.snapshot()
+      Swing_Thread.assert()
+
+      val snapshot = model.snapshot()
+
+      val command_range: Iterable[(Command, Int)] =
+      {
+        val range = snapshot.node.command_range(snapshot.revert(start(0)))
+        if (range.hasNext) {
+          val (cmd0, start0) = range.next
+          new Iterable[(Command, Int)] {
+            def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
+          }
+        }
+        else Iterable.empty
+      }
 
-        val command_range: Iterable[(Command, Int)] =
-        {
-          val range = snapshot.node.command_range(snapshot.revert(start(0)))
-          if (range.hasNext) {
-            val (cmd0, start0) = range.next
-            new Iterable[(Command, Int)] {
-              def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
+      val saved_color = gfx.getColor
+      try {
+        var y = y0
+        for (i <- 0 until physical_lines.length) {
+          if (physical_lines(i) != -1) {
+            val line_start = start(i)
+            val line_end = model.visible_line_end(line_start, end(i))
+
+            val a = snapshot.revert(line_start)
+            val b = snapshot.revert(line_end)
+            val cmds = command_range.iterator.
+              dropWhile { case (cmd, c) => c + cmd.length <= a } .
+              takeWhile { case (_, c) => c < b }
+
+            for ((command, command_start) <- cmds if !command.is_ignored) {
+              val p =
+                text_area.offsetToXY(line_start max snapshot.convert(command_start))
+              val q =
+                text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
+              assert(p.y == q.y)
+              gfx.setColor(Document_View.choose_color(snapshot, command))
+              gfx.fillRect(p.x, y, q.x - p.x, line_height)
             }
           }
-          else Iterable.empty
+          y += line_height
         }
-
-        val saved_color = gfx.getColor
-        try {
-          var y = y0
-          for (i <- 0 until physical_lines.length) {
-            if (physical_lines(i) != -1) {
-              val line_start = start(i)
-              val line_end = model.visible_line_end(line_start, end(i))
-
-              val a = snapshot.revert(line_start)
-              val b = snapshot.revert(line_end)
-              val cmds = command_range.iterator.
-                dropWhile { case (cmd, c) => c + cmd.length <= a } .
-                takeWhile { case (_, c) => c < b }
-
-              for ((command, command_start) <- cmds if !command.is_ignored) {
-                val p =
-                  text_area.offsetToXY(line_start max snapshot.convert(command_start))
-                val q =
-                  text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
-                assert(p.y == q.y)
-                gfx.setColor(Document_View.choose_color(snapshot, command))
-                gfx.fillRect(p.x, y, q.x - p.x, line_height)
-              }
-            }
-            y += line_height
-          }
-        }
-        finally { gfx.setColor(saved_color) }
       }
+      finally { gfx.setColor(saved_color) }
     }
 
     override def getToolTipText(x: Int, y: Int): String =
     {
+      Swing_Thread.assert()
+
       val snapshot = model.snapshot()
       val offset = snapshot.revert(text_area.xyToOffset(x, y))
       snapshot.node.command_at(offset) match {
@@ -213,7 +215,10 @@
   /* caret handling */
 
   def selected_command(): Option[Command] =
+  {
+    Swing_Thread.require()
     model.snapshot().node.proper_command_at(text_area.getCaretPosition)
+  }
 
   private val caret_listener = new CaretListener {
     private val delay = Swing_Thread.delay_last(session.input_delay) {

--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sat Aug 07 14:45:26 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sat Aug 07 16:15:52 2010 +0200
@@ -40,6 +40,7 @@
 {
   def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
   {
+    Swing_Thread.assert()
     Document_Model(buffer) match {
       case Some(model) =>
         val snapshot = model.snapshot()

--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat Aug 07 14:45:26 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat Aug 07 16:15:52 2010 +0200
@@ -95,7 +95,7 @@
     import Isabelle_Sidekick.int_to_pos
 
     val root = data.root
-    val doc = model.snapshot().node  // FIXME cover all nodes (!??)
+    val doc = Swing_Thread.now { model.snapshot().node }  // FIXME cover all nodes (!??)
     for {
       (command, command_start) <- doc.command_range(0)
       if command.is_command && !stopped
@@ -128,7 +128,7 @@
     import Isabelle_Sidekick.int_to_pos
 
     val root = data.root
-    val snapshot = model.snapshot()  // FIXME cover all nodes (!??)
+    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
       root.add(snapshot.document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
           {

--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat Aug 07 14:45:26 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat Aug 07 16:15:52 2010 +0200
@@ -22,7 +22,7 @@
 
 class Output_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  Swing_Thread.assert()
+  Swing_Thread.require()
 
   val html_panel =
     new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))