# HG changeset patch
# User wenzelm
# Date 1310327201 -7200
# Node ID 8786e36b81429b435b6dd275636fd5252fb96043
# Parent  d033a34a490a0902d07e9ec246073d8cffa77903# Parent  70072780e095a7d7ab4aefc4471282de71668546
merged;

diff -r d033a34a490a -r 8786e36b8142 NEWS
--- a/NEWS	Sun Jul 10 21:39:03 2011 +0200
+++ b/NEWS	Sun Jul 10 21:46:41 2011 +0200
@@ -149,6 +149,12 @@
 
 *** ML ***
 
+* The inner syntax of sort/type/term/prop supports inlined YXML
+representations within quoted string tokens.  By encoding logical
+entities via Term_XML (in ML or Scala) concrete syntax can be
+bypassed, which is particularly useful for producing bits of text
+under external program control.
+
 * Antiquotations for ML and document preparation are managed as theory
 data, which requires explicit setup.
 
diff -r d033a34a490a -r 8786e36b8142 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -71,11 +71,11 @@
 
 fun counter () =
   let
-    val counter = var "counter" 0;
+    val counter = var "counter" (0: int);
     fun next () =
       change_result counter
         (fn i =>
-          let val j = i + 1
+          let val j = i + (1: int)
           in (j, j) end);
   in next end;
 
diff -r d033a34a490a -r 8786e36b8142 src/Pure/Concurrent/synchronized_sequential.ML
--- a/src/Pure/Concurrent/synchronized_sequential.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/Concurrent/synchronized_sequential.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -27,11 +27,11 @@
 
 fun counter () =
   let
-    val counter = var "counter" 0;
+    val counter = var "counter" (0: int);
     fun next () =
       change_result counter
         (fn i =>
-          let val j = i + 1
+          let val j = i + (1: int)
           in (j, j) end);
   in next end;
 
