# HG changeset patch
# User wenzelm
# Date 1283157508 -7200
# Node ID 0f861635949db38595d852442486512631a2d15a
# Parent  23af89f419bbd51889d561d22f5ed835b9690fc8# Parent  35b2d91e88d762db11e8183f893633831c729ca1
merged

diff -r 23af89f419bb -r 0f861635949d src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Pure/Concurrent/future.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -28,6 +28,7 @@
 {
   def peek: Option[Exn.Result[A]]
   def is_finished: Boolean = peek.isDefined
+  def get_finished: A = { require(is_finished); Exn.release(peek.get) }
   def join: A
   def map[B](f: A => B): Future[B] = Future.fork { f(join) }
 
diff -r 23af89f419bb -r 0f861635949d src/Pure/Concurrent/volatile.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/volatile.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -0,0 +1,22 @@
+/*  Title:      Pure/Concurrent/volatile.scala
+    Author:     Makarius
+
+Volatile variables.
+*/
+
+package isabelle
+
+
+class Volatile[A](init: A)
+{
+  @volatile private var state: A = init
+  def peek(): A = state
+  def change(f: A => A) { state = f(state) }
+  def change_yield[B](f: A => (B, A)): B =
+  {
+    val (result, new_state) = f(state)
+    state = new_state
+    result
+  }
+}
+
diff -r 23af89f419bb -r 0f861635949d src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Pure/General/output.ML	Mon Aug 30 10:38:28 2010 +0200
@@ -79,11 +79,8 @@
 
 (* output primitives -- normally NOT used directly!*)
 
-fun std_output s = NAMED_CRITICAL "IO" (fn () =>
-  (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
-
-fun std_error s = NAMED_CRITICAL "IO" (fn () =>
-  (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
+fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
 
 fun writeln_default "" = ()
   | writeln_default s = std_output (suffix "\n" s);
diff -r 23af89f419bb -r 0f861635949d src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Pure/General/xml.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -112,7 +112,7 @@
         else
           lookup(x) match {
             case Some(y) => y
-            case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
+            case None => store(x.map(p => (cache_string(p._1).intern, cache_string(p._2))))
           }
       def cache_markup(x: Markup): Markup =
         lookup(x) match {
diff -r 23af89f419bb -r 0f861635949d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -116,7 +116,25 @@
   }
 
 
-  /* history navigation and persistent snapshots */
+  /* history navigation */
+
+  object History
+  {
+    val init = new History(List(Change.init))
+  }
+
+  // FIXME pruning, purging of state
+  class History(val undo_list: List[Change])
+  {
+    require(!undo_list.isEmpty)
+
+    def tip: Change = undo_list.head
+    def +(change: Change): History = new History(change :: undo_list)
+  }
+
+
+
+  /** global state -- document structure, execution process, editing history **/
 
   abstract class Snapshot
   {
@@ -129,54 +147,10 @@
     def convert(range: Text.Range): Text.Range = range.map(convert(_))
     def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range = range.map(revert(_))
-  }
-
-  object History
-  {
-    val init = new History(List(Change.init))
+    def select_markup[A](range: Text.Range)
+      (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]]
   }
 
-  // FIXME pruning, purging of state
-  class History(undo_list: List[Change])
-  {
-    require(!undo_list.isEmpty)
-
-    def tip: Change = undo_list.head
-    def +(ch: Change): History = new History(ch :: undo_list)
-
-    def snapshot(name: String, pending_edits: List[Text.Edit], state_snapshot: State): Snapshot =
-    {
-      val found_stable = undo_list.find(change =>
-        change.is_finished && state_snapshot.is_assigned(change.current.join))
-      require(found_stable.isDefined)
-      val stable = found_stable.get
-      val latest = undo_list.head
-
-      val edits =
-        (pending_edits /: undo_list.takeWhile(_ != stable))((edits, change) =>
-            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
-      lazy val reverse_edits = edits.reverse
-
-      new Snapshot
-      {
-        val version = stable.current.join
-        val node = version.nodes(name)
-        val is_outdated = !(pending_edits.isEmpty && latest == stable)
-        def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
-        def state(command: Command): Command.State =
-          try { state_snapshot.command_state(version, command) }
-          catch { case _: State.Fail => command.empty_state }
-
-        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
-        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
-      }
-    }
-  }
-
-
-
-  /** global state -- document structure and execution process **/
-
   object State
   {
     class Fail(state: State) extends Exception
@@ -189,6 +163,7 @@
       private val promise = Future.promise[Map[Command, Exec_ID]]
       def is_finished: Boolean = promise.is_finished
       def join: Map[Command, Exec_ID] = promise.join
+      def get_finished: Map[Command, Exec_ID] = promise.get_finished
       def assign(command_execs: List[(Command, Exec_ID)])
       {
         promise.fulfill(tmp_assignment ++ command_execs)
@@ -202,7 +177,8 @@
     val commands: Map[Command_ID, Command.State] = Map(),
     val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
     val assignments: Map[Version, State.Assignment] = Map(),
-    val disposed: Set[ID] = Set())  // FIXME unused!?
+    val disposed: Set[ID] = Set(),  // FIXME unused!?
+    val history: History = History.init)
   {
     private def fail[A]: A = throw new State.Fail(this)
 
@@ -265,11 +241,61 @@
         case None => false
       }
 
-    def command_state(version: Version, command: Command): Command.State =
+    def extend_history(previous: Future[Version],
+        edits: List[Node_Text_Edit],
+        result: Future[(List[Edit[Command]], Version)]): (Change, State) =
+    {
+      val change = new Change(previous, edits, result)
+      (change, copy(history = history + change))
+    }
+
+
+    // persistent user-view
+    def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
     {
-      val assgn = the_assignment(version)
-      require(assgn.is_finished)
-      the_exec_state(assgn.join.getOrElse(command, fail))
+      val found_stable = history.undo_list.find(change =>
+        change.is_finished && is_assigned(change.current.get_finished))
+      require(found_stable.isDefined)
+      val stable = found_stable.get
+      val latest = history.undo_list.head
+
+      val edits =
+        (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>
+            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+      lazy val reverse_edits = edits.reverse
+
+      new Snapshot
+      {
+        val version = stable.current.get_finished
+        val node = version.nodes(name)
+        val is_outdated = !(pending_edits.isEmpty && latest == stable)
+
+        def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
+
+        def state(command: Command): Command.State =
+          try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) }
+          catch { case _: State.Fail => command.empty_state }
+
+        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
+        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+
+        def select_markup[A](range: Text.Range)
+          (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
+        {
+          val former_range = revert(range)
+          for {
+            (command, command_start) <- node.command_range(former_range)
+            Text.Info(r0, x) <- state(command).markup.
+              select((former_range - command_start).restrict(command.range)) {
+                case Text.Info(r0, info)
+                if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
+                  result(Text.Info(convert(r0 + command_start), info))
+              } { default }
+            val r = convert(r0 + command_start)
+            if !r.is_singularity
+          } yield Text.Info(r, x)
+        }
+      }
     }
   }
 }
diff -r 23af89f419bb -r 0f861635949d src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -90,7 +90,7 @@
     Branches.overlapping(range, branches).toStream
 
   def select[A](root_range: Text.Range)
-    (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
+    (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
   {
     def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
       : Stream[Text.Info[A]] =
@@ -122,6 +122,7 @@
       }
     }
     stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
+      .iterator
   }
 
   def swing_tree(parent: DefaultMutableTreeNode)
diff -r 23af89f419bb -r 0f861635949d src/Pure/System/event_bus.scala
--- a/src/Pure/System/event_bus.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Pure/System/event_bus.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -32,4 +32,29 @@
   /* event invocation */
 
   def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
+
+
+  /* await global condition -- triggered via bus events */
+
+  def await(cond: => Boolean)
+  {
+    case object Wait
+    val a = new Actor {
+      def act {
+        if (cond) react { case Wait => reply(()); exit(Wait) }
+        else {
+          loop {
+            react {
+              case trigger if trigger != Wait =>
+                if (cond) { react { case Wait => reply(()); exit(Wait) } }
+            }
+          }
+        }
+      }
+    }
+    this += a
+    a.start
+    a !? Wait
+    this -= a
+  }
 }
diff -r 23af89f419bb -r 0f861635949d src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Pure/System/session.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -19,6 +19,7 @@
 
   case object Global_Settings
   case object Perspective
+  case object Assignment
   case class Commands_Changed(set: Set[Command])
 }
 
@@ -44,6 +45,7 @@
   val raw_output = new Event_Bus[Isabelle_Process.Result]
   val commands_changed = new Event_Bus[Session.Commands_Changed]
   val perspective = new Event_Bus[Session.Perspective.type]
+  val assignments = new Event_Bus[Session.Assignment.type]
 
 
   /* unique ids */
@@ -57,17 +59,64 @@
 
 
 
-  /** main actor **/
+  /** buffered command changes (delay_first discipline) **/
+
+  private case object Stop
+
+  private val command_change_buffer = Simple_Thread.actor("command_change_buffer", daemon = true)
+  //{{{
+  {
+    import scala.compat.Platform.currentTime
+
+    var changed: Set[Command] = Set()
+    var flush_time: Option[Long] = None
+
+    def flush_timeout: Long =
+      flush_time match {
+        case None => 5000L
+        case Some(time) => (time - currentTime) max 0
+      }
+
+    def flush()
+    {
+      if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
+      changed = Set()
+      flush_time = None
+    }
+
+    def invoke()
+    {
+      val now = currentTime
+      flush_time match {
+        case None => flush_time = Some(now + output_delay)
+        case Some(time) => if (now >= time) flush()
+      }
+    }
+
+    var finished = false
+    while (!finished) {
+      receiveWithin(flush_timeout) {
+        case command: Command => changed += command; invoke()
+        case TIMEOUT => flush()
+        case Stop => finished = true
+        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
+      }
+    }
+  }
+  //}}}
+
+
+
+  /** main protocol actor **/
 
   @volatile private var syntax = new Outer_Syntax(system.symbols)
   def current_syntax(): Outer_Syntax = syntax
 
-  @volatile private var global_state = Document.State.init
-  private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
-  def current_state(): Document.State = global_state
+  private val global_state = new Volatile(Document.State.init)
+  def current_state(): Document.State = global_state.peek()
 
+  private case class Edit_Version(edits: List[Document.Node_Text_Edit])
   private case class Started(timeout: Int, args: List[String])
-  private case object Stop
 
   private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
   {
@@ -79,12 +128,10 @@
     def handle_change(change: Document.Change)
     //{{{
     {
-      require(change.is_finished)
+      val previous = change.previous.get_finished
+      val (node_edits, current) = change.result.get_finished
 
-      val previous = change.previous.join
-      val (node_edits, current) = change.result.join
-
-      var former_assignment = current_state().the_assignment(previous).join
+      var former_assignment = global_state.peek().the_assignment(previous).get_finished
       for {
         (name, Some(cmd_edits)) <- node_edits
         (prev, None) <- cmd_edits
@@ -103,8 +150,8 @@
                     c2 match {
                       case None => None
                       case Some(command) =>
-                        if (current_state().lookup_command(command.id).isEmpty) {
-                          change_state(_.define_command(command))
+                        if (global_state.peek().lookup_command(command.id).isEmpty) {
+                          global_state.change(_.define_command(command))
                           prover.define_command(command.id, system.symbols.encode(command.source))
                         }
                         Some(command.id)
@@ -113,7 +160,7 @@
               }
             (name -> Some(ids))
         }
-      change_state(_.define_version(current, former_assignment))
+      global_state.change(_.define_version(current, former_assignment))
       prover.edit_version(previous.id, current.id, id_edits)
     }
     //}}}
@@ -134,16 +181,18 @@
       result.properties match {
         case Position.Id(state_id) =>
           try {
-            val (st, state) = global_state.accumulate(state_id, result.message)
-            global_state = state
-            indicate_command_change(st.command)
+            val st = global_state.change_yield(_.accumulate(state_id, result.message))
+            command_change_buffer ! st.command
           }
           catch { case _: Document.State.Fail => bad_result(result) }
         case _ =>
           if (result.is_status) {
             result.body match {
               case List(Isar_Document.Assign(id, edits)) =>
-                try { change_state(_.assign(id, edits)) }
+                try {
+                  global_state.change(_.assign(id, edits))
+                  assignments.event(Session.Assignment)
+                }
                 catch { case _: Document.State.Fail => bad_result(result) }
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name
@@ -202,6 +251,24 @@
     var finished = false
     while (!finished) {
       receive {
+        case Edit_Version(edits) =>
+          val previous = global_state.peek().history.tip.current
+          val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
+          val change = global_state.change_yield(_.extend_history(previous, edits, result))
+
+          val this_actor = self
+          change.current.map(_ => {
+            assignments.await { global_state.peek().is_assigned(previous.get_finished) }
+            this_actor ! change })
+
+          reply(())
+
+        case change: Document.Change if prover != null =>
+          handle_change(change)
+
+        case result: Isabelle_Process.Result =>
+          handle_result(result)
+
         case Started(timeout, args) =>
           if (prover == null) {
             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
@@ -219,13 +286,7 @@
             finished = true
           }
 
-        case change: Document.Change if prover != null =>
-          handle_change(change)
-
-        case result: Isabelle_Process.Result =>
-          handle_result(result)
-
-        case TIMEOUT =>  // FIXME clarify!
+        case TIMEOUT =>  // FIXME clarify
 
         case bad if prover != null =>
           System.err.println("session_actor: ignoring bad message " + bad)
@@ -235,95 +296,15 @@
 
 
 
-  /** buffered command changes (delay_first discipline) **/
-
-  private val command_change_buffer = actor
-  //{{{
-  {
-    import scala.compat.Platform.currentTime
-
-    var changed: Set[Command] = Set()
-    var flush_time: Option[Long] = None
-
-    def flush_timeout: Long =
-      flush_time match {
-        case None => 5000L
-        case Some(time) => (time - currentTime) max 0
-      }
-
-    def flush()
-    {
-      if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
-      changed = Set()
-      flush_time = None
-    }
-
-    def invoke()
-    {
-      val now = currentTime
-      flush_time match {
-        case None => flush_time = Some(now + output_delay)
-        case Some(time) => if (now >= time) flush()
-      }
-    }
-
-    loop {
-      reactWithin(flush_timeout) {
-        case command: Command => changed += command; invoke()
-        case TIMEOUT => flush()
-        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
-      }
-    }
-  }
-  //}}}
-
-  def indicate_command_change(command: Command)
-  {
-    command_change_buffer ! command
-  }
-
-
-
-  /** editor history **/
-
-  private case class Edit_Version(edits: List[Document.Node_Text_Edit])
-
-  @volatile private var history = Document.History.init
-
-  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
-    history.snapshot(name, pending_edits, current_state())
-
-  private val editor_history = actor
-  {
-    loop {
-      react {
-        case Edit_Version(edits) =>
-          val prev = history.tip.current
-          val result =
-            // FIXME potential denial-of-service concerning worker pool (!?!?)
-            isabelle.Future.fork {
-              val previous = prev.join
-              val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
-              Thy_Syntax.text_edits(Session.this, previous, edits)
-            }
-          val change = new Document.Change(prev, edits, result)
-          history += change
-          change.current.map(_ => session_actor ! change)
-          reply(())
-
-        case bad => System.err.println("editor_model: ignoring bad message " + bad)
-      }
-    }
-  }
-
-
-
   /** main methods **/
 
   def started(timeout: Int, args: List[String]): Option[String] =
     (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
 
-  def stop() { session_actor ! Stop }
+  def stop() { command_change_buffer ! Stop; session_actor ! Stop }
+
+  def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
 
-  def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
+  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
+    global_state.peek().snapshot(name, pending_edits)
 }
diff -r 23af89f419bb -r 0f861635949d src/Pure/System/swing_thread.scala
--- a/src/Pure/System/swing_thread.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Pure/System/swing_thread.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -23,7 +23,7 @@
 
   def now[A](body: => A): A =
   {
-    var result: Option[A] = None
+    @volatile var result: Option[A] = None
     if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
     else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
     result.get
diff -r 23af89f419bb -r 0f861635949d src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Pure/build-jars	Mon Aug 30 10:38:28 2010 +0200
@@ -24,6 +24,7 @@
 declare -a SOURCES=(
   Concurrent/future.scala
   Concurrent/simple_thread.scala
+  Concurrent/volatile.scala
   General/exn.scala
   General/linear_set.scala
   General/markup.scala
diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/dist-template/etc/settings
--- a/src/Tools/jEdit/dist-template/etc/settings	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/settings	Mon Aug 30 10:38:28 2010 +0200
@@ -4,8 +4,8 @@
 JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
 
 JEDIT_OPTIONS="-reuseview -noserver -nobackground"
-JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4"
-#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=8"
+JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
+#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=8 -Dactors.enableForkJoin=false"
 JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
 
 JEDIT_STYLE_SHEETS="$ISABELLE_HOME/lib/html/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Mon Aug 30 10:38:28 2010 +0200
@@ -29,6 +29,8 @@
 options.isabelle.relative-font-size=100
 options.isabelle.tooltip-font-size.title=Tooltip Font Size
 options.isabelle.tooltip-font-size=10
+options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
+options.isabelle.tooltip-dismiss-delay=8000
 options.isabelle.startup-timeout=10000
 
 #menu actions
diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -57,9 +57,18 @@
 
     /* line context */
 
-    private val rule_set = new ParserRuleSet("isabelle", "MAIN")
-    class LineContext(val line: Int, prev: LineContext)
-      extends TokenMarker.LineContext(rule_set, prev)
+    private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
+
+    class Line_Context(val line: Int, prev: Line_Context)
+      extends TokenMarker.LineContext(dummy_rules, prev)
+    {
+      override def hashCode: Int = line
+      override def equals(that: Any) =
+        that match {
+          case other: Line_Context => line == other.line
+          case _ => false
+        }
+    }
 
 
     /* mapping to jEdit token types */
@@ -256,18 +265,15 @@
     override def markTokens(prev: TokenMarker.LineContext,
         handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
     {
-      // FIXME proper synchronization / thread context (!??)
-      val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
+      Isabelle.swing_buffer_lock(buffer) {
+        val snapshot = Document_Model.this.snapshot()
 
-      Isabelle.buffer_read_lock(buffer) {
-        val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
+        val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context]
         val line = if (prev == null) 0 else previous.line + 1
-        val context = new Document_Model.Token_Markup.LineContext(line, previous)
+        val context = new Document_Model.Token_Markup.Line_Context(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)
 
         /* FIXME
         for (text_area <- Isabelle.jedit_text_areas(buffer)
@@ -290,27 +296,16 @@
             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 last = start
+        for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup)(Token.NULL)) {
+          val Text.Range(token_start, token_stop) = token.range
+          if (last < token_start)
+            handle_token(Token.COMMENT1, last - start, token_start - last)
+          handle_token(token.info, token_start - start, token_stop - token_start)
+          last = token_stop
         }
-        {
-          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)
+        if (last < stop)
+          handle_token(Token.COMMENT1, last - start, stop - last)
 
         handle_token(Token.END, line_segment.count, 0)
         handler.setLineContext(context)
diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -103,29 +103,26 @@
     loop {
       react {
         case Session.Commands_Changed(changed) =>
-          Swing_Thread.now {
-            // FIXME cover doc states as well!!?
+          val buffer = model.buffer
+          Isabelle.swing_buffer_lock(buffer) {
             val snapshot = model.snapshot()
-            val buffer = model.buffer
-            Isabelle.buffer_read_lock(buffer) {
-              if (changed.exists(snapshot.node.commands.contains)) {
-                var visible_change = false
+            if (changed.exists(snapshot.node.commands.contains)) {
+              var visible_change = false
+              for ((command, start) <- snapshot.node.command_starts) {
+                if (changed(command)) {
+                  val stop = start + command.length
+                  val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+                  val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
+                  if (line2 >= text_area.getFirstLine &&
+                      line1 <= text_area.getFirstLine + text_area.getVisibleLines)
+                    visible_change = true
+                  text_area.invalidateLineRange(line1, line2)
+                }
+              }
+              // FIXME danger of deadlock!?
+              if (visible_change) model.buffer.propertiesChanged()
 
-                for ((command, start) <- snapshot.node.command_starts) {
-                  if (changed(command)) {
-                    val stop = start + command.length
-                    val line1 = buffer.getLineOfOffset(snapshot.convert(start))
-                    val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
-                    if (line2 >= text_area.getFirstLine &&
-                        line1 <= text_area.getFirstLine + text_area.getVisibleLines)
-                      visible_change = true
-                    text_area.invalidateLineRange(line1, line2)
-                  }
-                }
-                if (visible_change) model.buffer.propertiesChanged()
-
-                overview.repaint()  // FIXME paint here!?
-              }
+              overview.repaint()  // FIXME really paint here!?
             }
           }
 
@@ -143,69 +140,64 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
     {
-      Swing_Thread.assert()
+      Isabelle.swing_buffer_lock(model.buffer) {
+        val snapshot = model.snapshot()
 
-      val snapshot = model.snapshot()
+        val command_range: Iterable[(Command, Text.Offset)] =
+        {
+          val range = snapshot.node.command_range(snapshot.revert(start(0)))
+          if (range.hasNext) {
+            val (cmd0, start0) = range.next
+            new Iterable[(Command, Text.Offset)] {
+              def iterator =
+                Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
+            }
+          }
+          else Iterable.empty
+        }
 
-      val command_range: Iterable[(Command, Text.Offset)] =
-      {
-        val range = snapshot.node.command_range(snapshot.revert(start(0)))
-        if (range.hasNext) {
-          val (cmd0, start0) = range.next
-          new Iterable[(Command, Text.Offset)] {
-            def iterator =
-              Document.Node.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))
+                if (p.y != q.y) System.err.println("Unexpected coordinates: " + p + ", " + q)
+                gfx.setColor(Document_View.choose_color(snapshot, command))
+                gfx.fillRect(p.x, y, q.x - p.x, line_height)
+              }
+            }
+            y += line_height
           }
         }
-        else Iterable.empty
+        finally { gfx.setColor(saved_color) }
       }
-
-      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) }
     }
 
     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 {
-        case Some((command, command_start)) =>
-          // FIXME Isar_Document.Tooltip extractor
-          (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) {
+      Isabelle.swing_buffer_lock(model.buffer) {
+        val snapshot = model.snapshot()
+        val offset = text_area.xyToOffset(x, y)
+        val markup =
+          snapshot.select_markup(Text.Range(offset, offset + 1)) {
             case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
-              val typing =
-                Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
-              Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40))
-          } { null }).head.info
-        case None => null
+              Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40))
+          } { null }
+        if (markup.hasNext) markup.next.info else null
       }
     }
   }
@@ -268,7 +260,7 @@
       super.paintComponent(gfx)
       Swing_Thread.assert()
       val buffer = model.buffer
-      Isabelle.buffer_read_lock(buffer) {
+      Isabelle.buffer_lock(buffer) {
         val snapshot = model.snapshot()
         val saved_color = gfx.getColor  // FIXME needed!?
         try {
diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -29,7 +29,8 @@
 {
   override def click(view: View) = {
     Isabelle.system.source_file(ref_file) match {
-      case None => System.err.println("Could not find source file " + ref_file)  // FIXME ??
+      case None =>
+        Library.error_dialog(view, "File not found", "Could not find source file " + ref_file)
       case Some(file) =>
         jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
     }
@@ -40,27 +41,24 @@
 {
   def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
   {
-    // FIXME lock buffer (!??)
     Swing_Thread.assert()
-    Document_Model(buffer) match {
-      case Some(model) =>
-        val snapshot = model.snapshot()
-        val offset = snapshot.revert(buffer_offset)
-        snapshot.node.command_at(offset) match {
-          case Some((command, command_start)) =>
-            // FIXME Isar_Document.Hyperlink extractor
-            (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) {
+    Isabelle.buffer_lock(buffer) {
+      Document_Model(buffer) match {
+        case Some(model) =>
+          val snapshot = model.snapshot()
+          val markup =
+            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
+              // FIXME Isar_Document.Hyperlink extractor
               case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _),
                   List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
-                val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
+                val Text.Range(begin, end) = info_range
                 val line = buffer.getLineOfOffset(begin)
-
                 (Position.File.unapply(props), Position.Line.unapply(props)) match {
                   case (Some(ref_file), Some(ref_line)) =>
                     new External_Hyperlink(begin, end, line, ref_file, ref_line)
                   case _ =>
-                    (Position.Id.unapply(props), Position.Offset.unapply(props)) match {
-                      case (Some(ref_id), Some(ref_offset)) =>
+                    (props, props) match {
+                      case (Position.Id(ref_id), Position.Offset(ref_offset)) =>
                         snapshot.lookup_command(ref_id) match {
                           case Some(ref_cmd) =>
                             snapshot.node.command_start(ref_cmd) match {
@@ -74,10 +72,11 @@
                       case _ => null
                     }
                 }
-            } { null }).head.info
-          case None => null
-        }
-      case None => null
+            } { null }
+          if (markup.hasNext) markup.next.info else null
+
+        case None => null
+      }
     }
   }
 }
diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/src/jedit/isabelle_options.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -17,6 +17,7 @@
   private val logic_name = new JComboBox()
   private val relative_font_size = new JSpinner()
   private val tooltip_font_size = new JSpinner()
+  private val tooltip_dismiss_delay = new JSpinner()
 
   private class List_Item(val name: String, val descr: String) {
     def this(name: String) = this(name, name)
@@ -46,6 +47,11 @@
       tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
       tooltip_font_size
     })
+
+    addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), {
+      tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000))
+      tooltip_dismiss_delay
+    })
   }
 
   override def _save()
@@ -58,5 +64,8 @@
 
     Isabelle.Int_Property("tooltip-font-size") =
       tooltip_font_size.getValue().asInstanceOf[Int]
+
+    Isabelle.Int_Property("tooltip-dismiss-delay") =
+      tooltip_dismiss_delay.getValue().asInstanceOf[Int]
   }
 }
diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Mon Aug 30 10:01:25 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Mon Aug 30 10:38:28 2010 +0200
@@ -81,6 +81,17 @@
         Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
       HTML.encode(text) + "</pre></html>"
 
+  def tooltip_dismiss_delay(): Int =
+    Int_Property("tooltip-dismiss-delay", 8000) max 500
+
+  def setup_tooltips()
+  {
+    Swing_Thread.now {
+      val manager = javax.swing.ToolTipManager.sharedInstance
+      manager.setDismissDelay(tooltip_dismiss_delay())
+    }
+  }
+
 
   /* settings */
 
@@ -118,12 +129,15 @@
   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
     jedit_text_areas().filter(_.getBuffer == buffer)
 
-  def buffer_read_lock[A](buffer: JEditBuffer)(body: => A): A =
+  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
   {
     try { buffer.readLock(); body }
     finally { buffer.readUnlock() }
   }
 
+  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
+    Swing_Thread.now { buffer_lock(buffer) { body } }
+
 
   /* dockable windows */
 
@@ -240,6 +254,8 @@
         Swing_Thread.now {
           for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
             Document_View(text_area).get.extend_styles()
+
+          Isabelle.setup_tooltips()
         }
 
         Isabelle.session.global_settings.event(Session.Global_Settings)
@@ -253,6 +269,8 @@
     Isabelle.system = new Isabelle_System
     Isabelle.system.install_fonts()
     Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
+
+    Isabelle.setup_tooltips()
   }
 
   override def stop()