# HG changeset patch
# User wenzelm
# Date 1281347130 -7200
# Node ID ea417f69b36f5f981b9cc49a5429e9bf4308b093
# Parent  b32a443611868dd652472864b7f0510e3e44b728# Parent  3925c6b471855d39a18269344c6d306818939bfc
merged

diff -r b32a44361186 -r ea417f69b36f etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Aug 09 11:38:32 2010 +0200
+++ b/etc/isar-keywords-ZF.el	Mon Aug 09 11:45:30 2010 +0200
@@ -8,10 +8,8 @@
   '("\\."
     "\\.\\."
     "Isabelle\\.command"
-    "Isar\\.begin_document"
     "Isar\\.define_command"
     "Isar\\.edit_document"
-    "Isar\\.end_document"
     "ML"
     "ML_command"
     "ML_prf"
@@ -258,10 +256,8 @@
 
 (defconst isar-keywords-control
   '("Isabelle\\.command"
-    "Isar\\.begin_document"
     "Isar\\.define_command"
     "Isar\\.edit_document"
-    "Isar\\.end_document"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
diff -r b32a44361186 -r ea417f69b36f etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Aug 09 11:38:32 2010 +0200
+++ b/etc/isar-keywords.el	Mon Aug 09 11:45:30 2010 +0200
@@ -8,10 +8,8 @@
   '("\\."
     "\\.\\."
     "Isabelle\\.command"
-    "Isar\\.begin_document"
     "Isar\\.define_command"
     "Isar\\.edit_document"
-    "Isar\\.end_document"
     "ML"
     "ML_command"
     "ML_prf"
@@ -322,10 +320,8 @@
 
 (defconst isar-keywords-control
   '("Isabelle\\.command"
-    "Isar\\.begin_document"
     "Isar\\.define_command"
     "Isar\\.edit_document"
-    "Isar\\.end_document"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
diff -r b32a44361186 -r ea417f69b36f src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -61,7 +61,7 @@
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
   val shutdown: unit -> unit
-  val report: (unit -> 'a) -> 'a
+  val status: (unit -> 'a) -> 'a
 end;
 
 structure Future: FUTURE =
@@ -532,9 +532,9 @@
   else ();
 
 
-(* report markup *)
+(* status markup *)
 
-fun report e =
+fun status e =
   let
     val _ = Output.status (Markup.markup Markup.forked "");
     val x = e ();  (*sic -- report "joined" only for success*)
diff -r b32a44361186 -r ea417f69b36f src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/General/markup.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -9,7 +9,7 @@
   type T = string * Properties.T
   val none: T
   val is_none: T -> bool
-  val properties: (string * string) list -> T -> T
+  val properties: Properties.T -> T -> T
   val nameN: string
   val name: string -> T -> T
   val bindingN: string val binding: string -> T
@@ -93,7 +93,7 @@
   val commentN: string val comment: T
   val controlN: string val control: T
   val malformedN: string val malformed: T
-  val tokenN: string val token: T
+  val tokenN: string val token: Properties.T -> T
   val command_spanN: string val command_span: string -> T
   val ignored_spanN: string val ignored_span: T
   val malformed_spanN: string val malformed_span: T
@@ -284,7 +284,8 @@
 val (controlN, control) = markup_elem "control";
 val (malformedN, malformed) = markup_elem "malformed";
 
-val (tokenN, token) = markup_elem "token";
+val tokenN = "token";
+fun token props = (tokenN, props);
 
 val (command_spanN, command_span) = markup_string "command_span" nameN;
 val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
diff -r b32a44361186 -r ea417f69b36f src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/General/markup.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -183,7 +183,7 @@
 
   /* interactive documents */
 
-  val ASSIGN = "assign"
+  val Assign = Markup("assign", Nil)
   val EDIT = "edit"
 
 
@@ -196,6 +196,7 @@
 
   val INIT = "init"
   val STATUS = "status"
+  val REPORT = "report"
   val WRITELN = "writeln"
   val TRACING = "tracing"
   val WARNING = "warning"
@@ -207,10 +208,12 @@
   val SIGNAL = "signal"
   val EXIT = "exit"
 
-  val READY = "ready"
+  val Ready = Markup("ready", Nil)
 
 
   /* system data */
 
-  val DATA = "data"
+  val Data = Markup("data", Nil)
 }
+
+sealed case class Markup(name: String, properties: List[(String, String)])
diff -r b32a44361186 -r ea417f69b36f src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/General/output.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -39,9 +39,11 @@
   val debug_fn: (output -> unit) Unsynchronized.ref
   val prompt_fn: (output -> unit) Unsynchronized.ref
   val status_fn: (output -> unit) Unsynchronized.ref
+  val report_fn: (output -> unit) Unsynchronized.ref
   val error_msg: string -> unit
   val prompt: string -> unit
   val status: string -> unit
+  val report: string -> unit
   val debugging: bool Unsynchronized.ref
   val no_warnings_CRITICAL: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
@@ -98,6 +100,7 @@
 val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
 val prompt_fn = Unsynchronized.ref std_output;
 val status_fn = Unsynchronized.ref (fn _: string => ());
+val report_fn = Unsynchronized.ref (fn _: string => ());
 
 fun writeln s = ! writeln_fn (output s);
 fun priority s = ! priority_fn (output s);
@@ -106,6 +109,7 @@
 fun error_msg s = ! error_fn (output s);
 fun prompt s = ! prompt_fn (output s);
 fun status s = ! status_fn (output s);
+fun report s = ! report_fn (output s);
 
 fun legacy_feature s = warning ("Legacy feature! " ^ s);
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/General/position.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -127,7 +127,7 @@
 
 fun report_text markup (pos as Pos (count, _)) txt =
   if invalid_count count then ()
-  else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) txt);
+  else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
 
 fun report markup pos = report_text markup pos "";
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/General/pretty.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -17,11 +17,11 @@
   object Block
   {
     def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
-      XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body)
+      XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent.toString))), body)
 
     def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
       tree match {
-        case XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent)), body) =>
+        case XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent))), body) =>
           Markup.parse_int(indent) match {
             case Some(i) => Some((i, body))
             case None => None
@@ -33,12 +33,12 @@
   object Break
   {
     def apply(width: Int): XML.Tree =
-      XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)),
+      XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width.toString))),
         List(XML.Text(Symbol.spaces(width))))
 
     def unapply(tree: XML.Tree): Option[Int] =
       tree match {
-        case XML.Elem(Markup.BREAK, List((Markup.WIDTH, width)), _) => Markup.parse_int(width)
+        case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width))), _) => Markup.parse_int(width)
         case _ => None
       }
   }
@@ -50,7 +50,7 @@
 
   private def standard_format(tree: XML.Tree): List[XML.Tree] =
     tree match {
-      case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(standard_format)))
+      case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format)))
       case XML.Text(text) =>
         Library.separate(FBreak,
           Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
@@ -82,7 +82,7 @@
 
     def content_length(tree: XML.Tree): Double =
       tree match {
-        case XML.Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
+        case XML.Elem(_, body) => (0.0 /: body)(_ + content_length(_))
         case XML.Text(s) => metric(s)
       }
 
@@ -122,10 +122,10 @@
           else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
         case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
 
-        case XML.Elem(name, atts, body) :: ts =>
+        case XML.Elem(markup, body) :: ts =>
           val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
           val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
-          val btext1 = btext.copy(tx = XML.Elem(name, atts, btext.content) :: text.tx)
+          val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
           format(ts1, blockin, after, btext1)
         case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
       }
@@ -146,7 +146,7 @@
         case Block(_, body) => body.flatMap(fmt)
         case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
         case FBreak => List(XML.Text(Symbol.space))
-        case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt)))
+        case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
         case XML.Text(_) => List(tree)
       }
     input.flatMap(standard_format).flatMap(fmt)
diff -r b32a44361186 -r ea417f69b36f src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/General/xml.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -1,14 +1,14 @@
 (*  Title:      Pure/General/xml.ML
     Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
 
-Basic support for XML.
+Simple XML tree values.
 *)
 
 signature XML =
 sig
   type attributes = Properties.T
   datatype tree =
-      Elem of string * attributes * tree list
+      Elem of Markup.T * tree list
     | Text of string
   val add_content: tree -> Buffer.T -> Buffer.T
   val header: string
@@ -32,10 +32,10 @@
 type attributes = Properties.T;
 
 datatype tree =
-    Elem of string * attributes * tree list
+    Elem of Markup.T * tree list
   | Text of string;
 
-fun add_content (Elem (_, _, ts)) = fold add_content ts
+fun add_content (Elem (_, ts)) = fold add_content ts
   | add_content (Text s) = Buffer.add s;
 
 
@@ -84,9 +84,9 @@
 
 fun buffer_of tree =
   let
-    fun traverse (Elem (name, atts, [])) =
+    fun traverse (Elem ((name, atts), [])) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
-      | traverse (Elem (name, atts, ts)) =
+      | traverse (Elem ((name, atts), ts)) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
           fold traverse ts #>
           Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