diff -r d033a34a490a -r 8786e36b8142 src/Pure/Concurrent/volatile.scala
--- a/src/Pure/Concurrent/volatile.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/Concurrent/volatile.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -10,7 +10,7 @@
 class Volatile[A](init: A)
 {
   @volatile private var state: A = init
-  def peek(): A = state
+  def apply(): A = state
   def change(f: A => A) { state = f(state) }
   def change_yield[B](f: A => (B, A)): B =
   {
diff -r d033a34a490a -r 8786e36b8142 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/General/markup.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -302,6 +302,12 @@
   val EDIT = "edit"
 
 
+  /* prover process */
+
+  val PROVER_COMMAND = "prover_command"
+  val PROVER_ARG = "prover_arg"
+
+
   /* messages */
 
   val Serial = new Long_Property("serial")
diff -r d033a34a490a -r 8786e36b8142 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/General/pretty.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -53,7 +53,7 @@
           Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
     }
 
-  case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
+  sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
   {
     def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
     def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
diff -r d033a34a490a -r 8786e36b8142 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/General/sha1.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -12,7 +12,7 @@
 
 object SHA1
 {
-  case class Digest(rep: String)
+  sealed case class Digest(rep: String)
   {
     override def toString: String = rep
   }
diff -r d033a34a490a -r 8786e36b8142 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/General/symbol.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -120,7 +120,7 @@
 
   class Index(text: CharSequence)
   {
-    case class Entry(chr: Int, sym: Int)
+    sealed case class Entry(chr: Int, sym: Int)
     val index: Array[Entry] =
     {
       val matcher = new Matcher(text)
diff -r d033a34a490a -r 8786e36b8142 src/Pure/General/xml_data.ML
--- a/src/Pure/General/xml_data.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/General/xml_data.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -4,139 +4,151 @@
 XML as basic data representation language.
 *)
 
+signature XML_DATA_OPS =
+sig
+  type 'a T
+  val properties: Properties.T T
+  val string: string T
+  val int: int T
+  val bool: bool T
+  val unit: unit T
+  val pair: 'a T -> 'b T -> ('a * 'b) T
+  val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
+  val list: 'a T -> 'a list T
+  val option: 'a T -> 'a option T
+  val variant: 'a T list -> 'a T
+end;
+
 signature XML_DATA =
 sig
+  structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body
   exception XML_ATOM of string
   exception XML_BODY of XML.body
-  val make_properties: Properties.T -> XML.body
-  val dest_properties: XML.body -> Properties.T
-  val make_string: string -> XML.body
-  val dest_string : XML.body -> string
-  val make_int: int -> XML.body
-  val dest_int : XML.body -> int
-  val make_bool: bool -> XML.body
-  val dest_bool: XML.body -> bool
-  val make_unit: unit -> XML.body
-  val dest_unit: XML.body -> unit
-  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
-  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
-  val make_triple:
-    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
-  val dest_triple:
-    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
-  val make_list: ('a -> XML.body) -> 'a list -> XML.body
-  val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
-  val make_option: ('a -> XML.body) -> 'a option -> XML.body
-  val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
-  val make_variant: ('a -> XML.body) list -> 'a -> XML.body
-  val dest_variant: (XML.body -> 'a) list -> XML.body -> 'a
+  structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a
 end;
 
 structure XML_Data: XML_DATA =
 struct
 
-(* basic values *)
-
-exception XML_ATOM of string;
-
+(** encode **)
 
-fun make_int_atom i = signed_string_of_int i;
+structure Encode =
+struct
 
-fun dest_int_atom s =
-  (case Int.fromString s of
-    SOME i => i
-  | NONE => raise XML_ATOM s);
+type 'a T = 'a -> XML.body;
 
 
-fun make_bool_atom false = "0"
-  | make_bool_atom true = "1";
+(* basic values *)
+
+fun int_atom i = signed_string_of_int i;
 
-fun dest_bool_atom "0" = false
-  | dest_bool_atom "1" = true
-  | dest_bool_atom s = raise XML_ATOM s;
-
+fun bool_atom false = "0"
+  | bool_atom true = "1";
 
-fun make_unit_atom () = "";
-
-fun dest_unit_atom "" = ()
-  | dest_unit_atom s = raise XML_ATOM s;
+fun unit_atom () = "";
 
 
 (* structural nodes *)
 
-exception XML_BODY of XML.tree list;
-
-fun make_node ts = XML.Elem ((":", []), ts);
+fun node ts = XML.Elem ((":", []), ts);
 
-fun dest_node (XML.Elem ((":", []), ts)) = ts
-  | dest_node t = raise XML_BODY [t];
-
-fun make_tagged (tag, ts) = XML.Elem ((make_int_atom tag, []), ts);
-
-fun dest_tagged (XML.Elem ((s, []), ts)) = (dest_int_atom s, ts)
-  | dest_tagged t = raise XML_BODY [t];
+fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
 
 
 (* representation of standard types *)
 
-fun make_properties props = [XML.Elem ((":", props), [])];
-
-fun dest_properties [XML.Elem ((":", props), [])] = props
-  | dest_properties ts = raise XML_BODY ts;
-
+fun properties props = [XML.Elem ((":", props), [])];
 
-fun make_string "" = []
-  | make_string s = [XML.Text s];
-
-fun dest_string [] = ""
-  | dest_string [XML.Text s] = s
-  | dest_string ts = raise XML_BODY ts;
-
+fun string "" = []
+  | string s = [XML.Text s];
 
-val make_int = make_string o make_int_atom;
-val dest_int = dest_int_atom o dest_string;
-
-val make_bool = make_string o make_bool_atom;
-val dest_bool = dest_bool_atom o dest_string;
+val int = string o int_atom;
 
-val make_unit = make_string o make_unit_atom;
-val dest_unit = dest_unit_atom o dest_string;
-
+val bool = string o bool_atom;
 
-fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
-
-fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
-  | dest_pair _ _ ts = raise XML_BODY ts;
+val unit = string o unit_atom;
 
-
-fun make_triple make1 make2 make3 (x, y, z) =
-  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
+fun pair f g (x, y) = [node (f x), node (g y)];
 
-fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
-      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
-  | dest_triple _ _ _ ts = raise XML_BODY ts;
-
-
-fun make_list make xs = map (make_node o make) xs;
-
-fun dest_list dest ts = map (dest o dest_node) ts;
-
+fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
 
-fun make_option _ NONE = []
-  | make_option make (SOME x) = [make_node (make x)];
-
-fun dest_option _ [] = NONE
-  | dest_option dest [t] = SOME (dest (dest_node t))
-  | dest_option _ ts = raise XML_BODY ts;
-
+fun list f xs = map (node o f) xs;
 
-fun make_variant makes x =
-  [make_tagged (the (get_index (fn make => try make x) makes))];
+fun option _ NONE = []
+  | option f (SOME x) = [node (f x)];
 
-fun dest_variant dests [t] =
-      let val (tag, ts) = dest_tagged t
-      in nth dests tag ts end
-  | dest_variant _ ts = raise XML_BODY ts;
+fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
 
 end;
 
+
+
+(** decode **)
+
+exception XML_ATOM of string;
+exception XML_BODY of XML.tree list;
+
+structure Decode =
+struct
+
+type 'a T = XML.body -> 'a;
+
+
+(* basic values *)
+
+fun int_atom s =
+  (case Int.fromString s of
+    SOME i => i
+  | NONE => raise XML_ATOM s);
+
+fun bool_atom "0" = false
+  | bool_atom "1" = true
+  | bool_atom s = raise XML_ATOM s;
+
+fun unit_atom "" = ()
+  | unit_atom s = raise XML_ATOM s;
+
+
+(* structural nodes *)
+
+fun node (XML.Elem ((":", []), ts)) = ts
+  | node t = raise XML_BODY [t];
+
+fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts)
+  | tagged t = raise XML_BODY [t];
+
+
+(* representation of standard types *)
+
+fun properties [XML.Elem ((":", props), [])] = props
+  | properties ts = raise XML_BODY ts;
+
+fun string [] = ""
+  | string [XML.Text s] = s
+  | string ts = raise XML_BODY ts;
+
+val int = int_atom o string;
+
+val bool = bool_atom o string;
+
+val unit = unit_atom o string;
+
+fun pair f g [t1, t2] = (f (node t1), g (node t2))
+  | pair _ _ ts = raise XML_BODY ts;
+
+fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
+  | triple _ _ _ ts = raise XML_BODY ts;
+
+fun list f ts = map (f o node) ts;
+
+fun option _ [] = NONE
+  | option f [t] = SOME (f (node t))
+  | option _ ts = raise XML_BODY ts;
+
+fun variant fs [t] = uncurry (nth fs) (tagged t)
+  | variant _ ts = raise XML_BODY ts;
+
+end;
+
+end;
+
diff -r d033a34a490a -r 8786e36b8142 src/Pure/General/xml_data.scala
--- a/src/Pure/General/xml_data.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/General/xml_data.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -10,150 +10,167 @@
 
 object XML_Data
 {
-  /* basic values */
-
-  class XML_Atom(s: String) extends Exception(s)
-
+  /** encode **/
 
-  private def make_long_atom(i: Long): String = i.toString
-
-  private def dest_long_atom(s: String): Long =
-    try { java.lang.Long.parseLong(s) }
-    catch { case e: NumberFormatException => throw new XML_Atom(s) }
+  object Encode
+  {
+    type T[A] = A => XML.Body
 
 
-  private def make_int_atom(i: Int): String = i.toString
+    /* basic values */
+
+    private def long_atom(i: Long): String = i.toString
 
-  private def dest_int_atom(s: String): Int =
-    try { Integer.parseInt(s) }
-    catch { case e: NumberFormatException => throw new XML_Atom(s) }
+    private def int_atom(i: Int): String = i.toString
+
+    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
+
+    private def unit_atom(u: Unit) = ""
 
 
-  private def make_bool_atom(b: Boolean): String = if (b) "1" else "0"
+    /* structural nodes */
 
-  private def dest_bool_atom(s: String): Boolean =
-    if (s == "1") true
-    else if (s == "0") false
-    else throw new XML_Atom(s)
+    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
 
-
-  private def make_unit_atom(u: Unit) = ""
-
-  private def dest_unit_atom(s: String): Unit =
-    if (s == "") () else throw new XML_Atom(s)
+    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
+      XML.Elem(Markup(int_atom(tag), Nil), ts)
 
 
-  /* structural nodes */
+    /* representation of standard types */
+
+    val properties: T[List[(String, String)]] =
+      (props => List(XML.Elem(Markup(":", props), Nil)))
 
-  class XML_Body(body: XML.Body) extends Exception
+    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
+
+    val long: T[Long] = (x => string(long_atom(x)))
+
+    val int: T[Int] = (x => string(int_atom(x)))
+
+    val bool: T[Boolean] = (x => string(bool_atom(x)))
 
-  private def make_node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
+    val unit: T[Unit] = (x => string(unit_atom(x)))
+
+    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
+      (x => List(node(f(x._1)), node(g(x._2))))
+
+    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
+      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
 
-  private def dest_node(t: XML.Tree): XML.Body =
-    t match {
-      case XML.Elem(Markup(":", Nil), ts) => ts
-      case _ => throw new XML_Body(List(t))
+    def list[A](f: T[A]): T[List[A]] =
+      (xs => xs.map((x: A) => node(f(x))))
+
+    def option[A](f: T[A]): T[Option[A]] =
+    {
+      case None => Nil
+      case Some(x) => List(node(f(x)))
     }
 
-  private def make_tagged(tag: Int, ts: XML.Body): XML.Tree =
-    XML.Elem(Markup(make_int_atom(tag), Nil), ts)
+    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
+    {
+      case x =>
+        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
+        List(tagged(tag, f(x)))
+    }
+  }
+
 
-  private def dest_tagged(t: XML.Tree): (Int, XML.Body) =
-    t match {
-      case XML.Elem(Markup(s, Nil), ts) => (dest_int_atom(s), ts)
-      case _ => throw new XML_Body(List(t))
-    }
+
+  /** decode **/
+
+  class XML_Atom(s: String) extends Exception(s)
+  class XML_Body(body: XML.Body) extends Exception
+
+  object Decode
+  {
+    type T[A] = XML.Body => A
 
 
-  /* representation of standard types */
+     /* basic values */
+
+    private def long_atom(s: String): Long =
+      try { java.lang.Long.parseLong(s) }
+      catch { case e: NumberFormatException => throw new XML_Atom(s) }
 
-  def make_properties(props: List[(String, String)]): XML.Body =
-    List(XML.Elem(Markup(":", props), Nil))
+    private def int_atom(s: String): Int =
+      try { Integer.parseInt(s) }
+      catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+    private def bool_atom(s: String): Boolean =
+      if (s == "1") true
+      else if (s == "0") false
+      else throw new XML_Atom(s)
+
+    private def unit_atom(s: String): Unit =
+      if (s == "") () else throw new XML_Atom(s)
+
 
-  def dest_properties(ts: XML.Body): List[(String, String)] =
-    ts match {
+    /* structural nodes */
+
+    private def node(t: XML.Tree): XML.Body =
+      t match {
+        case XML.Elem(Markup(":", Nil), ts) => ts
+        case _ => throw new XML_Body(List(t))
+      }
+
+    private def tagged(t: XML.Tree): (Int, XML.Body) =
+      t match {
+        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
+        case _ => throw new XML_Body(List(t))
+      }
+
+
+    /* representation of standard types */
+
+    val properties: T[List[(String, String)]] =
+    {
       case List(XML.Elem(Markup(":", props), Nil)) => props
-      case _ => throw new XML_Body(ts)
+      case ts => throw new XML_Body(ts)
     }
 
-
-  def make_string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
-
-  def dest_string(ts: XML.Body): String =
-    ts match {
+    val string: T[String] =
+    {
       case Nil => ""
       case List(XML.Text(s)) => s
-      case _ => throw new XML_Body(ts)
+      case ts => throw new XML_Body(ts)
     }
 
-
-  def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
-  def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
+    val long: T[Long] = (x => long_atom(string(x)))
 
-  def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
-  def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
+    val int: T[Int] = (x => int_atom(string(x)))
 
-  def make_bool(b: Boolean): XML.Body = make_string(make_bool_atom(b))
-  def dest_bool(ts: XML.Body) = dest_bool_atom(dest_string(ts))
+    val bool: T[Boolean] = (x => bool_atom(string(x)))
 
-  def make_unit(u: Unit): XML.Body = make_string(make_unit_atom(u))
-  def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
-
+    val unit: T[Unit] = (x => unit_atom(string(x)))
 
-  def make_pair[A, B](make1: A => XML.Body)(make2: B => XML.Body)(p: (A, B)): XML.Body =
-    List(make_node(make1(p._1)), make_node(make2(p._2)))
-
-  def dest_pair[A, B](dest1: XML.Body => A)(dest2: XML.Body => B)(ts: XML.Body): (A, B) =
-    ts match {
-      case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
-      case _ => throw new XML_Body(ts)
+    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
+    {
+      case List(t1, t2) => (f(node(t1)), g(node(t2)))
+      case ts => throw new XML_Body(ts)
     }
 
-
-  def make_triple[A, B, C](make1: A => XML.Body)(make2: B => XML.Body)(make3: C => XML.Body)
-      (p: (A, B, C)): XML.Body =
-    List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
-
-  def dest_triple[A, B, C](dest1: XML.Body => A)(dest2: XML.Body => B)(dest3: XML.Body => C)
-      (ts: XML.Body): (A, B, C) =
-    ts match {
-      case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
-      case _ => throw new XML_Body(ts)
+    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
+    {
+      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
+      case ts => throw new XML_Body(ts)
     }
 
-
-  def make_list[A](make: A => XML.Body)(xs: List[A]): XML.Body =
-    xs.map((x: A) => make_node(make(x)))
+    def list[A](f: T[A]): T[List[A]] =
+      (ts => ts.map(t => f(node(t))))
 
-  def dest_list[A](dest: XML.Body => A)(ts: XML.Body): List[A] =
-    ts.map((t: XML.Tree) => dest(dest_node(t)))
-
-
-  def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
-    opt match {
-      case None => Nil
-      case Some(x) => List(make_node(make(x)))
+    def option[A](f: T[A]): T[Option[A]] =
+    {
+      case Nil => None
+      case List(t) => Some(f(node(t)))
+      case ts => throw new XML_Body(ts)
     }
 
-  def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
-    ts match {
-      case Nil => None
-      case List(t) => Some(dest(dest_node(t)))
-      case _ => throw new XML_Body(ts)
+    def variant[A](fs: List[T[A]]): T[A] =
+    {
+      case List(t) =>
+        val (tag, ts) = tagged(t)
+        fs(tag)(ts)
+      case ts => throw new XML_Body(ts)
     }
-
-
-  def make_variant[A](makes: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
-  {
-    val (make, tag) = makes.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
-    List(make_tagged(tag, make(x)))
   }
-
-  def dest_variant[A](dests: List[XML.Body => A])(ts: XML.Body): A =
-    ts match {
-      case List(t) =>
-        val (tag, ts) = dest_tagged(t)
-        dests(tag)(ts)
-      case _ => throw new XML_Body(ts)
-    }
 }
diff -r d033a34a490a -r 8786e36b8142 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/General/yxml.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -16,8 +16,10 @@
 signature YXML =
 sig
   val escape_controls: string -> string
+  val detect: string -> bool
   val output_markup: Markup.T -> string * string
   val element: string -> XML.attributes -> string list -> string
+  val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
@@ -48,6 +50,8 @@
 val XY = X ^ Y;
 val XYX = XY ^ X;
 
+val detect = exists_string (fn s => s = X);
+
 
 (* output *)
 
@@ -59,17 +63,20 @@
   let val (pre, post) = output_markup (name, atts)
   in pre ^ implode body ^ post end;
 
-fun string_of t =
+fun string_of_body body =
   let
     fun attrib (a, x) =
       Buffer.add Y #>
       Buffer.add a #> Buffer.add "=" #> Buffer.add x;
     fun tree (XML.Elem ((name, atts), ts)) =
           Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
-          fold tree ts #>
+          trees ts #>
           Buffer.add XYX
-      | tree (XML.Text s) = Buffer.add s;
-  in Buffer.empty |> tree t |> Buffer.content end;
+      | tree (XML.Text s) = Buffer.add s
+    and trees ts = fold tree ts;
+  in Buffer.empty |> trees body |> Buffer.content end;
+
+val string_of = string_of_body o single;
 
 
 
diff -r d033a34a490a -r 8786e36b8142 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/IsaMakefile	Sun Jul 10 21:46:41 2011 +0200
@@ -250,6 +250,7 @@
   term.ML						\
   term_ord.ML						\
   term_subst.ML						\
+  term_xml.ML						\
   theory.ML						\
   thm.ML						\
   type.ML						\
diff -r d033a34a490a -r 8786e36b8142 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/Isar/token.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -180,8 +180,9 @@
 
 (* token content *)
 
-fun source_of (Token ((source, (pos, _)), _, _)) =
-  YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
+fun source_of (Token ((source, (pos, _)), (_, x), _)) =
+  if YXML.detect x then x
+  else 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 d033a34a490a -r 8786e36b8142 src/Pure/PIDE/blob.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/blob.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -0,0 +1,28 @@
+/*  Title:      Pure/PIDE/blob.scala
+    Author:     Makarius
+
+Unidentified text with markup.
+*/
+
+package isabelle
+
+
+object Blob
+{
+  sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
+  {
+    def + (info: Text.Info[Any]): State = copy(markup = markup + info)
+  }
+}
+
+
+sealed case class Blob(val source: String)
+{
+  def source(range: Text.Range): String = source.substring(range.start, range.stop)
+
+  lazy val symbol_index = new Symbol.Index(source)
+  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
+  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
+
+  val empty_state: Blob.State = Blob.State(this)
+}
diff -r d033a34a490a -r 8786e36b8142 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -16,7 +16,7 @@
 {
   /** accumulated results from prover **/
 
-  case class State(
+  sealed case class State(
     val command: Command,
     val status: List[Markup] = Nil,
     val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
diff -r d033a34a490a -r 8786e36b8142 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -16,12 +16,14 @@
   val parse_id: string -> id
   val print_id: id -> string
   type edit = string * ((command_id option * command_id option) list) option
+  type header = string * (string * string list * string list)
   type state
   val init_state: state
   val get_theory: state -> version_id -> Position.T -> string -> theory
   val cancel_execution: state -> unit -> unit
   val define_command: command_id -> string -> state -> state
-  val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
+  val edit: version_id -> version_id -> edit list -> header list ->
+    state -> (command_id * exec_id) list * state
   val execute: version_id -> state -> state
   val state: unit -> state
   val change_state: (state -> state) -> unit
@@ -78,6 +80,8 @@
   (*NONE: remove node, SOME: insert/remove commands*)
   ((command_id option * command_id option) list) option;
 
+type header = string * (string * string list * string list);
+
 fun the_entry (Node {entries, ...}) id =
   (case Entries.lookup entries id of
     NONE => err_undef "command entry" id
@@ -309,8 +313,10 @@
 
 in
 
-fun edit (old_id: version_id) (new_id: version_id) edits state =
+fun edit (old_id: version_id) (new_id: version_id) edits headers state =
   let
+    (* FIXME apply headers *)
+
     val old_version = the_version state old_id;
     val _ = Time.now ();  (* FIXME odd workaround *)
     val new_version = fold edit_nodes edits old_version;
diff -r d033a34a490a -r 8786e36b8142 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -46,10 +46,10 @@
 
   object Node
   {
-    class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
-    val empty_header = new Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
+    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
+    val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
 
-    val empty: Node = new Node(empty_header, Linear_Set())
+    val empty: Node = Node(empty_header, Map(), Linear_Set())
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
@@ -65,13 +65,11 @@
 
   private val block_size = 1024
 
-  class Node(val header: Node.Header, val commands: Linear_Set[Command])
+  sealed case class Node(
+    val header: Node.Header,
+    val blobs: Map[String, Blob],
+    val commands: Linear_Set[Command])
   {
-    /* header */
-
-    def set_header(header: Node.Header): Node = new Node(header, commands)
-
-
     /* commands */
 
     private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
@@ -132,25 +130,24 @@
 
   object Version
   {
-    val init: Version = new Version(no_id, Map().withDefaultValue(Node.empty))
+    val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
   }
 
-  class Version(val id: Version_ID, val nodes: Map[String, Node])
+  sealed case class Version(val id: Version_ID, val nodes: Map[String, Node])
 
 
   /* changes of plain text, eventually resulting in document edits */
 
   object Change
   {
-    val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init))
+    val init = Change(Future.value(Version.init), Nil, Future.value(Version.init))
   }
 
-  class Change(
+  sealed case class Change(
     val previous: Future[Version],
     val edits: List[Edit_Text],
-    val result: Future[(List[Edit_Command], Version)])
+    val version: Future[Version])
   {
-    val version: Future[Version] = result.map(_._2)
     def is_finished: Boolean = previous.is_finished && version.is_finished
   }
 
@@ -209,11 +206,11 @@
     }
   }
 
-  case class State(
+  sealed case class State(
     val versions: Map[Version_ID, Version] = Map(),
     val commands: Map[Command_ID, Command.State] = Map(),
     val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
-    val assignments: Map[Version, State.Assignment] = Map(),
+    val assignments: Map[Version_ID, State.Assignment] = Map(),
     val disposed: Set[ID] = Set(),  // FIXME unused!?
     val history: History = History.init)
   {
@@ -224,7 +221,7 @@
       val id = version.id
       if (versions.isDefinedAt(id) || disposed(id)) fail
       copy(versions = versions + (id -> version),
-        assignments = assignments + (version -> State.Assignment(former_assignment)))
+        assignments = assignments + (id -> State.Assignment(former_assignment)))
     }
 
     def define_command(command: Command): State =
@@ -239,7 +236,8 @@
     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
     def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
     def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
-    def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
+    def the_assignment(version: Version): State.Assignment =
+      assignments.getOrElse(version.id, fail)
 
     def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
@@ -269,22 +267,21 @@
           (st.command, exec_id)
         }
       val new_assignment = the_assignment(version).assign(assigned_execs)
-      val new_state =
-        copy(assignments = assignments + (version -> new_assignment), execs = new_execs)
+      val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
       (assigned_execs.map(_._1), new_state)
     }
 
     def is_assigned(version: Version): Boolean =
-      assignments.get(version) match {
+      assignments.get(version.id) match {
         case Some(assgn) => assgn.is_finished
         case None => false
       }
 
     def extend_history(previous: Future[Version],
         edits: List[Edit_Text],
-        result: Future[(List[Edit_Command], Version)]): (Change, State) =
+        version: Future[Version]): (Change, State) =
     {
-      val change = new Change(previous, edits, result)
+      val change = Change(previous, edits, version)
       (change, copy(history = history + change))
     }
 
diff -r d033a34a490a -r 8786e36b8142 src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -13,22 +13,19 @@
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.edit_version"
-    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
+    (fn [old_id_string, new_id_string, edits_yxml, headers_yxml] => Document.change_state (fn state =>
       let
         val old_id = Document.parse_id old_id_string;
         val new_id = Document.parse_id new_id_string;
-        val edits =
-          XML_Data.dest_list
-            (XML_Data.dest_pair
-              XML_Data.dest_string
-              (XML_Data.dest_option
-                (XML_Data.dest_list
-                  (XML_Data.dest_pair
-                    (XML_Data.dest_option XML_Data.dest_int)
-                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
+        val edits = YXML.parse_body edits_yxml |>
+          let open XML_Data.Decode
+          in list (pair string (option (list (pair (option int) (option int))))) end;
+        val headers = YXML.parse_body headers_yxml |>
+          let open XML_Data.Decode
+          in list (pair string (triple string (list string) (list string))) end;
 
       val await_cancellation = Document.cancel_execution state;
-      val (updates, state') = Document.edit old_id new_id edits state;
+      val (updates, state') = Document.edit old_id new_id edits headers state;
       val _ = await_cancellation ();
       val _ =
         Output.status (Markup.markup (Markup.assign new_id)
diff -r d033a34a490a -r 8786e36b8142 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -140,17 +140,18 @@
   /* document versions */
 
   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
-      edits: List[Document.Edit_Command_ID])
+      edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
   {
-    val arg =
-      XML_Data.make_list(
-        XML_Data.make_pair(XML_Data.make_string)(
-          XML_Data.make_option(XML_Data.make_list(
-              XML_Data.make_pair(
-                XML_Data.make_option(XML_Data.make_long))(
-                XML_Data.make_option(XML_Data.make_long))))))(edits)
+    val arg1 =
+    { import XML_Data.Encode._
+      list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
+
+    val arg2 =
+    { import XML_Data.Encode._
+      list(pair(string, Thy_Header.encode_xml_data))(headers) }
 
     input("Isar_Document.edit_version",
-      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
+      Document.ID(old_id), Document.ID(new_id),
+        YXML.string_of_body(arg1), YXML.string_of_body(arg2))
   }
 }
diff -r d033a34a490a -r 8786e36b8142 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -48,7 +48,7 @@
 }
 
 
-case class Markup_Tree(val branches: Markup_Tree.Branches.T)
+sealed case class Markup_Tree(val branches: Markup_Tree.Branches.T)
 {
   import Markup_Tree._
 
diff -r d033a34a490a -r 8786e36b8142 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -52,7 +52,7 @@
 
   /* information associated with text range */
 
-  case class Info[A](val range: Text.Range, val info: A)
+  sealed case class Info[A](val range: Text.Range, val info: A)
   {
     def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
     def try_restrict(r: Text.Range): Option[Info[A]] =
diff -r d033a34a490a -r 8786e36b8142 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/ROOT.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -127,6 +127,7 @@
 
 use "term_ord.ML";
 use "term_subst.ML";
+use "term_xml.ML";
 use "old_term.ML";
 use "General/name_space.ML";
 use "sorts.ML";
diff -r d033a34a490a -r 8786e36b8142 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -17,7 +17,8 @@
   val ambiguity_level: int Config.T
   val ambiguity_limit: int Config.T
   val read_token: string -> Symbol_Pos.T list * Position.T
-  val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T
+  val parse_token: Proof.context -> (XML.tree list -> 'a) ->
+    Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   val parse_sort: Proof.context -> string -> sort
   val parse_typ: Proof.context -> string -> typ
   val parse_term: Proof.context -> string -> term
@@ -193,11 +194,10 @@
   Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
 
 
-(* read token -- with optional YXML encoding of position *)
+(* outer syntax token -- with optional YXML content *)
 
-fun read_token str =
+fun explode_token tree =
   let
-    val tree = YXML.parse str handle Fail msg => error msg;
     val text = XML.content_of [tree];
     val pos =
       (case tree of
@@ -207,15 +207,26 @@
       | XML.Text _ => Position.none);
   in (Symbol_Pos.explode (text, pos), pos) end;
 
+fun read_token str = explode_token (YXML.parse str handle Fail msg => error msg);
+
+fun parse_token ctxt decode markup parse str =
+  let
+    fun parse_tree tree =
+      let
+        val (syms, pos) = explode_token tree;
+        val _ = Context_Position.report ctxt pos markup;
+      in parse (syms, pos) end;
+  in
+    (case YXML.parse_body str handle Fail msg => error msg of
+      body as [tree as XML.Elem ((name, _), _)] =>
+        if name = Markup.tokenN then parse_tree tree else decode body
+    | [tree as XML.Text _] => parse_tree tree
+    | body => decode body)
+  end;
+
 
 (* (un)parsing *)
 
-fun parse_token ctxt markup str =
-  let
-    val (syms, pos) = read_token str;
-    val _ = Context_Position.report ctxt pos markup;
-  in (syms, pos) end;
-
 val parse_sort = operation #parse_sort;
 val parse_typ = operation #parse_typ;
 val parse_term = operation #parse_term;
diff -r d033a34a490a -r 8786e36b8142 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -320,80 +320,79 @@
   cat_error msg ("Failed to parse " ^ kind ^
     Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
 
-fun parse_sort ctxt text =
-  let
-    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
-    val S =
+fun parse_sort ctxt =
+  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
+    (fn (syms, pos) =>
       parse_raw ctxt "sort" (syms, pos)
       |> report_result ctxt pos
       |> sort_of_term
-      handle ERROR msg => parse_failed ctxt pos msg "sort";
-  in Type.minimize_sort (Proof_Context.tsig_of ctxt) S end;
+      |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
+      handle ERROR msg => parse_failed ctxt pos msg "sort");
 
-fun parse_typ ctxt text =
-  let
-    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
-    val T =
+fun parse_typ ctxt =
+  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
+    (fn (syms, pos) =>
       parse_raw ctxt "type" (syms, pos)
       |> report_result ctxt pos
       |> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) t)
-      handle ERROR msg => parse_failed ctxt pos msg "type";
-  in T end;
+      handle ERROR msg => parse_failed ctxt pos msg "type");
 
-fun parse_term is_prop ctxt text =
+fun parse_term is_prop ctxt =
   let
     val (markup, kind, root, constrain) =
       if is_prop
       then (Markup.prop, "proposition", "prop", Type.constraint propT)
       else (Markup.term, "term", Config.get ctxt Syntax.root, I);
-    val (syms, pos) = Syntax.parse_token ctxt markup text;
+    val decode = constrain o Term_XML.Decode.term;
   in
-    let
-      val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
-      val ambiguity = length (proper_results results);
-
-      val level = Config.get ctxt Syntax.ambiguity_level;
-      val limit = Config.get ctxt Syntax.ambiguity_limit;
+    Syntax.parse_token ctxt decode markup
+      (fn (syms, pos) =>
+        let
+          val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
+          val ambiguity = length (proper_results results);
 
-      val ambig_msg =
-        if ambiguity > 1 andalso ambiguity <= level then
-          ["Got more than one parse tree.\n\
-          \Retry with smaller syntax_ambiguity_level for more information."]
-        else [];
+          val level = Config.get ctxt Syntax.ambiguity_level;
+          val limit = Config.get ctxt Syntax.ambiguity_limit;
 
-      (*brute-force disambiguation via type-inference*)
-      fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
-        handle exn as ERROR _ => Exn.Exn exn;
+          val ambig_msg =
+            if ambiguity > 1 andalso ambiguity <= level then
+              ["Got more than one parse tree.\n\
+              \Retry with smaller syntax_ambiguity_level for more information."]
+            else [];
+
+          (*brute-force disambiguation via type-inference*)
+          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
+            handle exn as ERROR _ => Exn.Exn exn;
 
-      val results' =
-        if ambiguity > 1 then
-          (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
-            check results
-        else results;
-      val reports' = fst (hd results');
+          val results' =
+            if ambiguity > 1 then
+              (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
+                check results
+            else results;
+          val reports' = fst (hd results');
 
-      val errs = map snd (failed_results results');
-      val checked = map snd (proper_results results');
-      val len = length checked;
+          val errs = map snd (failed_results results');
+          val checked = map snd (proper_results results');
+          val len = length checked;
 
-      val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
-    in
-      if len = 0 then
-        report_result ctxt pos
-          [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
-      else if len = 1 then
-        (if ambiguity > level then
-          Context_Position.if_visible ctxt warning
-            "Fortunately, only one parse tree is type correct.\n\
-            \You may still want to disambiguate your grammar or your input."
-        else (); report_result ctxt pos results')
-      else
-        report_result ctxt pos
-          [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
-            (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
-              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-              map show_term (take limit checked))))))]
-    end handle ERROR msg => parse_failed ctxt pos msg kind
+          val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
+        in
+          if len = 0 then
+            report_result ctxt pos
+              [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
+          else if len = 1 then
+            (if ambiguity > level then
+              Context_Position.if_visible ctxt warning
+                "Fortunately, only one parse tree is type correct.\n\
+                \You may still want to disambiguate your grammar or your input."
+            else (); report_result ctxt pos results')
+          else
+            report_result ctxt pos
+              [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
+                (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
+                  (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
+                  map show_term (take limit checked))))))]
+        end handle ERROR msg => parse_failed ctxt pos msg kind)
   end;
 
 
diff -r d033a34a490a -r 8786e36b8142 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -32,7 +32,17 @@
       ('G' : Int) -> Markup.ERROR)
   }
 
-  class Result(val message: XML.Elem)
+  abstract class Message
+
+  class Input(name: String, args: List[String]) extends Message
+  {
+    override def toString: String =
+      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
+        args.map(s =>
+          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
+  }
+
+  class Result(val message: XML.Elem) extends Message
   {
     def kind = message.markup.name
     def properties = message.markup.properties
@@ -377,7 +387,10 @@
     command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
 
   def input(name: String, args: String*): Unit =
+  {
+    receiver ! new Input(name, args.toList)
     input_bytes(name, args.map(Standard_System.string_bytes): _*)
+  }
 
   def close(): Unit = { close(command_input); close(standard_input) }
 }
diff -r d033a34a490a -r 8786e36b8142 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/System/session.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -16,7 +16,7 @@
 
 object Session
 {
-  /* abstract file store */
+  /* file store */
 
   abstract class File_Store
   {
@@ -26,6 +26,7 @@
 
   /* events */
 
+  //{{{
   case object Global_Settings
   case object Perspective
   case object Assignment
@@ -37,6 +38,7 @@
   case object Failed extends Phase
   case object Ready extends Phase
   case object Shutdown extends Phase  // transient
+  //}}}
 }
 
 
@@ -44,33 +46,29 @@
 {
   /* real time parameters */  // FIXME properties or settings (!?)
 
-  // user input (e.g. text edits, cursor movement)
-  val input_delay = Time.seconds(0.3)
-
-  // prover output (markup, common messages)
-  val output_delay = Time.seconds(0.1)
-
-  // GUI layout updates
-  val update_delay = Time.seconds(0.5)
+  val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
+  val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
+  val update_delay = Time.seconds(0.5)  // GUI layout updates
 
 
   /* pervasive event buses */
 
-  val phase_changed = new Event_Bus[Session.Phase]
   val global_settings = new Event_Bus[Session.Global_Settings.type]
-  val raw_messages = new Event_Bus[Isabelle_Process.Result]
-  val commands_changed = new Event_Bus[Session.Commands_Changed]
   val perspective = new Event_Bus[Session.Perspective.type]
   val assignments = new Event_Bus[Session.Assignment.type]
+  val commands_changed = new Event_Bus[Session.Commands_Changed]
+  val phase_changed = new Event_Bus[Session.Phase]
+  val raw_messages = new Event_Bus[Isabelle_Process.Message]
+
 
 
   /** buffered command changes (delay_first discipline) **/
 
+  //{{{
   private case object Stop
 
   private val (_, command_change_buffer) =
     Simple_Thread.actor("command_change_buffer", daemon = true)
-  //{{{
   {
     var changed: Set[Command] = Set()
     var flush_time: Option[Long] = None
@@ -115,7 +113,9 @@
 
   /* global state */
 
-  @volatile var loaded_theories: Set[String] = Set()
+  @volatile var verbose: Boolean = false
+
+  @volatile private var loaded_theories: Set[String] = Set()
 
   @volatile private var syntax = new Outer_Syntax
   def current_syntax(): Outer_Syntax = syntax
@@ -124,16 +124,19 @@
   def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
 
   @volatile private var _phase: Session.Phase = Session.Inactive
-  def phase = _phase
   private def phase_=(new_phase: Session.Phase)
   {
     _phase = new_phase
     phase_changed.event(new_phase)
   }
+  def phase = _phase
   def is_ready: Boolean = phase == Session.Ready
 
   private val global_state = new Volatile(Document.State.init)
-  def current_state(): Document.State = global_state.peek()
+  def current_state(): Document.State = global_state()
+
+  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
+    global_state().snapshot(name, pending_edits)
 
 
   /* theory files */
@@ -158,12 +161,16 @@
 
   /* actor messages */
 
-  private case object Interrupt_Prover
-  private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
+  private case class Start(timeout: Time, args: List[String])
+  private case object Interrupt
   private case class Init_Node(name: String, header: Document.Node.Header, text: String)
-  private case class Start(timeout: Time, args: List[String])
-
-  var verbose: Boolean = false
+  private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
+  private case class Change_Node(
+    name: String,
+    doc_edits: List[Document.Edit_Command],
+    header_edits: List[(String, Thy_Header.Header)],
+    previous: Document.Version,
+    version: Document.Version)
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
@@ -171,60 +178,82 @@
     var prover: Option[Isabelle_Process with Isar_Document] = None
 
 
-    /* document changes */
+    /* incoming edits */
 
-    def handle_change(change: Document.Change)
+    def handle_edits(name: String,
+        header: Document.Node.Header, edits: List[Option[List[Text.Edit]]])
     //{{{
     {
-      val previous = change.previous.get_finished
-      val (node_edits, version) = change.result.get_finished
+      val syntax = current_syntax()
+      val previous = global_state().history.tip.version
+      val doc_edits = edits.map(edit => (name, edit))
+      val result = Future.fork {
+        Thy_Syntax.text_edits(syntax, previous.join, doc_edits, List((name, header)))
+      }
+      val change =
+        global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._3)))
 
-      var former_assignment = global_state.peek().the_assignment(previous).get_finished
+      result.map {
+        case (doc_edits, header_edits, _) =>
+          assignments.await { global_state().is_assigned(previous.get_finished) }
+          this_actor !
+            Change_Node(name, doc_edits, header_edits, previous.join, change.version.join)
+      }
+    }
+    //}}}
+
+
+    /* resulting changes */
+
+    def handle_change(change: Change_Node)
+    //{{{
+    {
+      val previous = change.previous
+      val version = change.version
+      val name = change.name
+      val doc_edits = change.doc_edits
+      val header_edits = change.header_edits
+
+      var former_assignment = global_state().the_assignment(previous).get_finished
       for {
-        (name, Some(cmd_edits)) <- node_edits
+        (name, Some(cmd_edits)) <- doc_edits
         (prev, None) <- cmd_edits
         removed <- previous.nodes(name).commands.get_after(prev)
       } former_assignment -= removed
 
+      def id_command(command: Command): Document.Command_ID =
+      {
+        if (global_state().lookup_command(command.id).isEmpty) {
+          global_state.change(_.define_command(command))
+          prover.get.define_command(command.id, Symbol.encode(command.source))
+        }
+        command.id
+      }
       val id_edits =
-        node_edits map {
-          case (name, None) => (name, None)
-          case (name, Some(cmd_edits)) =>
+        doc_edits map {
+          case (name, edits) =>
             val ids =
-              cmd_edits map {
-                case (c1, c2) =>
-                  val id1 = c1.map(_.id)
-                  val id2 =
-                    c2 match {
-                      case None => None
-                      case Some(command) =>
-                        if (global_state.peek().lookup_command(command.id).isEmpty) {
-                          global_state.change(_.define_command(command))
-                          prover.get.define_command(command.id, Symbol.encode(command.source))
-                        }
-                        Some(command.id)
-                    }
-                  (id1, id2)
-              }
-            (name -> Some(ids))
+              edits.map(_.map { case (c1, c2) => (c1.map(id_command), c2.map(id_command)) })
+            (name, ids)
         }
+
       global_state.change(_.define_version(version, former_assignment))
-      prover.get.edit_version(previous.id, version.id, id_edits)
+      prover.get.edit_version(previous.id, version.id, id_edits, header_edits)
     }
     //}}}
 
 
     /* prover results */
 
-    def bad_result(result: Isabelle_Process.Result)
-    {
-      if (verbose)
-        System.err.println("Ignoring prover result: " + result.message.toString)
-    }
-
     def handle_result(result: Isabelle_Process.Result)
     //{{{
     {
+      def bad_result(result: Isabelle_Process.Result)
+      {
+        if (verbose)
+          System.err.println("Ignoring prover result: " + result.message.toString)
+      }
+
       result.properties match {
         case Position.Id(state_id) =>
           try {
@@ -236,7 +265,7 @@
           if (result.is_syslog) {
             reverse_syslog ::= result.message
             if (result.is_ready) {
-              // FIXME move to ML side
+              // FIXME move to ML side (!?)
               syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
               syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
               phase = Session.Ready
@@ -262,53 +291,16 @@
           }
           else bad_result(result)
         }
-
-      raw_messages.event(result)
-    }
-    //}}}
-
-
-    def edit_version(edits: List[Document.Edit_Text])
-    //{{{
-    {
-      val previous = global_state.peek().history.tip.version
-      val syntax = current_syntax()
-      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, edits) }
-      val change = global_state.change_yield(_.extend_history(previous, edits, result))
-
-      change.version.map(_ => {
-        assignments.await { global_state.peek().is_assigned(previous.get_finished) }
-        this_actor ! change })
     }
     //}}}
 
 
     /* main loop */
 
+    //{{{
     var finished = false
     while (!finished) {
       receive {
-        case Interrupt_Prover =>
-          prover.map(_.interrupt)
-
-        case Edit_Node(name, header, text_edits) if prover.isDefined =>
-          val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
-          edit_version(List((node_name, Some(text_edits))))
-          reply(())
-
-        case Init_Node(name, header, text) if prover.isDefined =>
-          // FIXME compare with existing node
-          val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
-          edit_version(List(
-            (node_name, None),
-            (node_name, Some(List(Text.Edit.insert(0, text))))))
-          reply(())
-
-        case change: Document.Change if prover.isDefined =>
-          handle_change(change)
-
-        case result: Isabelle_Process.Result => handle_result(result)
-
         case Start(timeout, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
@@ -320,37 +312,52 @@
             global_state.change(_ => Document.State.init)  // FIXME event bus!?
             phase = Session.Shutdown
             prover.get.terminate
+            prover = None
             phase = Session.Inactive
           }
           finished = true
           reply(())
 
-        case bad if prover.isDefined =>
-          System.err.println("session_actor: ignoring bad message " + bad)
+        case Interrupt if prover.isDefined =>
+          prover.get.interrupt
+
+        case Init_Node(name, header, text) if prover.isDefined =>
+          // FIXME compare with existing node
+          handle_edits(name, header, List(None, Some(List(Text.Edit.insert(0, text)))))
+          reply(())
+
+        case Edit_Node(name, header, text_edits) if prover.isDefined =>
+          handle_edits(name, header, List(Some(text_edits)))
+          reply(())
+
+        case change: Change_Node if prover.isDefined =>
+          handle_change(change)
+
+        case input: Isabelle_Process.Input =>
+          raw_messages.event(input)
+
+        case result: Isabelle_Process.Result =>
+          handle_result(result)
+          raw_messages.event(result)
+
+        case bad => System.err.println("session_actor: ignoring bad message " + bad)
       }
     }
+    //}}}
   }
 
 
-
-  /** main methods **/
+  /* actions */
 
   def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
 
   def stop() { command_change_buffer !? Stop; session_actor !? Stop }
 
-  def interrupt() { session_actor ! Interrupt_Prover }
-
-  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
-  {
-    session_actor !? Edit_Node(name, header, edits)
-  }
+  def interrupt() { session_actor ! Interrupt }
 
   def init_node(name: String, header: Document.Node.Header, text: String)
-  {
-    session_actor !? Init_Node(name, header, text)
-  }
+  { session_actor !? Init_Node(name, header, text) }
 
-  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
-    global_state.peek().snapshot(name, pending_edits)
+  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
+  { session_actor !? Edit_Node(name, header, edits) }
 }
diff -r d033a34a490a -r 8786e36b8142 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -31,6 +31,13 @@
       Header(f(name), imports.map(f), uses.map(f))
   }
 
+  val encode_xml_data: XML_Data.Encode.T[Header] =
+  {
+    case Header(name, imports, uses) =>
+      import XML_Data.Encode._
+      triple(string, list(string), list(string))(name, imports, uses)
+  }
+
 
   /* file name */
 
diff -r d033a34a490a -r 8786e36b8142 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -99,8 +99,12 @@
 
   /** text edits **/
 
-  def text_edits(syntax: Outer_Syntax, previous: Document.Version,
-      edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
+  def text_edits(
+      syntax: Outer_Syntax,
+      previous: Document.Version,
+      edits: List[Document.Edit_Text],
+      headers: List[(String, Document.Node.Header)])
+    : (List[Document.Edit_Command], List[(String, Thy_Header.Header)], Document.Version) =
   {
     /* phase 1: edit individual command source */
 
@@ -169,10 +173,25 @@
     }
 
 
+    /* node header */
+
+    def node_header(name: String, node: Document.Node)
+        : (List[(String, Thy_Header.Header)], Document.Node.Header) =
+      (node.header.thy_header, headers.find(p => p._1 == name).map(_._2)) match {
+        case (Exn.Res(thy_header0), Some(header @ Document.Node.Header(_, Exn.Res(thy_header))))
+        if thy_header0 != thy_header =>
+          (List((name, thy_header)), header)
+        case (Exn.Exn(_), Some(header @ Document.Node.Header(_, Exn.Res(thy_header)))) =>
+          (List((name, thy_header)), header)
+        case _ => (Nil, node.header)
+      }
+
+
     /* resulting document edits */
 
     {
       val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
+      val header_edits = new mutable.ListBuffer[(String, Thy_Header.Header)]
       var nodes = previous.nodes
 
       edits foreach {
@@ -194,9 +213,13 @@
             inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
           doc_edits += (name -> Some(cmd_edits))
-          nodes += (name -> new Document.Node(node.header, commands2))
+
+          val (new_headers, new_header) = node_header(name, node)
+          header_edits ++= new_headers
+
+          nodes += (name -> Document.Node(new_header, node.blobs, commands2))
       }
-      (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
+      (doc_edits.toList, header_edits.toList, Document.Version(Document.new_id(), nodes))
     }
   }
 }
diff -r d033a34a490a -r 8786e36b8142 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -139,8 +139,8 @@
           |> (if rem_dups then cons ("rem_dups", "") else I)
           |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
       in
-        XML.Elem (("Query", properties), XML_Data.make_list 
-          (XML_Data.make_pair XML_Data.make_bool (single o xml_of_criterion)) criteria)
+        XML.Elem (("Query", properties), XML_Data.Encode.list
+          (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
       end
   | xml_of_query _ = raise Fail "cannot serialize goal";
 
@@ -148,8 +148,9 @@
       let
         val rem_dups = Properties.defined properties "rem_dups";
         val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
-        val criteria = XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_bool 
-          (criterion_of_xml o the_single)) body;
+        val criteria =
+          XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
+            (criterion_of_xml o the_single)) body;
       in
         {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
       end
@@ -189,12 +190,12 @@
     val properties =
       if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
   in
-    XML.Elem (("Result", properties), XML_Data.make_list (single o xml_of_theorem) theorems)
+    XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
   end;
 
 fun result_of_xml (XML.Elem (("Result", properties), body)) =
       (Properties.get properties "found" |> Option.map Markup.parse_int,
-       XML_Data.dest_list (theorem_of_xml o the_single) body)
+       XML_Data.Decode.list (theorem_of_xml o the_single) body)
   | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
 
 fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
diff -r d033a34a490a -r 8786e36b8142 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Pure/build-jars	Sun Jul 10 21:46:41 2011 +0200
@@ -30,6 +30,7 @@
   Isar/outer_syntax.scala
   Isar/parse.scala
   Isar/token.scala
+  PIDE/blob.scala
   PIDE/command.scala
   PIDE/document.scala
   PIDE/isar_document.scala
@@ -56,6 +57,7 @@
   Thy/thy_syntax.scala
   library.scala
   package.scala
+  term.scala
 )
 
 
diff -r d033a34a490a -r 8786e36b8142 src/Pure/term.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/term.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -0,0 +1,91 @@
+/*  Title:      Pure/term.scala
+    Author:     Makarius
+
+Lambda terms with XML data representation.
+
+Note: Isabelle/ML is the primary environment for logical operations.
+*/
+
+package isabelle
+
+
+object Term
+{
+  /* basic type definitions */
+
+  type Indexname = (String, Int)
+
+  type Sort = List[String]
+  val dummyS: Sort = List("")
+
+  sealed abstract class Typ
+  case class Type(name: String, args: List[Typ] = Nil) extends Typ
+  case class TFree(name: String, sort: Sort = dummyS) extends Typ
+  case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ
+  val dummyT = Type("dummy")
+
+  sealed abstract class Term
+  case class Const(name: String, typ: Typ = dummyT) extends Term
+  case class Free(name: String, typ: Typ = dummyT) extends Term
+  case class Var(name: Indexname, typ: Typ = dummyT) extends Term
+  case class Bound(index: Int) extends Term
+  case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
+  case class App(fun: Term, arg: Term) extends Term
+}
+
+
+object Term_XML
+{
+  import Term._
+
+
+  /* XML data representation */
+
+  object Encode
+  {
+    import XML_Data.Encode._
+
+    val indexname: T[Indexname] = pair(string, int)
+
+    val sort: T[Sort] = list(string)
+
+    def typ: T[Typ] =
+      variant[Typ](List(
+        { case Type(a, b) => pair(string, list(typ))((a, b)) },
+        { case TFree(a, b) => pair(string, sort)((a, b)) },
+        { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
+
+    def term: T[Term] =
+      variant[Term](List(
+        { case Const(a, b) => pair(string, typ)((a, b)) },
+        { case Free(a, b) => pair(string, typ)((a, b)) },
+        { case Var(a, b) => pair(indexname, typ)((a, b)) },
+        { case Bound(a) => int(a) },
+        { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
+        { case App(a, b) => pair(term, term)((a, b)) }))
+  }
+
+  object Decode
+  {
+    import XML_Data.Decode._
+
+    val indexname: T[Indexname] = pair(string, int)
+
+    val sort: T[Sort] = list(string)
+
+    def typ: T[Typ] =
+      variant[Typ](List(
+        (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
+        (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
+        (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
+
+    def term: T[Term] =
+      variant[Term](List(
+        (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
+        (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
+        (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
+        (x => Bound(int(x))),
+        (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
+        (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
+  }
+}
diff -r d033a34a490a -r 8786e36b8142 src/Pure/term_xml.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/term_xml.ML	Sun Jul 10 21:46:41 2011 +0200
@@ -0,0 +1,78 @@
+(*  Title:      Pure/term_xml.ML
+    Author:     Makarius
+
+XML data representation of lambda terms.
+*)
+
+signature TERM_XML_OPS =
+sig
+  type 'a T
+  val indexname: indexname T
+  val sort: sort T
+  val typ: typ T
+  val term: term T
+end
+
+signature TERM_XML =
+sig
+  structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
+  structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
+end;
+
+structure Term_XML: TERM_XML =
+struct
+
+(* encode *)
+
+structure Encode =
+struct
+
+open XML_Data.Encode;
+
+val indexname = pair string int;
+
+val sort = list string;
+
+fun typ T = T |> variant
+ [fn Type x => pair string (list typ) x,
+  fn TFree x => pair string sort x,
+  fn TVar x => pair indexname sort x];
+
+fun term t = t |> variant
+ [fn Const x => pair string typ x,
+  fn Free x => pair string typ x,
+  fn Var x => pair indexname typ x,
+  fn Bound x => int x,
+  fn Abs x => triple string typ term x,
+  fn op $ x => pair term term x];
+
+end;
+
+
+(* decode *)
+
+structure Decode =
+struct
+
+open XML_Data.Decode;
+
+val indexname = pair string int;
+
+val sort = list string;
+
+fun typ T = T |> variant
+ [Type o pair string (list typ),
+  TFree o pair string sort,
+  TVar o pair indexname sort];
+
+fun term t = t |> variant
+ [Const o pair string typ,
+  Free o pair string typ,
+  Var o pair indexname typ,
+  Bound o int,
+  Abs o triple string typ term,
+  op $ o pair term term];
+
+end;
+
+end;
diff -r d033a34a490a -r 8786e36b8142 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -61,8 +61,10 @@
 {
   /* pending text edits */
 
+  private val node_name = (master_dir + Path.basic(thy_name)).implode
+
   private def node_header(): Document.Node.Header =
-    new Document.Node.Header(master_dir,
+    Document.Node.Header(Path.current,  // FIXME master_dir (!?)
       Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
 
   private object pending_edits  // owned by Swing thread
@@ -77,14 +79,14 @@
         case Nil =>
         case edits =>
           pending.clear
-          session.edit_node(thy_name, node_header(), edits)
+          session.edit_node(node_name, node_header(), edits)
       }
     }
 
     def init()
     {
       flush()
-      session.init_node(thy_name, node_header(), Isabelle.buffer_text(buffer))
+      session.init_node(node_name, node_header(), Isabelle.buffer_text(buffer))
     }
 
     private val delay_flush =
@@ -104,7 +106,6 @@
   def snapshot(): Document.Snapshot =
   {
     Swing_Thread.require()
-    val node_name = (master_dir + Path.basic(thy_name)).implode  // FIXME
     session.snapshot(node_name, pending_edits.snapshot())
   }
 
diff -r d033a34a490a -r 8786e36b8142 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -105,7 +105,7 @@
 
   /* text area ranges */
 
-  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
+  sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int)
 
   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   {
diff -r d033a34a490a -r 8786e36b8142 src/Tools/jEdit/src/protocol_dockable.scala
--- a/src/Tools/jEdit/src/protocol_dockable.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -28,6 +28,9 @@
   private val main_actor = actor {
     loop {
       react {
+        case input: Isabelle_Process.Input =>
+          Swing_Thread.now { text_area.append(input.toString + "\n") }
+
         case result: Isabelle_Process.Result =>
           Swing_Thread.now { text_area.append(result.message.toString + "\n") }
 
diff -r d033a34a490a -r 8786e36b8142 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -30,6 +30,8 @@
   private val main_actor = actor {
     loop {
       react {
+        case input: Isabelle_Process.Input =>
+
         case result: Isabelle_Process.Result =>
           if (result.is_stdout)
             Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
diff -r d033a34a490a -r 8786e36b8142 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sun Jul 10 21:39:03 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Jul 10 21:46:41 2011 +0200
@@ -76,6 +76,8 @@
   private val main_actor = actor {
     loop {
       react {
+        case input: Isabelle_Process.Input =>
+
         case result: Isabelle_Process.Result =>
           if (result.is_syslog)
             Swing_Thread.now {