tuned;

--- a/src/Pure/PIDE/command.scala	Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Aug 14 11:52:24 2010 +0200
@@ -148,8 +148,7 @@
 
 class Command(
     val id: Document.Command_ID,
-    val span: Thy_Syntax.Span,
-    val static_parent: Option[Command] = None)  // FIXME !?
+    val span: List[Token])
 {
   /* classification */
 

--- a/src/Pure/PIDE/document.ML	Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Aug 14 11:52:24 2010 +0200
@@ -8,9 +8,9 @@
 signature DOCUMENT =
 sig
   type id = int
-  type exec_id = id
+  type version_id = id
   type command_id = id
-  type version_id = id
+  type exec_id = id
   val no_id: id
   val parse_id: string -> id
   val print_id: id -> string
@@ -23,9 +23,9 @@
 (* unique identifiers *)
 
 type id = int;
-type exec_id = id;
+type version_id = id;
 type command_id = id;
-type version_id = id;
+type exec_id = id;
 
 val no_id = 0;
 

--- a/src/Pure/PIDE/document.scala	Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Aug 14 11:52:24 2010 +0200
@@ -17,9 +17,9 @@
   /* formal identifiers */
 
   type ID = Long
-  type Exec_ID = ID
+  type Version_ID = ID
   type Command_ID = ID
-  type Version_ID = ID
+  type Exec_ID = ID
 
   val NO_ID: ID = 0
 
@@ -187,7 +187,7 @@
     }
 
 
-    /* phase 3: resulting document edits */
+    /* resulting document edits */
 
     {
       val doc_edits = new mutable.ListBuffer[Edit[Command]]
@@ -216,10 +216,10 @@
 
   /** global state -- accumulated prover results **/
 
-  class Failed_State(state: State) extends Exception
-
   object State
   {
+    class Fail(state: State) extends Exception
+
     val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil)
 
     class Assignment(former_assignment: Map[Command, Exec_ID])
@@ -237,20 +237,13 @@
   }
 
   case class State(
+    val documents: Map[Version_ID, Document] = Map(),
     val commands: Map[Command_ID, Command.State] = Map(),
-    val documents: Map[Version_ID, Document] = Map(),
     val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(),
     val assignments: Map[Document, State.Assignment] = Map(),
     val disposed: Set[ID] = Set())  // FIXME unused!?
   {
-    private def fail[A]: A = throw new Failed_State(this)
-
-    def define_command(command: Command): State =
-    {
-      val id = command.id
-      if (commands.isDefinedAt(id) || disposed(id)) fail
-      copy(commands = commands + (id -> command.empty_state))
-    }
+    private def fail[A]: A = throw new State.Fail(this)
 
     def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State =
     {
@@ -260,9 +253,17 @@
         assignments = assignments + (document -> new State.Assignment(former_assignment)))
     }
 
+    def define_command(command: Command): State =
+    {
+      val id = command.id
+      if (commands.isDefinedAt(id) || disposed(id)) fail
+      copy(commands = commands + (id -> command.empty_state))
+    }
+
     def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
+
+    def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
     def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
-    def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
     def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
     def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail)
 

--- a/src/Pure/PIDE/markup_node.scala	Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/PIDE/markup_node.scala	Sat Aug 14 11:52:24 2010 +0200
@@ -2,7 +2,7 @@
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
-Document markup nodes, with connection to Swing tree model.
+Text markup nodes.
 */
 
 package isabelle
@@ -78,8 +78,7 @@
 
 case class Markup_Text(val markup: List[Markup_Tree], val content: String)
 {
-  private lazy val root =
-    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
+  private val root = new Markup_Tree(new Markup_Node(0, content.length, None), markup)  // FIXME !?
 
   def + (new_tree: Markup_Tree): Markup_Text =
     new Markup_Text((root + new_tree).branches, content)

--- a/src/Pure/System/session.scala	Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/System/session.scala	Sat Aug 14 11:52:24 2010 +0200
@@ -139,12 +139,12 @@
             indicate_command_change(st.command)  // FIXME forward Command.State (!?)
           }
           catch {
-            case _: Document.Failed_State =>
+            case _: Document.State.Fail =>
               if (result.is_status) {
                 result.body match {
                   case List(Isar_Document.Assign(edits)) =>
                     try { change_state(_.assign(target_id, edits)) }
-                    catch { case _: Document.Failed_State => bad_result(result) }
+                    catch { case _: Document.State.Fail => bad_result(result) }
                   case _ => bad_result(result)
                 }
               }

--- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 14 11:52:24 2010 +0200
@@ -12,11 +12,9 @@
 
 object Thy_Syntax
 {
-  type Span = List[Token]
-
-  def parse_spans(toks: List[Token]): List[Span] =
+  def parse_spans(toks: List[Token]): List[List[Token]] =
   {
-    val result = new mutable.ListBuffer[Span]
+    val result = new mutable.ListBuffer[List[Token]]
     val span = new mutable.ListBuffer[Token]
     val whitespace = new mutable.ListBuffer[Token]