@@ -170,8 +170,7 @@
         (Scan.this_string "/>" >> ignored
          || $$ ">" |-- parse_content --|
             !! (err ("Expected </" ^ s ^ ">"))
-              (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >>
-    (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
+              (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >> Elem) xs;
 
 val parse_document =
   (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
diff -r b32a44361186 -r ea417f69b36f src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/General/xml.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -24,11 +24,11 @@
       s.toString
     }
   }
-  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
+  case class Elem(markup: Markup, body: List[Tree]) extends Tree
   case class Text(content: String) extends Tree
 
-  def elem(name: String, body: List[Tree]) = Elem(name, Nil, body)
-  def elem(name: String) = Elem(name, Nil, Nil)
+  def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
+  def elem(name: String) = Elem(Markup(name, Nil), Nil)
 
 
   /* string representation */
@@ -56,9 +56,9 @@
 
   private def append_tree(tree: Tree, s: StringBuilder) {
     tree match {
-      case Elem(name, atts, Nil) =>
+      case Elem(Markup(name, atts), Nil) =>
         s ++= "<"; append_elem(name, atts, s); s ++= "/>"
-      case Elem(name, atts, ts) =>
+      case Elem(Markup(name, atts), ts) =>
         s ++= "<"; append_elem(name, atts, s); s ++= ">"
         for (t <- ts) append_tree(t, s)
         s ++= "</"; s ++= name; s ++= ">"
@@ -72,7 +72,7 @@
   private type State = Option[(String, List[Tree])]
 
   private def get_next(tree: Tree): State = tree match {
-    case Elem(_, _, body) => get_nexts(body)
+    case Elem(_, body) => get_nexts(body)
     case Text(content) => Some(content, Nil)
   }
   private def get_nexts(trees: List[Tree]): State = trees match {
@@ -118,7 +118,7 @@
     def cache_string(x: String): String =
       lookup(x) match {
         case Some(y) => y
-        case None => store(x)
+        case None => store(new String(x.toCharArray))  // trim string value
       }
     def cache_props(x: List[(String, String)]): List[(String, String)] =
       if (x.isEmpty) x
@@ -127,14 +127,23 @@
           case Some(y) => y
           case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
         }
+    def cache_markup(x: Markup): Markup =
+      lookup(x) match {
+        case Some(y) => y
+        case None =>
+          x match {
+            case Markup(name, props) =>
+              store(Markup(cache_string(name), cache_props(props)))
+          }
+      }
     def cache_tree(x: XML.Tree): XML.Tree =
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
-            case XML.Elem(name, props, body) =>
-              store(XML.Elem(cache_string(name), cache_props(props), cache_trees(body)))
-            case XML.Text(text) => XML.Text(cache_string(text))
+            case XML.Elem(markup, body) =>
+              store(XML.Elem(cache_markup(markup), cache_trees(body)))
+            case XML.Text(text) => store(XML.Text(cache_string(text)))
           }
       }
     def cache_trees(x: List[XML.Tree]): List[XML.Tree] =
@@ -150,7 +159,7 @@
   /* document object model (W3C DOM) */
 
   def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
-    node.getUserData(Markup.DATA) match {
+    node.getUserData(Markup.Data.name) match {
       case tree: XML.Tree => Some(tree)
       case _ => None
     }
@@ -158,12 +167,12 @@
   def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
   {
     def DOM(tr: Tree): org.w3c.dom.Node = tr match {
-      case Elem(Markup.DATA, Nil, List(data, t)) =>
+      case Elem(Markup.Data, List(data, t)) =>
         val node = DOM(t)
-        node.setUserData(Markup.DATA, data, null)
+        node.setUserData(Markup.Data.name, data, null)
         node
-      case Elem(name, atts, ts) =>
-        if (name == Markup.DATA)
+      case Elem(Markup(name, atts), ts) =>
+        if (name == Markup.Data.name)
           error("Malformed data element: " + tr.toString)
         val node = doc.createElement(name)
         for ((name, value) <- atts) node.setAttribute(name, value)
diff -r b32a44361186 -r ea417f69b36f src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/General/yxml.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -64,7 +64,7 @@
     fun attrib (a, x) =
       Buffer.add Y #>
       Buffer.add a #> Buffer.add "=" #> Buffer.add x;
-    fun tree (XML.Elem (name, atts, ts)) =
+    fun tree (XML.Elem ((name, atts), ts)) =
           Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
           fold tree ts #>
           Buffer.add XYX
@@ -104,7 +104,7 @@
   | push name atts pending = ((name, atts), []) :: pending;
 
 fun pop ((("", _), _) :: _) = err_unbalanced ""
-  | pop (((name, atts), body) :: pending) = add (XML.Elem (name, atts, rev body)) pending;
+  | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
 
 
 (* parsing *)
diff -r b32a44361186 -r ea417f69b36f src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/General/yxml.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -55,7 +55,7 @@
     val s = source.toString
     val i = s.indexOf('=')
     if (i <= 0) err_attribute()
-    (s.substring(0, i).intern, s.substring(i + 1))
+    (s.substring(0, i), s.substring(i + 1))
   }
 
 
@@ -64,7 +64,7 @@
     /* stack operations */
 
     def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
-    var stack: List[((String, XML.Attributes), ListBuffer[XML.Tree])] = List((("", Nil), buffer()))
+    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup("", Nil), buffer()))
 
     def add(x: XML.Tree)
     {
@@ -74,15 +74,16 @@
     def push(name: String, atts: XML.Attributes)
     {
       if (name == "") err_element()
-      else stack = ((name, atts), buffer()) :: stack
+      else stack = (Markup(name, atts), buffer()) :: stack
     }
 
     def pop()
     {
       (stack: @unchecked) match {
-        case ((("", _), _) :: _) => err_unbalanced("")
-        case (((name, atts), body) :: pending) =>
-          stack = pending; add(XML.Elem(name, atts, body.toList))
+        case ((Markup("", _), _) :: _) => err_unbalanced("")
+        case ((markup, body) :: pending) =>
+          stack = pending
+          add(XML.Elem(markup, body.toList))
       }
     }
 
@@ -94,14 +95,14 @@
       else {
         Library.chunks(chunk, Y).toList match {
           case ch :: name :: atts if ch.length == 0 =>
-            push(name.toString.intern, atts.map(parse_attrib))
+            push(name.toString, atts.map(parse_attrib))
           case txts => for (txt <- txts) add(XML.Text(txt.toString))
         }
       }
     }
     stack match {
-      case List((("", _), body)) => body.toList
-      case ((name, _), _) :: _ => err_unbalanced(name)
+      case List((Markup("", _), body)) => body.toList
+      case (Markup(name, _), _) :: _ => err_unbalanced(name)
     }
   }
 
@@ -116,7 +117,7 @@
   /* failsafe parsing */
 
   private def markup_failsafe(source: CharSequence) =
-    XML.Elem (Markup.MALFORMED, Nil,
+    XML.elem (Markup.MALFORMED,
       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
 
   def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
diff -r b32a44361186 -r ea417f69b36f src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -233,7 +233,7 @@
     val _ = define_state state_id' state';
   in (state_id', (id, state_id') :: updates) end;
 
-fun report_updates updates =
+fun updates_status updates =
   implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
   |> Markup.markup Markup.assign
   |> Output.status;
@@ -262,7 +262,7 @@
           |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
 
       val _ = define_document new_id new_document';
-      val _ = report_updates (flat updatess);
+      val _ = updates_status (flat updatess);
       val _ = execute new_document';
     in () end);
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/Isar/isar_document.scala
--- a/src/Pure/Isar/isar_document.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -9,12 +9,12 @@
 
 object Isar_Document
 {
-  /* reports */
+  /* protocol messages */
 
   object Assign {
     def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
       msg match {
-        case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits)
+        case XML.Elem(Markup.Assign, edits) => Some(edits)
         case _ => None
       }
   }
@@ -22,7 +22,7 @@
   object Edit {
     def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
       msg match {
-        case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
+        case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
           Some(cmd_id, state_id)
         case _ => None
       }
diff -r b32a44361186 -r ea417f69b36f src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Isar/keyword.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -44,8 +44,8 @@
   val dest_commands: unit -> string list
   val command_keyword: string -> T option
   val command_tags: string -> string list
-  val keyword_status_reportN: string
-  val report: unit -> unit
+  val keyword_statusN: string
+  val status: unit -> unit
   val keyword: string -> unit
   val command: string -> T -> unit
   val is_diag: string -> bool
@@ -146,27 +146,27 @@
 fun command_tags name = these (Option.map tags_of (command_keyword name));
 
 
-(* reports *)
+(* status *)
 
-val keyword_status_reportN = "keyword_status_report";
+val keyword_statusN = "keyword_status";
 
-fun report_message s =
-  (if print_mode_active keyword_status_reportN then Output.status else writeln) s;
+fun status_message s =
+  (if print_mode_active keyword_statusN then Output.status else writeln) s;
 
-fun report_keyword name =
-  report_message (Markup.markup (Markup.keyword_decl name)
+fun keyword_status name =
+  status_message (Markup.markup (Markup.keyword_decl name)
     ("Outer syntax keyword: " ^ quote name));
 
-fun report_command (name, kind) =
-  report_message (Markup.markup (Markup.command_decl name (kind_of kind))
+fun command_status (name, kind) =
+  status_message (Markup.markup (Markup.command_decl name (kind_of kind))
     ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
 
-fun report () =
+fun status () =
   let val (keywords, commands) = CRITICAL (fn () =>
     (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   in
-    List.app report_keyword keywords;
-    List.app report_command commands
+    List.app keyword_status keywords;
+    List.app command_status commands
   end;
 
 
@@ -174,12 +174,12 @@
 
 fun keyword name =
  (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
-  report_keyword name);
+  keyword_status name);
 
 fun command name kind =
  (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   change_commands (Symtab.update (name, kind));
-  report_command (name, kind));
+  command_status (name, kind));
 
 
 (* command categories *)
diff -r b32a44361186 -r ea417f69b36f src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Isar/keyword.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -50,12 +50,12 @@
   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
 
 
-  /* reports */
+  /* protocol messages */
 
   object Keyword_Decl {
     def unapply(msg: XML.Tree): Option[String] =
       msg match {
-        case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
+        case XML.Elem(Markup(Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) => Some(name)
         case _ => None
       }
   }
@@ -63,7 +63,7 @@
   object Command_Decl {
     def unapply(msg: XML.Tree): Option[(String, String)] =
       msg match {
-        case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
+        case XML.Elem(Markup(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind))), _) =>
           Some((name, kind))
         case _ => None
       }
diff -r b32a44361186 -r ea417f69b36f src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -277,7 +277,7 @@
 
     val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
     val spans = Source.exhaust (Thy_Syntax.span_source toks);
-    val _ = List.app Thy_Syntax.report_span spans;
+    val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
     val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
       |> Par_List.map (prepare_unit commands init) |> flat;
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -1074,8 +1074,7 @@
 local
 
 fun future_terminal_proof proof1 proof2 meths int state =
-  if not (Goal.local_future_enforced ()) andalso
-    int orelse is_relevant state orelse not (Goal.local_future_enabled ())
+  if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
   then proof1 meths state
   else snd (proof2 (fn state' => Goal.fork (fn () => ((), proof1 meths state'))) state);
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -334,7 +334,7 @@
     val (syms, pos) = Syntax.read_token text;
     val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
       handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
-    val _ = Position.report (Markup.tclass c) pos;
+    val _ = Context_Position.report ctxt (Markup.tclass c) pos;
   in c end;
 
 
@@ -469,7 +469,7 @@
     val _ =
       if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
       else ();
-    val _ = Position.report (Markup.const d) pos;
+    val _ = Context_Position.report ctxt (Markup.const d) pos;
   in t end;
 
 in
@@ -480,13 +480,13 @@
     val (c, pos) = token_content text;
   in
     if Syntax.is_tid c then
-     (Position.report Markup.tfree pos;
+     (Context_Position.report ctxt Markup.tfree pos;
       TFree (c, default_sort ctxt (c, ~1)))
     else
       let
         val d = Type.intern_type tsig c;
         val decl = Type.the_decl tsig d;
-        val _ = Position.report (Markup.tycon d) pos;
+        val _ = Context_Position.report ctxt (Markup.tycon d) pos;
         fun err () = error ("Bad type name: " ^ quote d);
         val args =
           (case decl of
@@ -511,7 +511,7 @@
   in
     (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
-        (Position.report (Markup.name x
+        (Context_Position.report ctxt (Markup.name x
             (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
           Free (x, infer_type ctxt (x, ty)))
     | _ => prep_const_proper ctxt strict (c, pos))
@@ -738,14 +738,14 @@
 
 fun parse_sort ctxt text =
   let
-    val (syms, pos) = Syntax.parse_token Markup.sort text;
+    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
     val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
       handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos)
   in Type.minimize_sort (tsig_of ctxt) S end;
 
 fun parse_typ ctxt text =
   let
-    val (syms, pos) = Syntax.parse_token Markup.typ text;
+    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
     val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
       handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
   in T end;
@@ -756,7 +756,7 @@
 
     val (T', _) = Type_Infer.paramify_dummies T 0;
     val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
-    val (syms, pos) = Syntax.parse_token markup text;
+    val (syms, pos) = Syntax.parse_token ctxt markup text;
 
     fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
       handle ERROR msg => SOME msg;
@@ -977,7 +977,7 @@
           if name = "" then [Thm.transfer thy Drule.dummy_thm]
           else
             (case Facts.lookup (Context.Proof ctxt) local_facts name of
-              SOME (_, ths) => (Position.report (Markup.local_fact name) pos;
+              SOME (_, ths) => (Context_Position.report ctxt (Markup.local_fact name) pos;
                 map (Thm.transfer thy) (Facts.select thmref ths))
             | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
       in pick name thms end;
@@ -1007,7 +1007,7 @@
   let
     val pos = Binding.pos_of b;
     val name = full_name ctxt b;
-    val _ = Context_Position.report_visible ctxt (Markup.local_fact_decl name) pos;
+    val _ = Context_Position.report ctxt (Markup.local_fact_decl name) pos;
 
     val facts = PureThy.name_thmss false name raw_facts;
     fun app (th, attrs) x =
@@ -1186,7 +1186,7 @@
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
       |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed));
     val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
-      Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
+      Context_Position.report ctxt (Markup.fixed_decl x') (Binding.pos_of b));
   in (xs', ctxt'') end;
 
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Isar/token.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -181,7 +181,7 @@
 (* token content *)
 
 fun source_of (Token ((source, (pos, _)), _, _)) =
-  YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
+  YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
 
 fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -571,7 +571,7 @@
   if print then
     ignore
       (Future.fork (fn () =>
-          setmp_thread_position tr (fn () => Future.report (fn () => print_state false st)) ()))
+          setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
   else ();
 
 fun error_msg tr exn_info =
diff -r b32a44361186 -r ea417f69b36f src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -22,7 +22,7 @@
       endLine = end_line, endPosition = end_offset} = loc;
     val loc_props =
       (case YXML.parse text of
-        XML.Elem (e, atts, _) => if e = Markup.positionN then atts else []
+        XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
       | XML.Text s => Position.file_name s);
   in
     Position.value Markup.lineN line @
diff -r b32a44361186 -r ea417f69b36f src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -105,7 +105,7 @@
   let val ((name, _), pos) = Args.dest_src src in
     (case Symtab.lookup (! global_parsers) name of
       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
-    | SOME scan => (Position.report (Markup.ML_antiq name) pos;
+    | SOME scan => (Context_Position.report ctxt (Markup.ML_antiq name) pos;
         Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
   end;
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/PIDE/change.scala
--- a/src/Pure/PIDE/change.scala	Mon Aug 09 11:38:32 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-/*  Title:      Pure/PIDE/change.scala
-    Author:     Fabian Immler, TU Munich
-    Author:     Makarius
-
-Changes of plain text, resulting in document edits.
-*/
-
-package isabelle
-
-
-object Change
-{
-  val init = new Change(Document.NO_ID, None, Nil, Future.value(Nil, Document.init))
-
-  abstract class Snapshot
-  {
-    val document: Document
-    val node: Document.Node
-    val is_outdated: Boolean
-    def convert(offset: Int): Int
-    def revert(offset: Int): Int
-  }
-}
-
-class Change(
-  val id: Document.Version_ID,
-  val parent: Option[Change],
-  val edits: List[Document.Node_Text_Edit],
-  val result: Future[(List[Document.Edit[Command]], Document)])
-{
-  /* ancestor versions */
-
-  def ancestors: Iterator[Change] = new Iterator[Change]
-  {
-    private var state: Option[Change] = Some(Change.this)
-    def hasNext = state.isDefined
-    def next =
-      state match {
-        case Some(change) => state = change.parent; change
-        case None => throw new NoSuchElementException("next on empty iterator")
-      }
-  }
-
-
-  /* editing and state assignment */
-
-  def edit(session: Session, edits: List[Document.Node_Text_Edit]): Change =
-  {
-    val new_id = session.create_id()
-    val result: Future[(List[Document.Edit[Command]], Document)] =
-      Future.fork {
-        val old_doc = join_document
-        old_doc.await_assignment
-        Document.text_edits(session, old_doc, new_id, edits)
-      }
-    new Change(new_id, Some(this), edits, result)
-  }
-
-  def join_document: Document = result.join._2
-  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
-
-
-  /* snapshot */
-
-  def snapshot(name: String, extra_edits: List[Text_Edit]): Change.Snapshot =
-  {
-    val latest = this
-    val stable = latest.ancestors.find(_.is_assigned)
-    require(stable.isDefined)
-
-    val edits =
-      (extra_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
-          (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
-    lazy val reverse_edits = edits.reverse
-
-    new Change.Snapshot {
-      val document = stable.get.join_document
-      val node = document.nodes(name)
-      val is_outdated = !(extra_edits.isEmpty && latest == stable.get)
-      def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
-      def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
-    }
-  }
-}
\ No newline at end of file
diff -r b32a44361186 -r ea417f69b36f src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -37,7 +37,7 @@
 class Command(
     val id: Document.Command_ID,
     val span: Thy_Syntax.Span,
-    val static_parent: Option[Command] = None)
+    val static_parent: Option[Command] = None)  // FIXME !?
   extends Session.Entity
 {
   /* classification */
diff -r b32a44361186 -r ea417f69b36f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -14,33 +14,31 @@
 
 object Document
 {
-  /* unique identifiers */
+  /* formal identifiers */
 
+  type Version_ID = String
+  type Command_ID = String
   type State_ID = String
-  type Command_ID = String
-  type Version_ID = String
 
   val NO_ID = ""
 
 
-  /* command start positions */
 
-  def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
-  {
-    var i = offset
-    for (command <- commands) yield {
-      val start = i
-      i += command.length
-      (command, start)
-    }
-  }
-
-
-  /* named document nodes */
+  /** named document nodes **/
 
   object Node
   {
     val empty: Node = new Node(Linear_Set())
+
+    def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
+    {
+      var i = offset
+      for (command <- commands) yield {
+        val start = i
+        i += command.length
+        (command, start)
+      }
+    }
   }
 
   class Node(val commands: Linear_Set[Command])
@@ -48,7 +46,7 @@
     /* command ranges */
 
     def command_starts: Iterator[(Command, Int)] =
-      Document.command_starts(commands.iterator)
+      Node.command_starts(commands.iterator)
 
     def command_start(cmd: Command): Option[Int] =
       command_starts.find(_._1 == cmd).map(_._2)
@@ -85,7 +83,7 @@
 
 
 
-  /** editing **/
+  /** changes of plain text, eventually resulting in document edits **/
 
   type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
 
@@ -93,6 +91,65 @@
    (String,  // node name
     Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
 
+  abstract class Snapshot
+  {
+    val document: Document
+    val node: Document.Node
+    val is_outdated: Boolean
+    def convert(offset: Int): Int
+    def revert(offset: Int): Int
+  }
+
+  object Change
+  {
+    val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init))
+  }
+
+  class Change(
+    val id: Version_ID,
+    val parent: Option[Change],
+    val edits: List[Node_Text_Edit],
+    val result: Future[(List[Edit[Command]], Document)])
+  {
+    def ancestors: Iterator[Change] = new Iterator[Change]
+    {
+      private var state: Option[Change] = Some(Change.this)
+      def hasNext = state.isDefined
+      def next =
+        state match {
+          case Some(change) => state = change.parent; change
+          case None => throw new NoSuchElementException("next on empty iterator")
+        }
+    }
+
+    def join_document: Document = result.join._2
+    def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
+
+    def snapshot(name: String, pending_edits: List[Text_Edit]): Snapshot =
+    {
+      val latest = Change.this
+      val stable = latest.ancestors.find(_.is_assigned)
+      require(stable.isDefined)
+
+      val edits =
+        (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
+            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+      lazy val reverse_edits = edits.reverse
+
+      new Snapshot {
+        val document = stable.get.join_document
+        val node = document.nodes(name)
+        val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
+        def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
+        def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+      }
+    }
+  }
+
+
+
+  /** editing **/
+
   def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
       edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
   {
@@ -102,9 +159,9 @@
     /* unparsed dummy commands */
 
     def unparsed(source: String) =
-      new Command(null, List(Token(Token.Kind.UNPARSED, source)))
+      new Command(NO_ID, List(Token(Token.Kind.UNPARSED, source)))
 
-    def is_unparsed(command: Command) = command.id == null
+    def is_unparsed(command: Command) = command.id == NO_ID
 
 
     /* phase 1: edit individual command source */
@@ -114,7 +171,7 @@
     {
       eds match {
         case e :: es =>
-          command_starts(commands.iterator).find {
+          Node.command_starts(commands.iterator).find {
             case (cmd, cmd_start) =>
               e.can_edit(cmd.source, cmd_start) ||
                 e.is_insert && e.start == cmd_start + cmd.length
@@ -182,7 +239,7 @@
       for ((name, text_edits) <- edits) {
         val commands0 = nodes(name).commands
         val commands1 = edit_text(text_edits, commands0)
-        val commands2 = parse_spans(commands1)
+        val commands2 = parse_spans(commands1)   // FIXME somewhat slow
 
         val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
         val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
diff -r b32a44361186 -r ea417f69b36f src/Pure/PIDE/state.scala
--- a/src/Pure/PIDE/state.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -2,7 +2,7 @@
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
-Accumulating results from prover.
+Accumulated results from prover.
 */
 
 package isabelle
@@ -76,15 +76,21 @@
 
   def accumulate(message: XML.Tree): State =
     message match {
-      case XML.Elem(Markup.STATUS, _, elems) =>
+      case XML.Elem(Markup(Markup.STATUS, _), elems) =>
         (this /: elems)((state, elem) =>
           elem match {
-            case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
-            case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
-            case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
-            case XML.Elem(Markup.FORKED, _, _) => state.add_forks(1)
-            case XML.Elem(Markup.JOINED, _, _) => state.add_forks(-1)
-            case XML.Elem(kind, atts, body) if Position.get_id(atts) == Some(command.id) =>
+            case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
+            case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
+            case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
+            case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
+            case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
+            case _ => System.err.println("Ignored status message: " + elem); state
+          })
+
+      case XML.Elem(Markup(Markup.REPORT, _), elems) =>
+        (this /: elems)((state, elem) =>
+          elem match {
+            case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
               atts match {
                 case Position.Range(begin, end) =>
                   if (kind == Markup.ML_TYPING) {
@@ -94,7 +100,7 @@
                   }
                   else if (kind == Markup.ML_REF) {
                     body match {
-                      case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
+                      case List(XML.Elem(Markup(Markup.ML_DEF, atts), _)) =>
                         state.add_markup(command.markup_node(
                           begin - 1, end - 1,
                           Command.RefInfo(
@@ -112,9 +118,7 @@
                   }
                 case _ => state
               }
-            case _ =>
-              System.err.println("Ignored status report: " + elem)
-              state
+            case _ => System.err.println("Ignored report message: " + elem); state
           })
       case _ => add_result(message)
     }
diff -r b32a44361186 -r ea417f69b36f src/Pure/ProofGeneral/pgip_input.ML
--- a/src/Pure/ProofGeneral/pgip_input.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_input.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -62,7 +62,7 @@
     (* unofficial escape command for debugging *)
     | Quitpgip       of { }
 
-    val input: string * XML.attributes * XML.tree list -> pgipinput option  (* raises PGIP *)
+    val input: Markup.T * XML.tree list -> pgipinput option  (* raises PGIP *)
 end
 
 structure PgipInput : PGIPINPUT = 
@@ -161,7 +161,7 @@
    Raise PGIP exception for invalid data.
    Return NONE for unknown/unhandled commands. 
 *)
-fun input (elem, attrs, data) =
+fun input ((elem, attrs), data) =
 SOME 
  (case elem of 
      "askpgip"        => Askpgip { }
diff -r b32a44361186 -r ea417f69b36f src/Pure/ProofGeneral/pgip_markup.ML
--- a/src/Pure/ProofGeneral/pgip_markup.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_markup.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -75,81 +75,81 @@
        case docelt of
 
            Openblock vs  =>
-           XML.Elem("openblock", opt_attr "name" (#metavarid vs) @
-                                 opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
-                                 opt_attr "metavarid" (#metavarid vs),
+           XML.Elem(("openblock", opt_attr "name" (#metavarid vs) @
+                                  opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
+                                  opt_attr "metavarid" (#metavarid vs)),
                     [])
 
          | Closeblock _ =>
-           XML.Elem("closeblock", [], [])
+           XML.Elem(("closeblock", []), [])
 
          | Opentheory vs  =>
-           XML.Elem("opentheory",
+           XML.Elem(("opentheory",
                     opt_attr "thyname" (#thyname vs) @
                     opt_attr "parentnames"
                              (case (#parentnames vs)
                                of [] => NONE
-                                | ps => SOME (space_implode ";" ps)),
+                                | ps => SOME (space_implode ";" ps))),
                     [XML.Text (#text vs)])
 
          | Theoryitem vs =>
-           XML.Elem("theoryitem",
+           XML.Elem(("theoryitem",
                     opt_attr "name" (#name vs) @
-                    opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs),
+                    opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs)),
                     [XML.Text (#text vs)])
 
          | Closetheory vs =>
-           XML.Elem("closetheory", [], [XML.Text (#text vs)])
+           XML.Elem(("closetheory", []), [XML.Text (#text vs)])
 
          | Opengoal vs =>
-           XML.Elem("opengoal",
-                    opt_attr "thmname" (#thmname vs),
+           XML.Elem(("opengoal",
+                    opt_attr "thmname" (#thmname vs)),
                     [XML.Text (#text vs)])
 
          | Proofstep vs =>
-           XML.Elem("proofstep", [], [XML.Text (#text vs)])
+           XML.Elem(("proofstep", []), [XML.Text (#text vs)])
 
          | Closegoal vs =>
-           XML.Elem("closegoal", [], [XML.Text (#text vs)])
+           XML.Elem(("closegoal", []), [XML.Text (#text vs)])
 
          | Giveupgoal vs =>
-           XML.Elem("giveupgoal", [], [XML.Text (#text vs)])
+           XML.Elem(("giveupgoal", []), [XML.Text (#text vs)])
 
          | Postponegoal vs =>
-           XML.Elem("postponegoal", [], [XML.Text (#text vs)])
+           XML.Elem(("postponegoal", []), [XML.Text (#text vs)])
 
          | Comment vs =>
-           XML.Elem("comment", [], [XML.Text (#text vs)])
+           XML.Elem(("comment", []), [XML.Text (#text vs)])
 
          | Whitespace vs =>
-           XML.Elem("whitespace", [], [XML.Text (#text vs)])
+           XML.Elem(("whitespace", []), [XML.Text (#text vs)])
 
          | Doccomment vs =>
-           XML.Elem("doccomment", [], [XML.Text (#text vs)])
+           XML.Elem(("doccomment", []), [XML.Text (#text vs)])
 
          | Spuriouscmd vs =>
-           XML.Elem("spuriouscmd", [], [XML.Text (#text vs)])
+           XML.Elem(("spuriouscmd", []), [XML.Text (#text vs)])
 
          | Badcmd vs =>
-           XML.Elem("badcmd", [], [XML.Text (#text vs)])
+           XML.Elem(("badcmd", []), [XML.Text (#text vs)])
 
          | Unparseable vs =>
-           XML.Elem("unparseable", [], [XML.Text (#text vs)])
+           XML.Elem(("unparseable", []), [XML.Text (#text vs)])
 
          | Metainfo vs =>
-           XML.Elem("metainfo", opt_attr "name" (#name vs),
+           XML.Elem(("metainfo", opt_attr "name" (#name vs)),
                     [XML.Text (#text vs)])
 
          | Litcomment vs =>
-           XML.Elem("litcomment", opt_attr "format" (#format vs),
+           XML.Elem(("litcomment", opt_attr "format" (#format vs)),
                    #content vs)
 
          | Showcode vs =>
-           XML.Elem("showcode",
-                    attr "show" (PgipTypes.bool_to_pgstring (#show vs)), [])
+           XML.Elem(("showcode",
+                    attr "show" (PgipTypes.bool_to_pgstring (#show vs))), [])
 
          | Setformat vs =>
-           XML.Elem("setformat", attr "format" (#format vs), [])
+           XML.Elem(("setformat", attr "format" (#format vs)), [])
 
    val output_doc = map xml_of
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/ProofGeneral/pgip_output.ML
--- a/src/Pure/ProofGeneral/pgip_output.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_output.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -117,9 +117,7 @@
     let 
         val content = #content vs
     in
-        XML.Elem ("normalresponse", 
-                  [],
-                  content)
+        XML.Elem (("normalresponse", []), content)
     end
 
 fun errorresponse (Errorresponse vs) =
@@ -128,9 +126,9 @@
         val location = #location vs
         val content = #content vs
     in
-        XML.Elem ("errorresponse",
+        XML.Elem (("errorresponse",
                  attrs_of_fatality fatality @
-                 these (Option.map attrs_of_location location),
+                 these (Option.map attrs_of_location location)),
                  content)
     end
 
@@ -139,9 +137,9 @@
         val url = #url vs
         val completed = #completed vs
     in
-        XML.Elem ("informfileloaded", 
+        XML.Elem (("informfileloaded", 
                   attrs_of_pgipurl url @ 
-                  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
+                  (attr "completed" (PgipTypes.bool_to_pgstring completed))),
                   [])
     end
 
@@ -150,9 +148,9 @@
         val url = #url vs
         val completed = #completed vs
     in
-        XML.Elem ("informfileoutdated", 
+        XML.Elem (("informfileoutdated", 
                   attrs_of_pgipurl url @ 
-                  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
+                  (attr "completed" (PgipTypes.bool_to_pgstring completed))),
                   [])
     end
 
@@ -161,9 +159,9 @@
         val url = #url vs
         val completed = #completed vs
     in
-        XML.Elem ("informfileretracted", 
+        XML.Elem (("informfileretracted", 
                   attrs_of_pgipurl url @ 
-                  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
+                  (attr "completed" (PgipTypes.bool_to_pgstring completed))),
                   [])
     end
 
@@ -172,14 +170,14 @@
         val attrs = #attrs vs
         val content = #content vs
     in
-        XML.Elem ("metainforesponse", attrs, content)
+        XML.Elem (("metainforesponse", attrs), content)
     end
 
 fun lexicalstructure (Lexicalstructure vs) =
     let
         val content = #content vs
     in
-        XML.Elem ("lexicalstructure", [], content)
+        XML.Elem (("lexicalstructure", []), content)
     end
 
 fun proverinfo (Proverinfo vs) =
@@ -191,13 +189,13 @@
         val url = #url vs
         val filenameextns = #filenameextns vs
     in 
-        XML.Elem ("proverinfo",
+        XML.Elem (("proverinfo",
                  [("name", name),
                   ("version", version),
                   ("instance", instance), 
                   ("descr", descr),
                   ("url", Url.implode url),
-                  ("filenameextns", filenameextns)],
+                  ("filenameextns", filenameextns)]),
                  [])
     end
 
@@ -205,7 +203,7 @@
     let
         val idtables = #idtables vs
     in
-        XML.Elem ("setids",[],map idtable_to_xml idtables)
+        XML.Elem (("setids", []), map idtable_to_xml idtables)
     end
 
 fun setrefs (Setrefs vs) =
@@ -216,13 +214,13 @@
         val name = #name vs
         val idtables = #idtables vs
         val fileurls = #fileurls vs
-        fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
+        fun fileurl_to_xml url = XML.Elem (("fileurl", attrs_of_pgipurl url), [])
     in
-        XML.Elem ("setrefs",
+        XML.Elem (("setrefs",
                   (the_default [] (Option.map attrs_of_pgipurl url)) @ 
                   (the_default [] (Option.map attrs_of_objtype objtype)) @
                   (opt_attr "thyname" thyname) @
-                  (opt_attr "name" name),
+                  (opt_attr "name" name)),
                   (map idtable_to_xml idtables) @ 
                   (map fileurl_to_xml fileurls))
     end
@@ -231,14 +229,14 @@
     let
         val idtables = #idtables vs
     in
-        XML.Elem ("addids",[],map idtable_to_xml idtables)
+        XML.Elem (("addids", []), map idtable_to_xml idtables)
     end
 
 fun delids (Delids vs) =
     let
         val idtables = #idtables vs
     in
-        XML.Elem ("delids",[],map idtable_to_xml idtables)
+        XML.Elem (("delids", []), map idtable_to_xml idtables)
     end
 
 fun hasprefs (Hasprefs vs) =
@@ -246,7 +244,7 @@
       val prefcategory = #prefcategory vs
       val prefs = #prefs vs
   in 
-      XML.Elem("hasprefs",opt_attr "prefcategory" prefcategory, map haspref prefs)
+      XML.Elem (("hasprefs", opt_attr "prefcategory" prefcategory), map haspref prefs)
   end
 
 fun prefval (Prefval vs) =
@@ -254,7 +252,7 @@
         val name = #name vs
         val value = #value vs
     in
-        XML.Elem("prefval", attr "name" name, [XML.Text value])
+        XML.Elem (("prefval", attr "name" name), [XML.Text value])
     end 
 
 fun idvalue (Idvalue vs) =
@@ -264,10 +262,10 @@
         val name = #name vs
         val text = #text vs
     in
-        XML.Elem("idvalue", 
+        XML.Elem (("idvalue", 
                  objtype_attrs @
                  (opt_attr "thyname" thyname) @
-                 (attr "name" name),
+                 attr "name" name),
                  text)
     end
 
@@ -278,7 +276,7 @@
       val theorem = #theorem vs
       val proofpos = #proofpos vs
 
-      fun elto nm attrfn xo = case xo of NONE=>[] | SOME x=>[XML.Elem(nm,attrfn x,[])]
+      fun elto nm attrfn xo = case xo of NONE => [] | SOME x => [XML.Elem ((nm, attrfn x), [])]
 
       val guisefile = elto "guisefile" attrs_of_pgipurl file
       val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
@@ -286,7 +284,7 @@
                             (fn thm=>(attr "thmname" thm) @
                                      (opt_attr "proofpos" (Option.map Int.toString proofpos))) theorem
   in 
-      XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
+      XML.Elem (("informguise", []), guisefile @ guisetheory @ guiseproof)
   end
 
 fun parseresult (Parseresult vs) =
@@ -296,7 +294,7 @@
         val errs = #errs vs
         val xmldoc = PgipMarkup.output_doc doc
     in 
-        XML.Elem("parseresult", attrs, errs @ xmldoc)
+        XML.Elem (("parseresult", attrs), errs @ xmldoc)
     end
 
 fun acceptedpgipelems (Usespgip vs) = 
@@ -305,11 +303,10 @@
         fun async_attrs b = if b then attr "async" "true" else []
         fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs)
         fun singlepgipelem (e,async,attrs) = 
-            XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[XML.Text e])
+            XML.Elem (("pgipelem", async_attrs async @ attrs_attrs attrs), [XML.Text e])
                                                       
     in
-        XML.Elem ("acceptedpgipelems", [],
-                 map singlepgipelem pgipelems)
+        XML.Elem (("acceptedpgipelems", []), map singlepgipelem pgipelems)
     end
 
 fun usespgip (Usespgip vs) =
@@ -317,14 +314,14 @@
         val version = #version vs
         val acceptedelems = acceptedpgipelems (Usespgip vs)
     in 
-        XML.Elem("usespgip", attr "version" version, [acceptedelems])
+        XML.Elem (("usespgip", attr "version" version), [acceptedelems])
     end
 
 fun usespgml (Usespgml vs) =
     let
         val version = #version vs
     in 
-        XML.Elem("usespgml", attr "version" version, [])
+        XML.Elem (("usespgml", attr "version" version), [])
     end
 
 fun pgip (Pgip vs) =
@@ -338,18 +335,18 @@
         val refseq = #refseq vs
         val content = #content vs
     in
-        XML.Elem("pgip",
+        XML.Elem(("pgip",
                  opt_attr "tag" tag @
                  attr "id" id @
                  opt_attr "destid" destid @
                  attr "class" class @
                  opt_attr "refid" refid @
                  opt_attr_map string_of_int "refseq" refseq @
-                 attr "seq" (string_of_int seq),
+                 attr "seq" (string_of_int seq)),
                  content)
     end
 
-fun ready (Ready _) = XML.Elem("ready",[],[])
+fun ready (Ready _) = XML.Elem (("ready", []), [])
 
 
 fun output pgipoutput = case pgipoutput of
diff -r b32a44361186 -r ea417f69b36f src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -168,11 +168,9 @@
     let 
         val objtype_attrs = attrs_of_objtype objtype
         val context_attrs = opt_attr "context" context
-        val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
+        val ids_content = map (fn x => XML.Elem(("identifier", []), [XML.Text x])) ids
     in 
-        XML.Elem ("idtable",
-                  objtype_attrs @ context_attrs,
-                  ids_content)
+        XML.Elem (("idtable", objtype_attrs @ context_attrs), ids_content)
     end
 
 
@@ -282,7 +280,7 @@
                           Pgipchoice ds => map destpgipdtype ds
                         | _ => []
     in 
-        XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
+        XML.Elem ((elt, desc_attr @ attrs), map pgipdtype_to_xml typargs)
     end
 
 val pgiptype_to_xml = pgipdtype_to_xml o pair NONE
@@ -424,10 +422,10 @@
                     pgiptype: pgiptype }
 
 fun haspref ({ name, descr, default, pgiptype}:preference) = 
-    XML.Elem ("haspref",
+    XML.Elem (("haspref",
               attr "name" name @
               opt_attr "descr" descr @
-              opt_attr "default" default,
+              opt_attr "default" default),
               [pgiptype_to_xml pgiptype])
 
 end
diff -r b32a44361186 -r ea417f69b36f src/Pure/ProofGeneral/pgml.ML
--- a/src/Pure/ProofGeneral/pgml.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -109,25 +109,25 @@
 
     (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle;
        would be better not to *)  (* FIXME !??? *)
-    fun atom_to_xml (Sym {name, content}) = XML.Elem ("sym", attr "name" name, [XML.Text content])
+    fun atom_to_xml (Sym {name, content}) = XML.Elem (("sym", attr "name" name), [XML.Text content])
       | atom_to_xml (Str content) = XML.Text content;
 
     fun pgmlterm_to_xml (Atoms {kind, content}) =
-        XML.Elem("atom", opt_attr "kind" kind, map atom_to_xml content)
+        XML.Elem(("atom", opt_attr "kind" kind), map atom_to_xml content)
 
       | pgmlterm_to_xml (Box {orient, indent, content}) =
-        XML.Elem("box",
+        XML.Elem(("box",
                  opt_attr_map pgmlorient_to_string "orient" orient @
-                 opt_attr_map int_to_pgstring "indent" indent,
+                 opt_attr_map int_to_pgstring "indent" indent),
                  map pgmlterm_to_xml content)
 
       | pgmlterm_to_xml (Break {mandatory, indent}) =
-        XML.Elem("break",
+        XML.Elem(("break",
                  opt_attr_map bool_to_pgstring "mandatory" mandatory @
-                 opt_attr_map int_to_pgstring "indent" indent, [])
+                 opt_attr_map int_to_pgstring "indent" indent), [])
 
       | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
-        XML.Elem("subterm",
+        XML.Elem(("subterm",
                  opt_attr "kind" kind @
                  opt_attr "param" param @
                  opt_attr_map pgmlplace_to_string "place" place @
@@ -135,13 +135,13 @@
                  opt_attr_map pgmldec_to_string "decoration" decoration @
                  opt_attr_map pgmlaction_to_string "action" action @
                  opt_attr "pos" pos @
-                 opt_attr_map string_of_pgipurl "xref" xref,
+                 opt_attr_map string_of_pgipurl "xref" xref),
                  map pgmlterm_to_xml content)
 
       | pgmlterm_to_xml (Alt {kind, content}) =
-        XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
+        XML.Elem(("alt", opt_attr "kind" kind), map pgmlterm_to_xml content)
 
-      | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
+      | pgmlterm_to_xml (Embed xmls) = XML.Elem(("embed", []), xmls)
 
       | pgmlterm_to_xml (Raw xml) = xml
 
@@ -152,9 +152,9 @@
                        content: pgmlterm list }
 
     fun pgml_to_xml (Pgml {version,systemid,area,content}) =
-        XML.Elem("pgml",
+        XML.Elem(("pgml",
                  opt_attr "version" version @
                  opt_attr "systemid" systemid @
-                 the_default [] (Option.map PgipTypes.attrs_of_displayarea area),
+                 the_default [] (Option.map PgipTypes.attrs_of_displayarea area)),
                  map pgmlterm_to_xml content)
 end
diff -r b32a44361186 -r ea417f69b36f src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -33,7 +33,7 @@
 
 fun render_trees ts = fold render_tree ts
 and render_tree (XML.Text s) = Buffer.add s
-  | render_tree (XML.Elem (name, props, ts)) =
+  | render_tree (XML.Elem ((name, props), ts)) =
       let
         val (bg1, en1) =
           if name <> Markup.promptN andalso print_mode_active test_markupN
@@ -78,6 +78,7 @@
 fun setup_messages () =
  (Output.writeln_fn := message "" "" "";
   Output.status_fn := (fn _ => ());
+  Output.report_fn := (fn _ => ());
   Output.priority_fn := message (special "I") (special "J") "";
   Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   Output.debug_fn := message (special "K") (special "L") "+++ ";
diff -r b32a44361186 -r ea417f69b36f src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -105,7 +105,7 @@
 
 in
 
-fun pgml_terms (XML.Elem (name, atts, body)) =
+fun pgml_terms (XML.Elem ((name, atts), body)) =
       if member (op =) token_markups name then
         let val content = pgml_syms (Buffer.content (fold XML.add_content body Buffer.empty))
         in [Pgml.Atoms {kind = SOME name, content = content}] end
@@ -132,7 +132,7 @@
     val body = YXML.parse_body s;
     val area =
       (case body of
-        [XML.Elem (name, _, _)] =>
+        [XML.Elem ((name, _), _)] =>
           if name = Markup.stateN then PgipTypes.Display else default_area
       | _ => default_area);
   in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
@@ -161,6 +161,7 @@
 fun setup_messages () =
  (Output.writeln_fn := (fn s => normalmsg Message s);
   Output.status_fn := (fn _ => ());
+  Output.report_fn := (fn _ => ());
   Output.priority_fn := (fn s => normalmsg Status s);
   Output.tracing_fn := (fn s => normalmsg Tracing s);
   Output.warning_fn := (fn s => errormsg Message Warning s);
@@ -283,8 +284,8 @@
 
 fun thm_deps_message (thms, deps) =
   let
-    val valuethms = XML.Elem ("value", [("name", "thms")], [XML.Text thms]);
-    val valuedeps = XML.Elem ("value", [("name", "deps")], [XML.Text deps]);
+    val valuethms = XML.Elem (("value", [("name", "thms")]), [XML.Text thms]);
+    val valuedeps = XML.Elem (("value", [("name", "deps")]), [XML.Text deps]);
   in
     issue_pgip (Metainforesponse
       {attrs = [("infotype", "isabelle_theorem_dependencies")],
@@ -312,7 +313,7 @@
     let val keywords = Keyword.dest_keywords ()
         val commands = Keyword.dest_commands ()
         fun keyword_elt kind keyword =
-            XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
+            XML.Elem (("keyword", [("word", keyword), ("category", kind)]), [])
         in
             (* Also, note we don't call init_outer_syntax here to add interface commands,
             but they should never appear in scripts anyway so it shouldn't matter *)
@@ -647,8 +648,7 @@
 
         fun idvalue strings =
             issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
-                                  text=[XML.Elem("pgml",[],
-                                                 maps YXML.parse_body strings)] })
+                                  text=[XML.Elem (("pgml", []), maps YXML.parse_body strings)] })
 
         fun strings_of_thm (thy, name) =
           map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
@@ -927,7 +927,7 @@
     (pgip_refid := NONE;
      pgip_refseq := NONE;
      (case xml of
-          XML.Elem ("pgip", attrs, pgips) =>
+          XML.Elem (("pgip", attrs), pgips) =>
           (let
                val class = PgipTypes.get_attr "class" attrs
                val dest  = PgipTypes.get_attr_opt "destid" attrs
diff -r b32a44361186 -r ea417f69b36f src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -65,7 +65,7 @@
   val tvarT: typ
   val terminals: string list
   val is_terminal: string -> bool
-  val report_token: token -> unit
+  val report_token: Proof.context -> token -> unit
   val matching_tokens: token * token -> bool
   val valued_token: token -> bool
   val predef_term: string -> token option
@@ -185,8 +185,8 @@
   | Comment     => Markup.inner_comment
   | EOF         => Markup.none;
 
-fun report_token (Token (kind, _, (pos, _))) =
-  Position.report (token_kind_markup kind) pos;
+fun report_token ctxt (Token (kind, _, (pos, _))) =
+  Context_Position.report ctxt (token_kind_markup kind) pos;
 
 
 (* matching_tokens *)
diff -r b32a44361186 -r ea417f69b36f src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -80,7 +80,7 @@
     (string * string) trrule list -> syntax -> syntax
   val update_trrules_i: ast trrule list -> syntax -> syntax
   val remove_trrules_i: ast trrule list -> syntax -> syntax
-  val parse_token: Markup.T -> string -> Symbol_Pos.T list * Position.T
+  val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T
   val parse_sort: Proof.context -> string -> sort
   val parse_typ: Proof.context -> string -> typ
   val parse_term: Proof.context -> string -> term
@@ -458,12 +458,15 @@
 (* read token -- with optional YXML encoding of position *)
 
 fun read_token str =
-  let val (text, pos) =
-    (case YXML.parse str handle Fail msg => error msg of
-      XML.Elem ("token", props, [XML.Text text]) => (text, Position.of_properties props)
-    | XML.Elem ("token", props, []) => ("", Position.of_properties props)
-    | XML.Text text => (text, Position.none)
-    | _ => (str, Position.none))
+  let
+    val tree = YXML.parse str handle Fail msg => error msg;
+    val text = Buffer.empty |> XML.add_content tree |> Buffer.content;
+    val pos =
+      (case tree of
+        XML.Elem ((name, props), _) =>
+          if name = Markup.tokenN then Position.of_properties props
+          else Position.none
+      | XML.Text _ => Position.none);
   in (Symbol_Pos.explode (text, pos), pos) end;
 
 
@@ -479,7 +482,7 @@
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
     val toks = Lexicon.tokenize lexicon xids syms;
-    val _ = List.app Lexicon.report_token toks;
+    val _ = List.app (Lexicon.report_token ctxt) toks;
 
     val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
     val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
@@ -691,10 +694,10 @@
 
 (* (un)parsing *)
 
-fun parse_token markup str =
+fun parse_token ctxt markup str =
   let
     val (syms, pos) = read_token str;
-    val _ = Position.report markup pos;
+    val _ = Context_Position.report ctxt markup pos;
   in (syms, pos) end;
 
 local
diff -r b32a44361186 -r ea417f69b36f src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -34,7 +34,7 @@
 fun message _ _ _ "" = ()
   | message out_stream ch props body =
       let
-        val header = YXML.string_of (XML.Elem (ch, map (pairself YXML.binary_text) props, []));
+        val header = YXML.string_of (XML.Elem ((ch, map (pairself YXML.binary_text) props), []));
         val msg = Symbol.STX ^ chunk header ^ chunk body;
       in TextIO.output (out_stream, msg) (*atomic output*) end;
 
@@ -72,11 +72,12 @@
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
   in
     Output.status_fn   := standard_message out_stream "B";
-    Output.writeln_fn  := standard_message out_stream "C";
-    Output.tracing_fn  := standard_message out_stream "D";
-    Output.warning_fn  := standard_message out_stream "E";
-    Output.error_fn    := standard_message out_stream "F";
-    Output.debug_fn    := standard_message out_stream "G";
+    Output.report_fn   := standard_message out_stream "C";
+    Output.writeln_fn  := standard_message out_stream "D";
+    Output.tracing_fn  := standard_message out_stream "E";
+    Output.warning_fn  := standard_message out_stream "F";
+    Output.error_fn    := standard_message out_stream "G";
+    Output.debug_fn    := standard_message out_stream "H";
     Output.priority_fn := ! Output.writeln_fn;
     Output.prompt_fn   := ignore;
     out_stream
@@ -89,10 +90,10 @@
 
 fun init out =
  (Unsynchronized.change print_mode
-    (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
+    (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
   setup_channels out |> init_message;
   quick_and_dirty := true;  (* FIXME !? *)
-  Keyword.report ();
+  Keyword.status ();
   Output.status (Markup.markup Markup.ready "");
   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -24,11 +24,12 @@
     val markup = Map(
       ('A' : Int) -> Markup.INIT,
       ('B' : Int) -> Markup.STATUS,
-      ('C' : Int) -> Markup.WRITELN,
-      ('D' : Int) -> Markup.TRACING,
-      ('E' : Int) -> Markup.WARNING,
-      ('F' : Int) -> Markup.ERROR,
-      ('G' : Int) -> Markup.DEBUG)
+      ('C' : Int) -> Markup.REPORT,
+      ('D' : Int) -> Markup.WRITELN,
+      ('E' : Int) -> Markup.TRACING,
+      ('F' : Int) -> Markup.WARNING,
+      ('G' : Int) -> Markup.ERROR,
+      ('H' : Int) -> Markup.DEBUG)
     def is_raw(kind: String) =
       kind == Markup.STDOUT
     def is_control(kind: String) =
@@ -45,26 +46,27 @@
 
   class Result(val message: XML.Elem)
   {
-    def kind = message.name
+    def kind = message.markup.name
+    def properties = message.markup.properties
     def body = message.body
 
     def is_raw = Kind.is_raw(kind)
     def is_control = Kind.is_control(kind)
     def is_system = Kind.is_system(kind)
     def is_status = kind == Markup.STATUS
-    def is_ready = is_status && body == List(XML.Elem(Markup.READY, Nil, Nil))
+    def is_report = kind == Markup.REPORT
+    def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
 
     override def toString: String =
     {
       val res =
-        if (is_status) message.body.map(_.toString).mkString
+        if (is_status || is_report) message.body.map(_.toString).mkString
         else Pretty.string_of(message.body)
-      val props = message.attributes
-      if (props.isEmpty)
+      if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"
       else
         kind.toString + " " +
-          (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
+          (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
     }
 
     def cache(c: XML.Cache): Result = new Result(c.cache_tree(message).asInstanceOf[XML.Elem])
@@ -98,7 +100,7 @@
     if (kind == Markup.INIT) {
       for ((Markup.PID, p) <- props) pid = p
     }
-    receiver ! new Result(XML.Elem(kind, props, body))
+    receiver ! new Result(XML.Elem(Markup(kind, props), body))
   }
 
   private def put_result(kind: String, text: String)
@@ -300,7 +302,7 @@
             val header = read_chunk()
             val body = read_chunk()
             header match {
-              case List(XML.Elem(name, props, Nil))
+              case List(XML.Elem(Markup(name, props), Nil))
                   if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
                 put_result(Kind.markup(name(0)), props, body)
               case _ => throw new Protocol_Error("bad header: " + header.toString)
diff -r b32a44361186 -r ea417f69b36f src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/System/session.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -1,5 +1,6 @@
 /*  Title:      Pure/System/session.scala
     Author:     Makarius
+    Options:    :folding=explicit:collapseFolds=1:
 
 Isabelle session, potentially with running prover.
 */
@@ -8,6 +9,7 @@
 
 
 import scala.actors.TIMEOUT
+import scala.actors.Actor
 import scala.actors.Actor._
 
 
@@ -74,7 +76,7 @@
       case _ => None
     }
 
-  private case class Start(timeout: Int, args: List[String])
+  private case class Started(timeout: Int, args: List[String])
   private case object Stop
 
   private lazy val session_actor = actor {
@@ -90,7 +92,8 @@
 
     /* document changes */
 
-    def handle_change(change: Change)
+    def handle_change(change: Document.Change)
+    //{{{
     {
       require(change.parent.isDefined)
 
@@ -120,6 +123,7 @@
       register_document(doc)
       prover.edit_document(change.parent.get.id, doc.id, id_edits)
     }
+    //}}}
 
 
     /* prover results */
@@ -130,10 +134,11 @@
     }
 
     def handle_result(result: Isabelle_Process.Result)
+    //{{{
     {
       raw_results.event(result)
 
-      val target_id: Option[Session.Entity_ID] = Position.get_id(result.message.attributes)
+      val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties)
       val target: Option[Session.Entity] =
         target_id match {
           case None => None
@@ -175,6 +180,7 @@
       else if (!result.is_system)   // FIXME syslog (!?)
         bad_result(result)
     }
+    //}}}
 
 
     /* prover startup */
@@ -222,7 +228,7 @@
 
     loop {
       react {
-        case Start(timeout, args) =>
+        case Started(timeout, args) =>
           if (prover == null) {
             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
             val origin = sender
@@ -238,7 +244,7 @@
             prover = null
           }
 
-        case change: Change if prover != null =>
+        case change: Document.Change if prover != null =>
           handle_change(change)
 
         case result: Isabelle_Process.Result =>
@@ -254,9 +260,11 @@
 
 
 
-  /** buffered command changes -- delay_first discipline **/
+  /** buffered command changes (delay_first discipline) **/
 
-  private lazy val command_change_buffer = actor {
+  private lazy val command_change_buffer = actor
+  //{{{
+  {
     import scala.compat.Platform.currentTime
 
     var changed: Set[Command] = Set()
@@ -292,6 +300,7 @@
       }
     }
   }
+  //}}}
 
   def indicate_command_change(command: Command)
   {
@@ -299,11 +308,49 @@
   }
 
 
-  /* main methods */
+
+  /** editor history **/
+
+  private case class Edit_Document(edits: List[Document.Node_Text_Edit])
+
+  private val editor_history = new Actor
+  {
+    @volatile private var history = Document.Change.init
+    def current_change(): Document.Change = history
 
-  def start(timeout: Int, args: List[String]): Option[String] =
-    (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
+    def act
+    {
+      loop {
+        react {
+          case Edit_Document(edits) =>
+            val old_change = history
+            val new_id = create_id()
+            val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
+              isabelle.Future.fork {
+                val old_doc = old_change.join_document
+                old_doc.await_assignment
+                Document.text_edits(Session.this, old_doc, new_id, edits)
+              }
+            val new_change = new Document.Change(new_id, Some(old_change), edits, result)
+            history = new_change
+            new_change.result.map(_ => session_actor ! new_change)
+
+          case bad => System.err.println("editor_model: ignoring bad message " + bad)
+        }
+      }
+    }
+  }
+  editor_history.start
+
+
+
+  /** 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 input(change: Change) { session_actor ! change }
+
+  def current_change(): Document.Change = editor_history.current_change()
+  def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history ! Edit_Document(edits) }
 }
diff -r b32a44361186 -r ea417f69b36f src/Pure/System/swing_thread.scala
--- a/src/Pure/System/swing_thread.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/System/swing_thread.scala	Mon Aug 09 11:45:30 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)
 
diff -r b32a44361186 -r ea417f69b36f src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Thy/html.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -42,7 +42,7 @@
   // document markup
 
   def span(cls: String, body: List[XML.Tree]): XML.Elem =
-    XML.Elem(SPAN, List((CLASS, cls)), body)
+    XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
 
   def hidden(txt: String): XML.Elem =
     span(Markup.HIDDEN, List(XML.Text(txt)))
@@ -52,8 +52,8 @@
 
   def spans(tree: XML.Tree): List[XML.Tree] =
     tree match {
-      case XML.Elem(name, _, ts) =>
-        List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
+      case XML.Elem(Markup(name, _), ts) =>
+        List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(spans)))))
       case XML.Text(txt) =>
         val ts = new ListBuffer[XML.Tree]
         val t = new StringBuilder
diff -r b32a44361186 -r ea417f69b36f src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -7,30 +7,29 @@
 package isabelle
 
 
+import scala.collection.mutable
+
+
 object Thy_Syntax
 {
-  private val parser = new Parse.Parser
-  {
-    override def filter_proper = false
-
-    val command_span: Parser[Span] =
-    {
-      val whitespace = token("white space", _.is_ignored)
-      val command = token("command keyword", _.is_command)
-      val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
-      command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
-    }
-  }
-
   type Span = List[Token]
 
   def parse_spans(toks: List[Token]): List[Span] =
   {
-    import parser._
+    val result = new mutable.ListBuffer[Span]
+    val span = new mutable.ListBuffer[Token]
+    val whitespace = new mutable.ListBuffer[Token]
 
-    parse(rep(command_span), Token.reader(toks)) match {
-      case Success(spans, rest) if rest.atEnd => spans
-      case bad => error(bad.toString)
+    def flush(buffer: mutable.ListBuffer[Token])
+    {
+      if (!buffer.isEmpty) { result += buffer.toList; buffer.clear }
     }
+    for (tok <- toks) {
+      if (tok.is_command) { flush(span); flush(whitespace); span += tok }
+      else if (tok.is_ignored) whitespace += tok
+      else { span ++= whitespace; whitespace.clear; span += tok }
+    }
+    flush(span); flush(whitespace)
+    result.toList
   }
 }
diff -r b32a44361186 -r ea417f69b36f src/Pure/Tools/xml_syntax.ML
--- a/src/Pure/Tools/xml_syntax.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/Tools/xml_syntax.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -22,148 +22,150 @@
 
 (**** XML output ****)
 
-fun xml_of_class name = XML.Elem ("class", [("name", name)], []);
+fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
 
-fun xml_of_type (TVar ((s, i), S)) = XML.Elem ("TVar",
-      ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
-      map xml_of_class S)
+fun xml_of_type (TVar ((s, i), S)) =
+      XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
+        map xml_of_class S)
   | xml_of_type (TFree (s, S)) =
-      XML.Elem ("TFree", [("name", s)], map xml_of_class S)
+      XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
   | xml_of_type (Type (s, Ts)) =
-      XML.Elem ("Type", [("name", s)], map xml_of_type Ts);
+      XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
 
 fun xml_of_term (Bound i) =
-      XML.Elem ("Bound", [("index", string_of_int i)], [])
+      XML.Elem (("Bound", [("index", string_of_int i)]), [])
   | xml_of_term (Free (s, T)) =
-      XML.Elem ("Free", [("name", s)], [xml_of_type T])
-  | xml_of_term (Var ((s, i), T)) = XML.Elem ("Var",
-      ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
-      [xml_of_type T])
+      XML.Elem (("Free", [("name", s)]), [xml_of_type T])
+  | xml_of_term (Var ((s, i), T)) =
+      XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
+        [xml_of_type T])
   | xml_of_term (Const (s, T)) =
-      XML.Elem ("Const", [("name", s)], [xml_of_type T])
+      XML.Elem (("Const", [("name", s)]), [xml_of_type T])
   | xml_of_term (t $ u) =
-      XML.Elem ("App", [], [xml_of_term t, xml_of_term u])
+      XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
   | xml_of_term (Abs (s, T, t)) =
-      XML.Elem ("Abs", [("vname", s)], [xml_of_type T, xml_of_term t]);
+      XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
 
 fun xml_of_opttypes NONE = []
-  | xml_of_opttypes (SOME Ts) = [XML.Elem ("types", [], map xml_of_type Ts)];
+  | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
 
 (* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
 (* it can be looked up in the theorem database. Thus, it could be      *)
 (* omitted from the xml representation.                                *)
 
+(* FIXME not exhaustive *)
 fun xml_of_proof (PBound i) =
-      XML.Elem ("PBound", [("index", string_of_int i)], [])
+      XML.Elem (("PBound", [("index", string_of_int i)]), [])
   | xml_of_proof (Abst (s, optT, prf)) =
-      XML.Elem ("Abst", [("vname", s)],
-        (case optT of NONE => [] | SOME T => [xml_of_type T]) @
-        [xml_of_proof prf])
+      XML.Elem (("Abst", [("vname", s)]),
+        (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
   | xml_of_proof (AbsP (s, optt, prf)) =
-      XML.Elem ("AbsP", [("vname", s)],
-        (case optt of NONE => [] | SOME t => [xml_of_term t]) @
-        [xml_of_proof prf])
+      XML.Elem (("AbsP", [("vname", s)]),
+        (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
   | xml_of_proof (prf % optt) =
-      XML.Elem ("Appt", [],
-        xml_of_proof prf ::
-        (case optt of NONE => [] | SOME t => [xml_of_term t]))
+      XML.Elem (("Appt", []),
+        xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
   | xml_of_proof (prf %% prf') =
-      XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
-  | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
+      XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
+  | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
   | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
-      XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
+      XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   | xml_of_proof (PAxm (s, t, optTs)) =
-      XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
+      XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   | xml_of_proof (Oracle (s, t, optTs)) =
-      XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
+      XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   | xml_of_proof MinProof =
-      XML.Elem ("MinProof", [], []);
+      XML.Elem (("MinProof", []), []);
+
 
 (* useful for checking the output against a schema file *)
 
 fun write_to_file path elname x =
   File.write path
     ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
-     XML.string_of (XML.Elem (elname,
-       [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
-        ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")],
+     XML.string_of (XML.Elem ((elname,
+         [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
+          ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
        [x])));
 
 
+
 (**** XML input ****)
 
 exception XML of string * XML.tree;
 
-fun class_of_xml (XML.Elem ("class", [("name", name)], [])) = name
+fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
   | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
 
-fun index_of_string s tree idx = (case Int.fromString idx of
-  NONE => raise XML (s ^ ": bad index", tree) | SOME i => i);
+fun index_of_string s tree idx =
+  (case Int.fromString idx of
+    NONE => raise XML (s ^ ": bad index", tree)
+  | SOME i => i);
 
-fun type_of_xml (tree as XML.Elem ("TVar", atts, classes)) = TVar
+fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
       ((case Properties.get atts "name" of
           NONE => raise XML ("type_of_xml: name of TVar missing", tree)
         | SOME name => name,
         the_default 0 (Option.map (index_of_string "type_of_xml" tree)
           (Properties.get atts "index"))),
        map class_of_xml classes)
-  | type_of_xml (XML.Elem ("TFree", [("name", s)], classes)) =
+  | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
       TFree (s, map class_of_xml classes)
-  | type_of_xml (XML.Elem ("Type", [("name", s)], types)) =
+  | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
       Type (s, map type_of_xml types)
   | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
 
-fun term_of_xml (tree as XML.Elem ("Bound", [("index", idx)], [])) =
+fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
       Bound (index_of_string "bad variable index" tree idx)
-  | term_of_xml (XML.Elem ("Free", [("name", s)], [typ])) =
+  | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
       Free (s, type_of_xml typ)
-  | term_of_xml (tree as XML.Elem ("Var", atts, [typ])) = Var
+  | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
       ((case Properties.get atts "name" of
           NONE => raise XML ("type_of_xml: name of Var missing", tree)
         | SOME name => name,
         the_default 0 (Option.map (index_of_string "term_of_xml" tree)
           (Properties.get atts "index"))),
        type_of_xml typ)
-  | term_of_xml (XML.Elem ("Const", [("name", s)], [typ])) =
+  | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
       Const (s, type_of_xml typ)
-  | term_of_xml (XML.Elem ("App", [], [term, term'])) =
+  | term_of_xml (XML.Elem (("App", []), [term, term'])) =
       term_of_xml term $ term_of_xml term'
-  | term_of_xml (XML.Elem ("Abs", [("vname", s)], [typ, term])) =
+  | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
       Abs (s, type_of_xml typ, term_of_xml term)
   | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
 
 fun opttypes_of_xml [] = NONE
-  | opttypes_of_xml [XML.Elem ("types", [], types)] =
+  | opttypes_of_xml [XML.Elem (("types", []), types)] =
       SOME (map type_of_xml types)
   | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
 
-fun proof_of_xml (tree as XML.Elem ("PBound", [("index", idx)], [])) =
+fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
       PBound (index_of_string "proof_of_xml" tree idx)
-  | proof_of_xml (XML.Elem ("Abst", [("vname", s)], [proof])) =
+  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
       Abst (s, NONE, proof_of_xml proof)
-  | proof_of_xml (XML.Elem ("Abst", [("vname", s)], [typ, proof])) =
+  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
       Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
-  | proof_of_xml (XML.Elem ("AbsP", [("vname", s)], [proof])) =
+  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
       AbsP (s, NONE, proof_of_xml proof)
-  | proof_of_xml (XML.Elem ("AbsP", [("vname", s)], [term, proof])) =
+  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
       AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
-  | proof_of_xml (XML.Elem ("Appt", [], [proof])) =
+  | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
       proof_of_xml proof % NONE
-  | proof_of_xml (XML.Elem ("Appt", [], [proof, term])) =
+  | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
       proof_of_xml proof % SOME (term_of_xml term)
-  | proof_of_xml (XML.Elem ("AppP", [], [proof, proof'])) =
+  | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
       proof_of_xml proof %% proof_of_xml proof'
-  | proof_of_xml (XML.Elem ("Hyp", [], [term])) =
+  | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
       Hyp (term_of_xml term)
-  | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
+  | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
       (* FIXME? *)
       PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
         Future.value (Proofterm.approximate_proof_body MinProof)))
-  | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
+  | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
       PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
-  | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
+  | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
       Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
-  | proof_of_xml (XML.Elem ("MinProof", _, _)) = MinProof
+  | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
   | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
 
 end;
diff -r b32a44361186 -r ea417f69b36f src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/build-jars	Mon Aug 09 11:45:30 2010 +0200
@@ -37,7 +37,6 @@
   Isar/outer_syntax.scala
   Isar/parse.scala
   Isar/token.scala
-  PIDE/change.scala
   PIDE/command.scala
   PIDE/document.scala
   PIDE/event_bus.scala
diff -r b32a44361186 -r ea417f69b36f src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/context_position.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -9,7 +9,7 @@
   val is_visible: Proof.context -> bool
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
-  val report_visible: Proof.context -> Markup.T -> Position.T -> unit
+  val report: Proof.context -> Markup.T -> Position.T -> unit
 end;
 
 structure Context_Position: CONTEXT_POSITION =
@@ -25,7 +25,7 @@
 val set_visible = Data.put;
 val restore_visible = set_visible o is_visible;
 
-fun report_visible ctxt markup pos =
+fun report ctxt markup pos =
   if is_visible ctxt then Position.report markup pos else ();
 
 end;
diff -r b32a44361186 -r ea417f69b36f src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/goal.ML	Mon Aug 09 11:45:30 2010 +0200
@@ -26,7 +26,6 @@
   val fork: (unit -> 'a) -> 'a future
   val future_enabled: unit -> bool
   val local_future_enabled: unit -> bool
-  val local_future_enforced: unit -> bool
   val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
@@ -104,7 +103,7 @@
 
 (* parallel proofs *)
 
-fun fork e = Future.fork_pri ~1 (fn () => Future.report e);
+fun fork e = Future.fork_pri ~1 (fn () => Future.status e);
 
 val parallel_proofs = Unsynchronized.ref 1;
 
@@ -112,7 +111,6 @@
   Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
 
 fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
-fun local_future_enforced () = future_enabled () andalso ! parallel_proofs >= 3;
 
 
 (* future_result *)
diff -r b32a44361186 -r ea417f69b36f src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Pure/library.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -89,8 +89,9 @@
     (parent: Component, title: String, message: Any*)
   {
     Swing_Thread.now {
+      val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
       JOptionPane.showMessageDialog(parent,
-        message.toArray.asInstanceOf[Array[AnyRef]],
+        java_message.toArray.asInstanceOf[Array[AnyRef]],
         if (title == null) default_title else title, kind)
     }
   }
diff -r b32a44361186 -r ea417f69b36f src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -2,7 +2,7 @@
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
-Document model connected to jEdit buffer.
+Document model connected to jEdit buffer -- single node in theory graph.
 */
 
 package isabelle.jedit
@@ -149,10 +149,10 @@
 
   private val key = "isabelle.document_model"
 
-  def init(session: Session, buffer: Buffer): Document_Model =
+  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
   {
-    Swing_Thread.assert()
-    val model = new Document_Model(session, buffer)
+    Swing_Thread.require()
+    val model = new Document_Model(session, buffer, thy_name)
     buffer.setProperty(key, model)
     model.activate()
     model
@@ -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) =>
@@ -180,7 +180,7 @@
 }
 
 
-class Document_Model(val session: Session, val buffer: Buffer)
+class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
 {
   /* visible line end */
 
@@ -195,32 +195,39 @@
   }
 
 
-  /* global state -- owned by Swing thread */
+  /* pending text edits */
+
+  object pending_edits  // owned by Swing thread
+  {
+    private val pending = new mutable.ListBuffer[Text_Edit]
+    def snapshot(): List[Text_Edit] = pending.toList
+
+    private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
+      if (!pending.isEmpty) session.edit_document(List((thy_name, flush())))
+    }
 
-  @volatile private var history = Change.init // owned by Swing thread
-  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
+    def flush(): List[Text_Edit] =
+    {
+      Swing_Thread.require()
+      val edits = snapshot()
+      pending.clear
+      edits
+    }
+
+    def +=(edit: Text_Edit)
+    {
+      Swing_Thread.require()
+      pending += edit
+      delay_flush()
+    }
+  }
 
 
   /* snapshot */
 
-  // FIXME proper error handling
-  val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2
-
-  def current_change(): Change = history
-
-  def snapshot(): Change.Snapshot =
-    Swing_Thread.now { history.snapshot(thy_name, edits_buffer.toList) }
-
-
-  /* text edits */
-
-  private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
-    if (!edits_buffer.isEmpty) {
-      val new_change = history.edit(session, List((thy_name, edits_buffer.toList)))
-      edits_buffer.clear
-      history = new_change
-      new_change.result.map(_ => session.input(new_change))
-    }
+  def snapshot(): Document.Snapshot = {
+    Swing_Thread.require()
+    session.current_change().snapshot(thy_name, pending_edits.snapshot())
   }
 
 
@@ -231,15 +238,13 @@
     override def contentInserted(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, length: Int)
     {
-      edits_buffer += new Text_Edit(true, offset, buffer.getText(offset, length))
-      edits_delay()
+      pending_edits += new Text_Edit(true, offset, buffer.getText(offset, length))
     }
 
     override def preContentRemoved(buffer: JEditBuffer,
       start_line: Int, start: Int, num_lines: Int, removed_length: Int)
     {
-      edits_buffer += new Text_Edit(false, start, buffer.getText(start, removed_length))
-      edits_delay()
+      pending_edits += new Text_Edit(false, start, buffer.getText(start, removed_length))
     }
   }
 
@@ -257,7 +262,8 @@
       val start = buffer.getLineStartOffset(line)
       val stop = start + line_segment.count
 
-      val snapshot = Document_Model.this.snapshot()
+      // FIXME proper synchronization / thread context (!??)
+      val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
 
       /* FIXME
       for (text_area <- Isabelle.jedit_text_areas(buffer)
@@ -314,9 +320,7 @@
     buffer.setTokenMarker(token_marker)
     buffer.addBufferListener(buffer_listener)
     buffer.propertiesChanged()
-
-    edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
-    edits_delay()
+    pending_edits += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
   }
 
   def refresh()
diff -r b32a44361186 -r ea417f69b36f src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -24,7 +24,7 @@
 
 object Document_View
 {
-  def choose_color(snapshot: Change.Snapshot, command: Command): Color =
+  def choose_color(snapshot: Document.Snapshot, command: Command): Color =
   {
     val state = snapshot.document.current_state(command)
     if (snapshot.is_outdated) new Color(240, 240, 240)
@@ -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)
   }
 
@@ -116,9 +116,9 @@
     }
   }
 
-  def full_repaint(snapshot: Change.Snapshot, changed: Set[Command])
+  def full_repaint(snapshot: Document.Snapshot, changed: Set[Command])
   {
-    Swing_Thread.assert()
+    Swing_Thread.require()
 
     val buffer = model.buffer
     var visible_change = false
@@ -148,54 +148,57 @@
       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.Node.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 +216,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) {
diff -r b32a44361186 -r ea417f69b36f src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -158,7 +158,8 @@
       val html_body =
         current_body.flatMap(div =>
           Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
-            .map(t => XML.Elem(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE)), HTML.spans(t))))
+            .map(t =>
+              XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))), HTML.spans(t))))
       val doc =
         builder.parse(
           new InputSourceImpl(
diff -r b32a44361186 -r ea417f69b36f src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Aug 09 11:45:30 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()
diff -r b32a44361186 -r ea417f69b36f src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Aug 09 11:45:30 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) =>
           {
diff -r b32a44361186 -r ea417f69b36f src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Aug 09 11:45:30 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()))
@@ -68,8 +68,8 @@
               val snapshot = doc_view.model.snapshot()
               val filtered_results =
                 snapshot.document.current_state(cmd).results filter {
-                  case XML.Elem(Markup.TRACING, _, _) => show_tracing
-                  case XML.Elem(Markup.DEBUG, _, _) => show_debug
+                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
+                  case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
                   case _ => true
                 }
               html_panel.render(filtered_results)
diff -r b32a44361186 -r ea417f69b36f src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Mon Aug 09 11:45:30 2010 +0200
@@ -1,6 +1,4 @@
 /*  Title:      Tools/jEdit/src/jedit/plugin.scala
-    Author:     Johannes Hölzl, TU Munich
-    Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
 Main Isabelle/jEdit plugin setup.
@@ -32,11 +30,6 @@
   var session: Session = null
 
 
-  /* name */
-
-  val NAME = "Isabelle"
-
-
   /* properties */
 
   val OPTION_PREFIX = "options.isabelle."
@@ -110,7 +103,7 @@
   }
 
 
-  /* main jEdit components */  // FIXME ownership!?
+  /* main jEdit components */
 
   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
 
@@ -149,12 +142,12 @@
     }
 
 
-  /* manage prover */
+  /* manage prover */  // FIXME async!?
 
   private def prover_started(view: View): Boolean =
   {
     val timeout = Int_Property("startup-timeout") max 1000
-    session.start(timeout, Isabelle.isabelle_args()) match {
+    session.started(timeout, Isabelle.isabelle_args()) match {
       case Some(err) =>
         val text = new JTextArea(err); text.setEditable(false)
         Library.error_dialog(view, null, "Failed to start Isabelle process", text)
@@ -169,7 +162,10 @@
   def activate_buffer(view: View, buffer: Buffer)
   {
     if (prover_started(view)) {
-      val model = Document_Model.init(session, buffer)
+      // FIXME proper error handling
+      val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))
+
+      val model = Document_Model.init(session, buffer, thy_name)
       for (text_area <- jedit_text_areas(buffer))
         Document_View.init(model, text_area)
     }