merged;
authorwenzelm
Sun Jul 10 21:46:41 2011 +0200 (2011-07-10)
changeset 437438786e36b8142
parent 43742 d033a34a490a
parent 43731 70072780e095
child 43744 2c7e1565b4a3
child 43757 17c36f05b40d
merged;
NEWS
     1.1 --- a/NEWS	Sun Jul 10 21:39:03 2011 +0200
     1.2 +++ b/NEWS	Sun Jul 10 21:46:41 2011 +0200
     1.3 @@ -149,6 +149,12 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* The inner syntax of sort/type/term/prop supports inlined YXML
     1.8 +representations within quoted string tokens.  By encoding logical
     1.9 +entities via Term_XML (in ML or Scala) concrete syntax can be
    1.10 +bypassed, which is particularly useful for producing bits of text
    1.11 +under external program control.
    1.12 +
    1.13  * Antiquotations for ML and document preparation are managed as theory
    1.14  data, which requires explicit setup.
    1.15  
     2.1 --- a/src/Pure/Concurrent/synchronized.ML	Sun Jul 10 21:39:03 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/synchronized.ML	Sun Jul 10 21:46:41 2011 +0200
     2.3 @@ -71,11 +71,11 @@
     2.4  
     2.5  fun counter () =
     2.6    let
     2.7 -    val counter = var "counter" 0;
     2.8 +    val counter = var "counter" (0: int);
     2.9      fun next () =
    2.10        change_result counter
    2.11          (fn i =>
    2.12 -          let val j = i + 1
    2.13 +          let val j = i + (1: int)
    2.14            in (j, j) end);
    2.15    in next end;
    2.16  
     3.1 --- a/src/Pure/Concurrent/synchronized_sequential.ML	Sun Jul 10 21:39:03 2011 +0200
     3.2 +++ b/src/Pure/Concurrent/synchronized_sequential.ML	Sun Jul 10 21:46:41 2011 +0200
     3.3 @@ -27,11 +27,11 @@
     3.4  
     3.5  fun counter () =
     3.6    let
     3.7 -    val counter = var "counter" 0;
     3.8 +    val counter = var "counter" (0: int);
     3.9      fun next () =
    3.10        change_result counter
    3.11          (fn i =>
    3.12 -          let val j = i + 1
    3.13 +          let val j = i + (1: int)
    3.14            in (j, j) end);
    3.15    in next end;
    3.16  
     4.1 --- a/src/Pure/Concurrent/volatile.scala	Sun Jul 10 21:39:03 2011 +0200
     4.2 +++ b/src/Pure/Concurrent/volatile.scala	Sun Jul 10 21:46:41 2011 +0200
     4.3 @@ -10,7 +10,7 @@
     4.4  class Volatile[A](init: A)
     4.5  {
     4.6    @volatile private var state: A = init
     4.7 -  def peek(): A = state
     4.8 +  def apply(): A = state
     4.9    def change(f: A => A) { state = f(state) }
    4.10    def change_yield[B](f: A => (B, A)): B =
    4.11    {
     5.1 --- a/src/Pure/General/markup.scala	Sun Jul 10 21:39:03 2011 +0200
     5.2 +++ b/src/Pure/General/markup.scala	Sun Jul 10 21:46:41 2011 +0200
     5.3 @@ -302,6 +302,12 @@
     5.4    val EDIT = "edit"
     5.5  
     5.6  
     5.7 +  /* prover process */
     5.8 +
     5.9 +  val PROVER_COMMAND = "prover_command"
    5.10 +  val PROVER_ARG = "prover_arg"
    5.11 +
    5.12 +
    5.13    /* messages */
    5.14  
    5.15    val Serial = new Long_Property("serial")
     6.1 --- a/src/Pure/General/pretty.scala	Sun Jul 10 21:39:03 2011 +0200
     6.2 +++ b/src/Pure/General/pretty.scala	Sun Jul 10 21:46:41 2011 +0200
     6.3 @@ -53,7 +53,7 @@
     6.4            Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
     6.5      }
     6.6  
     6.7 -  case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
     6.8 +  sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
     6.9    {
    6.10      def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
    6.11      def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
     7.1 --- a/src/Pure/General/sha1.scala	Sun Jul 10 21:39:03 2011 +0200
     7.2 +++ b/src/Pure/General/sha1.scala	Sun Jul 10 21:46:41 2011 +0200
     7.3 @@ -12,7 +12,7 @@
     7.4  
     7.5  object SHA1
     7.6  {
     7.7 -  case class Digest(rep: String)
     7.8 +  sealed case class Digest(rep: String)
     7.9    {
    7.10      override def toString: String = rep
    7.11    }
     8.1 --- a/src/Pure/General/symbol.scala	Sun Jul 10 21:39:03 2011 +0200
     8.2 +++ b/src/Pure/General/symbol.scala	Sun Jul 10 21:46:41 2011 +0200
     8.3 @@ -120,7 +120,7 @@
     8.4  
     8.5    class Index(text: CharSequence)
     8.6    {
     8.7 -    case class Entry(chr: Int, sym: Int)
     8.8 +    sealed case class Entry(chr: Int, sym: Int)
     8.9      val index: Array[Entry] =
    8.10      {
    8.11        val matcher = new Matcher(text)
     9.1 --- a/src/Pure/General/xml_data.ML	Sun Jul 10 21:39:03 2011 +0200
     9.2 +++ b/src/Pure/General/xml_data.ML	Sun Jul 10 21:46:41 2011 +0200
     9.3 @@ -4,139 +4,151 @@
     9.4  XML as basic data representation language.
     9.5  *)
     9.6  
     9.7 +signature XML_DATA_OPS =
     9.8 +sig
     9.9 +  type 'a T
    9.10 +  val properties: Properties.T T
    9.11 +  val string: string T
    9.12 +  val int: int T
    9.13 +  val bool: bool T
    9.14 +  val unit: unit T
    9.15 +  val pair: 'a T -> 'b T -> ('a * 'b) T
    9.16 +  val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
    9.17 +  val list: 'a T -> 'a list T
    9.18 +  val option: 'a T -> 'a option T
    9.19 +  val variant: 'a T list -> 'a T
    9.20 +end;
    9.21 +
    9.22  signature XML_DATA =
    9.23  sig
    9.24 +  structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body
    9.25    exception XML_ATOM of string
    9.26    exception XML_BODY of XML.body
    9.27 -  val make_properties: Properties.T -> XML.body
    9.28 -  val dest_properties: XML.body -> Properties.T
    9.29 -  val make_string: string -> XML.body
    9.30 -  val dest_string : XML.body -> string
    9.31 -  val make_int: int -> XML.body
    9.32 -  val dest_int : XML.body -> int
    9.33 -  val make_bool: bool -> XML.body
    9.34 -  val dest_bool: XML.body -> bool
    9.35 -  val make_unit: unit -> XML.body
    9.36 -  val dest_unit: XML.body -> unit
    9.37 -  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
    9.38 -  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
    9.39 -  val make_triple:
    9.40 -    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
    9.41 -  val dest_triple:
    9.42 -    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
    9.43 -  val make_list: ('a -> XML.body) -> 'a list -> XML.body
    9.44 -  val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
    9.45 -  val make_option: ('a -> XML.body) -> 'a option -> XML.body
    9.46 -  val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
    9.47 -  val make_variant: ('a -> XML.body) list -> 'a -> XML.body
    9.48 -  val dest_variant: (XML.body -> 'a) list -> XML.body -> 'a
    9.49 +  structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a
    9.50  end;
    9.51  
    9.52  structure XML_Data: XML_DATA =
    9.53  struct
    9.54  
    9.55 -(* basic values *)
    9.56 -
    9.57 -exception XML_ATOM of string;
    9.58 -
    9.59 +(** encode **)
    9.60  
    9.61 -fun make_int_atom i = signed_string_of_int i;
    9.62 +structure Encode =
    9.63 +struct
    9.64  
    9.65 -fun dest_int_atom s =
    9.66 -  (case Int.fromString s of
    9.67 -    SOME i => i
    9.68 -  | NONE => raise XML_ATOM s);
    9.69 +type 'a T = 'a -> XML.body;
    9.70  
    9.71  
    9.72 -fun make_bool_atom false = "0"
    9.73 -  | make_bool_atom true = "1";
    9.74 +(* basic values *)
    9.75 +
    9.76 +fun int_atom i = signed_string_of_int i;
    9.77  
    9.78 -fun dest_bool_atom "0" = false
    9.79 -  | dest_bool_atom "1" = true
    9.80 -  | dest_bool_atom s = raise XML_ATOM s;
    9.81 -
    9.82 +fun bool_atom false = "0"
    9.83 +  | bool_atom true = "1";
    9.84  
    9.85 -fun make_unit_atom () = "";
    9.86 -
    9.87 -fun dest_unit_atom "" = ()
    9.88 -  | dest_unit_atom s = raise XML_ATOM s;
    9.89 +fun unit_atom () = "";
    9.90  
    9.91  
    9.92  (* structural nodes *)
    9.93  
    9.94 -exception XML_BODY of XML.tree list;
    9.95 -
    9.96 -fun make_node ts = XML.Elem ((":", []), ts);
    9.97 +fun node ts = XML.Elem ((":", []), ts);
    9.98  
    9.99 -fun dest_node (XML.Elem ((":", []), ts)) = ts
   9.100 -  | dest_node t = raise XML_BODY [t];
   9.101 -
   9.102 -fun make_tagged (tag, ts) = XML.Elem ((make_int_atom tag, []), ts);
   9.103 -
   9.104 -fun dest_tagged (XML.Elem ((s, []), ts)) = (dest_int_atom s, ts)
   9.105 -  | dest_tagged t = raise XML_BODY [t];
   9.106 +fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
   9.107  
   9.108  
   9.109  (* representation of standard types *)
   9.110  
   9.111 -fun make_properties props = [XML.Elem ((":", props), [])];
   9.112 -
   9.113 -fun dest_properties [XML.Elem ((":", props), [])] = props
   9.114 -  | dest_properties ts = raise XML_BODY ts;
   9.115 -
   9.116 +fun properties props = [XML.Elem ((":", props), [])];
   9.117  
   9.118 -fun make_string "" = []
   9.119 -  | make_string s = [XML.Text s];
   9.120 -
   9.121 -fun dest_string [] = ""
   9.122 -  | dest_string [XML.Text s] = s
   9.123 -  | dest_string ts = raise XML_BODY ts;
   9.124 -
   9.125 +fun string "" = []
   9.126 +  | string s = [XML.Text s];
   9.127  
   9.128 -val make_int = make_string o make_int_atom;
   9.129 -val dest_int = dest_int_atom o dest_string;
   9.130 -
   9.131 -val make_bool = make_string o make_bool_atom;
   9.132 -val dest_bool = dest_bool_atom o dest_string;
   9.133 +val int = string o int_atom;
   9.134  
   9.135 -val make_unit = make_string o make_unit_atom;
   9.136 -val dest_unit = dest_unit_atom o dest_string;
   9.137 -
   9.138 +val bool = string o bool_atom;
   9.139  
   9.140 -fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
   9.141 -
   9.142 -fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
   9.143 -  | dest_pair _ _ ts = raise XML_BODY ts;
   9.144 +val unit = string o unit_atom;
   9.145  
   9.146 -
   9.147 -fun make_triple make1 make2 make3 (x, y, z) =
   9.148 -  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
   9.149 +fun pair f g (x, y) = [node (f x), node (g y)];
   9.150  
   9.151 -fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
   9.152 -      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
   9.153 -  | dest_triple _ _ _ ts = raise XML_BODY ts;
   9.154 -
   9.155 -
   9.156 -fun make_list make xs = map (make_node o make) xs;
   9.157 -
   9.158 -fun dest_list dest ts = map (dest o dest_node) ts;
   9.159 -
   9.160 +fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
   9.161  
   9.162 -fun make_option _ NONE = []
   9.163 -  | make_option make (SOME x) = [make_node (make x)];
   9.164 -
   9.165 -fun dest_option _ [] = NONE
   9.166 -  | dest_option dest [t] = SOME (dest (dest_node t))
   9.167 -  | dest_option _ ts = raise XML_BODY ts;
   9.168 -
   9.169 +fun list f xs = map (node o f) xs;
   9.170  
   9.171 -fun make_variant makes x =
   9.172 -  [make_tagged (the (get_index (fn make => try make x) makes))];
   9.173 +fun option _ NONE = []
   9.174 +  | option f (SOME x) = [node (f x)];
   9.175  
   9.176 -fun dest_variant dests [t] =
   9.177 -      let val (tag, ts) = dest_tagged t
   9.178 -      in nth dests tag ts end
   9.179 -  | dest_variant _ ts = raise XML_BODY ts;
   9.180 +fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
   9.181  
   9.182  end;
   9.183  
   9.184 +
   9.185 +
   9.186 +(** decode **)
   9.187 +
   9.188 +exception XML_ATOM of string;
   9.189 +exception XML_BODY of XML.tree list;
   9.190 +
   9.191 +structure Decode =
   9.192 +struct
   9.193 +
   9.194 +type 'a T = XML.body -> 'a;
   9.195 +
   9.196 +
   9.197 +(* basic values *)
   9.198 +
   9.199 +fun int_atom s =
   9.200 +  (case Int.fromString s of
   9.201 +    SOME i => i
   9.202 +  | NONE => raise XML_ATOM s);
   9.203 +
   9.204 +fun bool_atom "0" = false
   9.205 +  | bool_atom "1" = true
   9.206 +  | bool_atom s = raise XML_ATOM s;
   9.207 +
   9.208 +fun unit_atom "" = ()
   9.209 +  | unit_atom s = raise XML_ATOM s;
   9.210 +
   9.211 +
   9.212 +(* structural nodes *)
   9.213 +
   9.214 +fun node (XML.Elem ((":", []), ts)) = ts
   9.215 +  | node t = raise XML_BODY [t];
   9.216 +
   9.217 +fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts)
   9.218 +  | tagged t = raise XML_BODY [t];
   9.219 +
   9.220 +
   9.221 +(* representation of standard types *)
   9.222 +
   9.223 +fun properties [XML.Elem ((":", props), [])] = props
   9.224 +  | properties ts = raise XML_BODY ts;
   9.225 +
   9.226 +fun string [] = ""
   9.227 +  | string [XML.Text s] = s
   9.228 +  | string ts = raise XML_BODY ts;
   9.229 +
   9.230 +val int = int_atom o string;
   9.231 +
   9.232 +val bool = bool_atom o string;
   9.233 +
   9.234 +val unit = unit_atom o string;
   9.235 +
   9.236 +fun pair f g [t1, t2] = (f (node t1), g (node t2))
   9.237 +  | pair _ _ ts = raise XML_BODY ts;
   9.238 +
   9.239 +fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
   9.240 +  | triple _ _ _ ts = raise XML_BODY ts;
   9.241 +
   9.242 +fun list f ts = map (f o node) ts;
   9.243 +
   9.244 +fun option _ [] = NONE
   9.245 +  | option f [t] = SOME (f (node t))
   9.246 +  | option _ ts = raise XML_BODY ts;
   9.247 +
   9.248 +fun variant fs [t] = uncurry (nth fs) (tagged t)
   9.249 +  | variant _ ts = raise XML_BODY ts;
   9.250 +
   9.251 +end;
   9.252 +
   9.253 +end;
   9.254 +
    10.1 --- a/src/Pure/General/xml_data.scala	Sun Jul 10 21:39:03 2011 +0200
    10.2 +++ b/src/Pure/General/xml_data.scala	Sun Jul 10 21:46:41 2011 +0200
    10.3 @@ -10,150 +10,167 @@
    10.4  
    10.5  object XML_Data
    10.6  {
    10.7 -  /* basic values */
    10.8 -
    10.9 -  class XML_Atom(s: String) extends Exception(s)
   10.10 -
   10.11 +  /** encode **/
   10.12  
   10.13 -  private def make_long_atom(i: Long): String = i.toString
   10.14 -
   10.15 -  private def dest_long_atom(s: String): Long =
   10.16 -    try { java.lang.Long.parseLong(s) }
   10.17 -    catch { case e: NumberFormatException => throw new XML_Atom(s) }
   10.18 +  object Encode
   10.19 +  {
   10.20 +    type T[A] = A => XML.Body
   10.21  
   10.22  
   10.23 -  private def make_int_atom(i: Int): String = i.toString
   10.24 +    /* basic values */
   10.25 +
   10.26 +    private def long_atom(i: Long): String = i.toString
   10.27  
   10.28 -  private def dest_int_atom(s: String): Int =
   10.29 -    try { Integer.parseInt(s) }
   10.30 -    catch { case e: NumberFormatException => throw new XML_Atom(s) }
   10.31 +    private def int_atom(i: Int): String = i.toString
   10.32 +
   10.33 +    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
   10.34 +
   10.35 +    private def unit_atom(u: Unit) = ""
   10.36  
   10.37  
   10.38 -  private def make_bool_atom(b: Boolean): String = if (b) "1" else "0"
   10.39 +    /* structural nodes */
   10.40  
   10.41 -  private def dest_bool_atom(s: String): Boolean =
   10.42 -    if (s == "1") true
   10.43 -    else if (s == "0") false
   10.44 -    else throw new XML_Atom(s)
   10.45 +    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
   10.46  
   10.47 -
   10.48 -  private def make_unit_atom(u: Unit) = ""
   10.49 -
   10.50 -  private def dest_unit_atom(s: String): Unit =
   10.51 -    if (s == "") () else throw new XML_Atom(s)
   10.52 +    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
   10.53 +      XML.Elem(Markup(int_atom(tag), Nil), ts)
   10.54  
   10.55  
   10.56 -  /* structural nodes */
   10.57 +    /* representation of standard types */
   10.58 +
   10.59 +    val properties: T[List[(String, String)]] =
   10.60 +      (props => List(XML.Elem(Markup(":", props), Nil)))
   10.61  
   10.62 -  class XML_Body(body: XML.Body) extends Exception
   10.63 +    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
   10.64 +
   10.65 +    val long: T[Long] = (x => string(long_atom(x)))
   10.66 +
   10.67 +    val int: T[Int] = (x => string(int_atom(x)))
   10.68 +
   10.69 +    val bool: T[Boolean] = (x => string(bool_atom(x)))
   10.70  
   10.71 -  private def make_node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
   10.72 +    val unit: T[Unit] = (x => string(unit_atom(x)))
   10.73 +
   10.74 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   10.75 +      (x => List(node(f(x._1)), node(g(x._2))))
   10.76 +
   10.77 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   10.78 +      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
   10.79  
   10.80 -  private def dest_node(t: XML.Tree): XML.Body =
   10.81 -    t match {
   10.82 -      case XML.Elem(Markup(":", Nil), ts) => ts
   10.83 -      case _ => throw new XML_Body(List(t))
   10.84 +    def list[A](f: T[A]): T[List[A]] =
   10.85 +      (xs => xs.map((x: A) => node(f(x))))
   10.86 +
   10.87 +    def option[A](f: T[A]): T[Option[A]] =
   10.88 +    {
   10.89 +      case None => Nil
   10.90 +      case Some(x) => List(node(f(x)))
   10.91      }
   10.92  
   10.93 -  private def make_tagged(tag: Int, ts: XML.Body): XML.Tree =
   10.94 -    XML.Elem(Markup(make_int_atom(tag), Nil), ts)
   10.95 +    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
   10.96 +    {
   10.97 +      case x =>
   10.98 +        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
   10.99 +        List(tagged(tag, f(x)))
  10.100 +    }
  10.101 +  }
  10.102 +
  10.103  
  10.104 -  private def dest_tagged(t: XML.Tree): (Int, XML.Body) =
  10.105 -    t match {
  10.106 -      case XML.Elem(Markup(s, Nil), ts) => (dest_int_atom(s), ts)
  10.107 -      case _ => throw new XML_Body(List(t))
  10.108 -    }
  10.109 +
  10.110 +  /** decode **/
  10.111 +
  10.112 +  class XML_Atom(s: String) extends Exception(s)
  10.113 +  class XML_Body(body: XML.Body) extends Exception
  10.114 +
  10.115 +  object Decode
  10.116 +  {
  10.117 +    type T[A] = XML.Body => A
  10.118  
  10.119  
  10.120 -  /* representation of standard types */
  10.121 +     /* basic values */
  10.122 +
  10.123 +    private def long_atom(s: String): Long =
  10.124 +      try { java.lang.Long.parseLong(s) }
  10.125 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  10.126  
  10.127 -  def make_properties(props: List[(String, String)]): XML.Body =
  10.128 -    List(XML.Elem(Markup(":", props), Nil))
  10.129 +    private def int_atom(s: String): Int =
  10.130 +      try { Integer.parseInt(s) }
  10.131 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  10.132 +
  10.133 +    private def bool_atom(s: String): Boolean =
  10.134 +      if (s == "1") true
  10.135 +      else if (s == "0") false
  10.136 +      else throw new XML_Atom(s)
  10.137 +
  10.138 +    private def unit_atom(s: String): Unit =
  10.139 +      if (s == "") () else throw new XML_Atom(s)
  10.140 +
  10.141  
  10.142 -  def dest_properties(ts: XML.Body): List[(String, String)] =
  10.143 -    ts match {
  10.144 +    /* structural nodes */
  10.145 +
  10.146 +    private def node(t: XML.Tree): XML.Body =
  10.147 +      t match {
  10.148 +        case XML.Elem(Markup(":", Nil), ts) => ts
  10.149 +        case _ => throw new XML_Body(List(t))
  10.150 +      }
  10.151 +
  10.152 +    private def tagged(t: XML.Tree): (Int, XML.Body) =
  10.153 +      t match {
  10.154 +        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
  10.155 +        case _ => throw new XML_Body(List(t))
  10.156 +      }
  10.157 +
  10.158 +
  10.159 +    /* representation of standard types */
  10.160 +
  10.161 +    val properties: T[List[(String, String)]] =
  10.162 +    {
  10.163        case List(XML.Elem(Markup(":", props), Nil)) => props
  10.164 -      case _ => throw new XML_Body(ts)
  10.165 +      case ts => throw new XML_Body(ts)
  10.166      }
  10.167  
  10.168 -
  10.169 -  def make_string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
  10.170 -
  10.171 -  def dest_string(ts: XML.Body): String =
  10.172 -    ts match {
  10.173 +    val string: T[String] =
  10.174 +    {
  10.175        case Nil => ""
  10.176        case List(XML.Text(s)) => s
  10.177 -      case _ => throw new XML_Body(ts)
  10.178 +      case ts => throw new XML_Body(ts)
  10.179      }
  10.180  
  10.181 -
  10.182 -  def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
  10.183 -  def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
  10.184 +    val long: T[Long] = (x => long_atom(string(x)))
  10.185  
  10.186 -  def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
  10.187 -  def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
  10.188 +    val int: T[Int] = (x => int_atom(string(x)))
  10.189  
  10.190 -  def make_bool(b: Boolean): XML.Body = make_string(make_bool_atom(b))
  10.191 -  def dest_bool(ts: XML.Body) = dest_bool_atom(dest_string(ts))
  10.192 +    val bool: T[Boolean] = (x => bool_atom(string(x)))
  10.193  
  10.194 -  def make_unit(u: Unit): XML.Body = make_string(make_unit_atom(u))
  10.195 -  def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
  10.196 -
  10.197 +    val unit: T[Unit] = (x => unit_atom(string(x)))
  10.198  
  10.199 -  def make_pair[A, B](make1: A => XML.Body)(make2: B => XML.Body)(p: (A, B)): XML.Body =
  10.200 -    List(make_node(make1(p._1)), make_node(make2(p._2)))
  10.201 -
  10.202 -  def dest_pair[A, B](dest1: XML.Body => A)(dest2: XML.Body => B)(ts: XML.Body): (A, B) =
  10.203 -    ts match {
  10.204 -      case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
  10.205 -      case _ => throw new XML_Body(ts)
  10.206 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
  10.207 +    {
  10.208 +      case List(t1, t2) => (f(node(t1)), g(node(t2)))
  10.209 +      case ts => throw new XML_Body(ts)
  10.210      }
  10.211  
  10.212 -
  10.213 -  def make_triple[A, B, C](make1: A => XML.Body)(make2: B => XML.Body)(make3: C => XML.Body)
  10.214 -      (p: (A, B, C)): XML.Body =
  10.215 -    List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
  10.216 -
  10.217 -  def dest_triple[A, B, C](dest1: XML.Body => A)(dest2: XML.Body => B)(dest3: XML.Body => C)
  10.218 -      (ts: XML.Body): (A, B, C) =
  10.219 -    ts match {
  10.220 -      case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
  10.221 -      case _ => throw new XML_Body(ts)
  10.222 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
  10.223 +    {
  10.224 +      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
  10.225 +      case ts => throw new XML_Body(ts)
  10.226      }
  10.227  
  10.228 -
  10.229 -  def make_list[A](make: A => XML.Body)(xs: List[A]): XML.Body =
  10.230 -    xs.map((x: A) => make_node(make(x)))
  10.231 +    def list[A](f: T[A]): T[List[A]] =
  10.232 +      (ts => ts.map(t => f(node(t))))
  10.233  
  10.234 -  def dest_list[A](dest: XML.Body => A)(ts: XML.Body): List[A] =
  10.235 -    ts.map((t: XML.Tree) => dest(dest_node(t)))
  10.236 -
  10.237 -
  10.238 -  def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
  10.239 -    opt match {
  10.240 -      case None => Nil
  10.241 -      case Some(x) => List(make_node(make(x)))
  10.242 +    def option[A](f: T[A]): T[Option[A]] =
  10.243 +    {
  10.244 +      case Nil => None
  10.245 +      case List(t) => Some(f(node(t)))
  10.246 +      case ts => throw new XML_Body(ts)
  10.247      }
  10.248  
  10.249 -  def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
  10.250 -    ts match {
  10.251 -      case Nil => None
  10.252 -      case List(t) => Some(dest(dest_node(t)))
  10.253 -      case _ => throw new XML_Body(ts)
  10.254 +    def variant[A](fs: List[T[A]]): T[A] =
  10.255 +    {
  10.256 +      case List(t) =>
  10.257 +        val (tag, ts) = tagged(t)
  10.258 +        fs(tag)(ts)
  10.259 +      case ts => throw new XML_Body(ts)
  10.260      }
  10.261 -
  10.262 -
  10.263 -  def make_variant[A](makes: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
  10.264 -  {
  10.265 -    val (make, tag) = makes.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
  10.266 -    List(make_tagged(tag, make(x)))
  10.267    }
  10.268 -
  10.269 -  def dest_variant[A](dests: List[XML.Body => A])(ts: XML.Body): A =
  10.270 -    ts match {
  10.271 -      case List(t) =>
  10.272 -        val (tag, ts) = dest_tagged(t)
  10.273 -        dests(tag)(ts)
  10.274 -      case _ => throw new XML_Body(ts)
  10.275 -    }
  10.276  }
    11.1 --- a/src/Pure/General/yxml.ML	Sun Jul 10 21:39:03 2011 +0200
    11.2 +++ b/src/Pure/General/yxml.ML	Sun Jul 10 21:46:41 2011 +0200
    11.3 @@ -16,8 +16,10 @@
    11.4  signature YXML =
    11.5  sig
    11.6    val escape_controls: string -> string
    11.7 +  val detect: string -> bool
    11.8    val output_markup: Markup.T -> string * string
    11.9    val element: string -> XML.attributes -> string list -> string
   11.10 +  val string_of_body: XML.body -> string
   11.11    val string_of: XML.tree -> string
   11.12    val parse_body: string -> XML.body
   11.13    val parse: string -> XML.tree
   11.14 @@ -48,6 +50,8 @@
   11.15  val XY = X ^ Y;
   11.16  val XYX = XY ^ X;
   11.17  
   11.18 +val detect = exists_string (fn s => s = X);
   11.19 +
   11.20  
   11.21  (* output *)
   11.22  
   11.23 @@ -59,17 +63,20 @@
   11.24    let val (pre, post) = output_markup (name, atts)
   11.25    in pre ^ implode body ^ post end;
   11.26  
   11.27 -fun string_of t =
   11.28 +fun string_of_body body =
   11.29    let
   11.30      fun attrib (a, x) =
   11.31        Buffer.add Y #>
   11.32        Buffer.add a #> Buffer.add "=" #> Buffer.add x;
   11.33      fun tree (XML.Elem ((name, atts), ts)) =
   11.34            Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
   11.35 -          fold tree ts #>
   11.36 +          trees ts #>
   11.37            Buffer.add XYX
   11.38 -      | tree (XML.Text s) = Buffer.add s;
   11.39 -  in Buffer.empty |> tree t |> Buffer.content end;
   11.40 +      | tree (XML.Text s) = Buffer.add s
   11.41 +    and trees ts = fold tree ts;
   11.42 +  in Buffer.empty |> trees body |> Buffer.content end;
   11.43 +
   11.44 +val string_of = string_of_body o single;
   11.45  
   11.46  
   11.47  
    12.1 --- a/src/Pure/IsaMakefile	Sun Jul 10 21:39:03 2011 +0200
    12.2 +++ b/src/Pure/IsaMakefile	Sun Jul 10 21:46:41 2011 +0200
    12.3 @@ -250,6 +250,7 @@
    12.4    term.ML						\
    12.5    term_ord.ML						\
    12.6    term_subst.ML						\
    12.7 +  term_xml.ML						\
    12.8    theory.ML						\
    12.9    thm.ML						\
   12.10    type.ML						\
    13.1 --- a/src/Pure/Isar/token.ML	Sun Jul 10 21:39:03 2011 +0200
    13.2 +++ b/src/Pure/Isar/token.ML	Sun Jul 10 21:46:41 2011 +0200
    13.3 @@ -180,8 +180,9 @@
    13.4  
    13.5  (* token content *)
    13.6  
    13.7 -fun source_of (Token ((source, (pos, _)), _, _)) =
    13.8 -  YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
    13.9 +fun source_of (Token ((source, (pos, _)), (_, x), _)) =
   13.10 +  if YXML.detect x then x
   13.11 +  else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
   13.12  
   13.13  fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
   13.14  
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Pure/PIDE/blob.scala	Sun Jul 10 21:46:41 2011 +0200
    14.3 @@ -0,0 +1,28 @@
    14.4 +/*  Title:      Pure/PIDE/blob.scala
    14.5 +    Author:     Makarius
    14.6 +
    14.7 +Unidentified text with markup.
    14.8 +*/
    14.9 +
   14.10 +package isabelle
   14.11 +
   14.12 +
   14.13 +object Blob
   14.14 +{
   14.15 +  sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
   14.16 +  {
   14.17 +    def + (info: Text.Info[Any]): State = copy(markup = markup + info)
   14.18 +  }
   14.19 +}
   14.20 +
   14.21 +
   14.22 +sealed case class Blob(val source: String)
   14.23 +{
   14.24 +  def source(range: Text.Range): String = source.substring(range.start, range.stop)
   14.25 +
   14.26 +  lazy val symbol_index = new Symbol.Index(source)
   14.27 +  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
   14.28 +  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
   14.29 +
   14.30 +  val empty_state: Blob.State = Blob.State(this)
   14.31 +}
    15.1 --- a/src/Pure/PIDE/command.scala	Sun Jul 10 21:39:03 2011 +0200
    15.2 +++ b/src/Pure/PIDE/command.scala	Sun Jul 10 21:46:41 2011 +0200
    15.3 @@ -16,7 +16,7 @@
    15.4  {
    15.5    /** accumulated results from prover **/
    15.6  
    15.7 -  case class State(
    15.8 +  sealed case class State(
    15.9      val command: Command,
   15.10      val status: List[Markup] = Nil,
   15.11      val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
    16.1 --- a/src/Pure/PIDE/document.ML	Sun Jul 10 21:39:03 2011 +0200
    16.2 +++ b/src/Pure/PIDE/document.ML	Sun Jul 10 21:46:41 2011 +0200
    16.3 @@ -16,12 +16,14 @@
    16.4    val parse_id: string -> id
    16.5    val print_id: id -> string
    16.6    type edit = string * ((command_id option * command_id option) list) option
    16.7 +  type header = string * (string * string list * string list)
    16.8    type state
    16.9    val init_state: state
   16.10    val get_theory: state -> version_id -> Position.T -> string -> theory
   16.11    val cancel_execution: state -> unit -> unit
   16.12    val define_command: command_id -> string -> state -> state
   16.13 -  val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   16.14 +  val edit: version_id -> version_id -> edit list -> header list ->
   16.15 +    state -> (command_id * exec_id) list * state
   16.16    val execute: version_id -> state -> state
   16.17    val state: unit -> state
   16.18    val change_state: (state -> state) -> unit
   16.19 @@ -78,6 +80,8 @@
   16.20    (*NONE: remove node, SOME: insert/remove commands*)
   16.21    ((command_id option * command_id option) list) option;
   16.22  
   16.23 +type header = string * (string * string list * string list);
   16.24 +
   16.25  fun the_entry (Node {entries, ...}) id =
   16.26    (case Entries.lookup entries id of
   16.27      NONE => err_undef "command entry" id
   16.28 @@ -309,8 +313,10 @@
   16.29  
   16.30  in
   16.31  
   16.32 -fun edit (old_id: version_id) (new_id: version_id) edits state =
   16.33 +fun edit (old_id: version_id) (new_id: version_id) edits headers state =
   16.34    let
   16.35 +    (* FIXME apply headers *)
   16.36 +
   16.37      val old_version = the_version state old_id;
   16.38      val _ = Time.now ();  (* FIXME odd workaround *)
   16.39      val new_version = fold edit_nodes edits old_version;
    17.1 --- a/src/Pure/PIDE/document.scala	Sun Jul 10 21:39:03 2011 +0200
    17.2 +++ b/src/Pure/PIDE/document.scala	Sun Jul 10 21:46:41 2011 +0200
    17.3 @@ -46,10 +46,10 @@
    17.4  
    17.5    object Node
    17.6    {
    17.7 -    class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
    17.8 -    val empty_header = new Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
    17.9 +    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
   17.10 +    val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
   17.11  
   17.12 -    val empty: Node = new Node(empty_header, Linear_Set())
   17.13 +    val empty: Node = Node(empty_header, Map(), Linear_Set())
   17.14  
   17.15      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
   17.16        : Iterator[(Command, Text.Offset)] =
   17.17 @@ -65,13 +65,11 @@
   17.18  
   17.19    private val block_size = 1024
   17.20  
   17.21 -  class Node(val header: Node.Header, val commands: Linear_Set[Command])
   17.22 +  sealed case class Node(
   17.23 +    val header: Node.Header,
   17.24 +    val blobs: Map[String, Blob],
   17.25 +    val commands: Linear_Set[Command])
   17.26    {
   17.27 -    /* header */
   17.28 -
   17.29 -    def set_header(header: Node.Header): Node = new Node(header, commands)
   17.30 -
   17.31 -
   17.32      /* commands */
   17.33  
   17.34      private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
   17.35 @@ -132,25 +130,24 @@
   17.36  
   17.37    object Version
   17.38    {
   17.39 -    val init: Version = new Version(no_id, Map().withDefaultValue(Node.empty))
   17.40 +    val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
   17.41    }
   17.42  
   17.43 -  class Version(val id: Version_ID, val nodes: Map[String, Node])
   17.44 +  sealed case class Version(val id: Version_ID, val nodes: Map[String, Node])
   17.45  
   17.46  
   17.47    /* changes of plain text, eventually resulting in document edits */
   17.48  
   17.49    object Change
   17.50    {
   17.51 -    val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init))
   17.52 +    val init = Change(Future.value(Version.init), Nil, Future.value(Version.init))
   17.53    }
   17.54  
   17.55 -  class Change(
   17.56 +  sealed case class Change(
   17.57      val previous: Future[Version],
   17.58      val edits: List[Edit_Text],
   17.59 -    val result: Future[(List[Edit_Command], Version)])
   17.60 +    val version: Future[Version])
   17.61    {
   17.62 -    val version: Future[Version] = result.map(_._2)
   17.63      def is_finished: Boolean = previous.is_finished && version.is_finished
   17.64    }
   17.65  
   17.66 @@ -209,11 +206,11 @@
   17.67      }
   17.68    }
   17.69  
   17.70 -  case class State(
   17.71 +  sealed case class State(
   17.72      val versions: Map[Version_ID, Version] = Map(),
   17.73      val commands: Map[Command_ID, Command.State] = Map(),
   17.74      val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
   17.75 -    val assignments: Map[Version, State.Assignment] = Map(),
   17.76 +    val assignments: Map[Version_ID, State.Assignment] = Map(),
   17.77      val disposed: Set[ID] = Set(),  // FIXME unused!?
   17.78      val history: History = History.init)
   17.79    {
   17.80 @@ -224,7 +221,7 @@
   17.81        val id = version.id
   17.82        if (versions.isDefinedAt(id) || disposed(id)) fail
   17.83        copy(versions = versions + (id -> version),
   17.84 -        assignments = assignments + (version -> State.Assignment(former_assignment)))
   17.85 +        assignments = assignments + (id -> State.Assignment(former_assignment)))
   17.86      }
   17.87  
   17.88      def define_command(command: Command): State =
   17.89 @@ -239,7 +236,8 @@
   17.90      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
   17.91      def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
   17.92      def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
   17.93 -    def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
   17.94 +    def the_assignment(version: Version): State.Assignment =
   17.95 +      assignments.getOrElse(version.id, fail)
   17.96  
   17.97      def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
   17.98        execs.get(id) match {
   17.99 @@ -269,22 +267,21 @@
  17.100            (st.command, exec_id)
  17.101          }
  17.102        val new_assignment = the_assignment(version).assign(assigned_execs)
  17.103 -      val new_state =
  17.104 -        copy(assignments = assignments + (version -> new_assignment), execs = new_execs)
  17.105 +      val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
  17.106        (assigned_execs.map(_._1), new_state)
  17.107      }
  17.108  
  17.109      def is_assigned(version: Version): Boolean =
  17.110 -      assignments.get(version) match {
  17.111 +      assignments.get(version.id) match {
  17.112          case Some(assgn) => assgn.is_finished
  17.113          case None => false
  17.114        }
  17.115  
  17.116      def extend_history(previous: Future[Version],
  17.117          edits: List[Edit_Text],
  17.118 -        result: Future[(List[Edit_Command], Version)]): (Change, State) =
  17.119 +        version: Future[Version]): (Change, State) =
  17.120      {
  17.121 -      val change = new Change(previous, edits, result)
  17.122 +      val change = Change(previous, edits, version)
  17.123        (change, copy(history = history + change))
  17.124      }
  17.125  
    18.1 --- a/src/Pure/PIDE/isar_document.ML	Sun Jul 10 21:39:03 2011 +0200
    18.2 +++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 21:46:41 2011 +0200
    18.3 @@ -13,22 +13,19 @@
    18.4  
    18.5  val _ =
    18.6    Isabelle_Process.add_command "Isar_Document.edit_version"
    18.7 -    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    18.8 +    (fn [old_id_string, new_id_string, edits_yxml, headers_yxml] => Document.change_state (fn state =>
    18.9        let
   18.10          val old_id = Document.parse_id old_id_string;
   18.11          val new_id = Document.parse_id new_id_string;
   18.12 -        val edits =
   18.13 -          XML_Data.dest_list
   18.14 -            (XML_Data.dest_pair
   18.15 -              XML_Data.dest_string
   18.16 -              (XML_Data.dest_option
   18.17 -                (XML_Data.dest_list
   18.18 -                  (XML_Data.dest_pair
   18.19 -                    (XML_Data.dest_option XML_Data.dest_int)
   18.20 -                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
   18.21 +        val edits = YXML.parse_body edits_yxml |>
   18.22 +          let open XML_Data.Decode
   18.23 +          in list (pair string (option (list (pair (option int) (option int))))) end;
   18.24 +        val headers = YXML.parse_body headers_yxml |>
   18.25 +          let open XML_Data.Decode
   18.26 +          in list (pair string (triple string (list string) (list string))) end;
   18.27  
   18.28        val await_cancellation = Document.cancel_execution state;
   18.29 -      val (updates, state') = Document.edit old_id new_id edits state;
   18.30 +      val (updates, state') = Document.edit old_id new_id edits headers state;
   18.31        val _ = await_cancellation ();
   18.32        val _ =
   18.33          Output.status (Markup.markup (Markup.assign new_id)
    19.1 --- a/src/Pure/PIDE/isar_document.scala	Sun Jul 10 21:39:03 2011 +0200
    19.2 +++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 21:46:41 2011 +0200
    19.3 @@ -140,17 +140,18 @@
    19.4    /* document versions */
    19.5  
    19.6    def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
    19.7 -      edits: List[Document.Edit_Command_ID])
    19.8 +      edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
    19.9    {
   19.10 -    val arg =
   19.11 -      XML_Data.make_list(
   19.12 -        XML_Data.make_pair(XML_Data.make_string)(
   19.13 -          XML_Data.make_option(XML_Data.make_list(
   19.14 -              XML_Data.make_pair(
   19.15 -                XML_Data.make_option(XML_Data.make_long))(
   19.16 -                XML_Data.make_option(XML_Data.make_long))))))(edits)
   19.17 +    val arg1 =
   19.18 +    { import XML_Data.Encode._
   19.19 +      list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
   19.20 +
   19.21 +    val arg2 =
   19.22 +    { import XML_Data.Encode._
   19.23 +      list(pair(string, Thy_Header.encode_xml_data))(headers) }
   19.24  
   19.25      input("Isar_Document.edit_version",
   19.26 -      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
   19.27 +      Document.ID(old_id), Document.ID(new_id),
   19.28 +        YXML.string_of_body(arg1), YXML.string_of_body(arg2))
   19.29    }
   19.30  }
    20.1 --- a/src/Pure/PIDE/markup_tree.scala	Sun Jul 10 21:39:03 2011 +0200
    20.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sun Jul 10 21:46:41 2011 +0200
    20.3 @@ -48,7 +48,7 @@
    20.4  }
    20.5  
    20.6  
    20.7 -case class Markup_Tree(val branches: Markup_Tree.Branches.T)
    20.8 +sealed case class Markup_Tree(val branches: Markup_Tree.Branches.T)
    20.9  {
   20.10    import Markup_Tree._
   20.11  
    21.1 --- a/src/Pure/PIDE/text.scala	Sun Jul 10 21:39:03 2011 +0200
    21.2 +++ b/src/Pure/PIDE/text.scala	Sun Jul 10 21:46:41 2011 +0200
    21.3 @@ -52,7 +52,7 @@
    21.4  
    21.5    /* information associated with text range */
    21.6  
    21.7 -  case class Info[A](val range: Text.Range, val info: A)
    21.8 +  sealed case class Info[A](val range: Text.Range, val info: A)
    21.9    {
   21.10      def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
   21.11      def try_restrict(r: Text.Range): Option[Info[A]] =
    22.1 --- a/src/Pure/ROOT.ML	Sun Jul 10 21:39:03 2011 +0200
    22.2 +++ b/src/Pure/ROOT.ML	Sun Jul 10 21:46:41 2011 +0200
    22.3 @@ -127,6 +127,7 @@
    22.4  
    22.5  use "term_ord.ML";
    22.6  use "term_subst.ML";
    22.7 +use "term_xml.ML";
    22.8  use "old_term.ML";
    22.9  use "General/name_space.ML";
   22.10  use "sorts.ML";
    23.1 --- a/src/Pure/Syntax/syntax.ML	Sun Jul 10 21:39:03 2011 +0200
    23.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Jul 10 21:46:41 2011 +0200
    23.3 @@ -17,7 +17,8 @@
    23.4    val ambiguity_level: int Config.T
    23.5    val ambiguity_limit: int Config.T
    23.6    val read_token: string -> Symbol_Pos.T list * Position.T
    23.7 -  val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T
    23.8 +  val parse_token: Proof.context -> (XML.tree list -> 'a) ->
    23.9 +    Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   23.10    val parse_sort: Proof.context -> string -> sort
   23.11    val parse_typ: Proof.context -> string -> typ
   23.12    val parse_term: Proof.context -> string -> term
   23.13 @@ -193,11 +194,10 @@
   23.14    Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
   23.15  
   23.16  
   23.17 -(* read token -- with optional YXML encoding of position *)
   23.18 +(* outer syntax token -- with optional YXML content *)
   23.19  
   23.20 -fun read_token str =
   23.21 +fun explode_token tree =
   23.22    let
   23.23 -    val tree = YXML.parse str handle Fail msg => error msg;
   23.24      val text = XML.content_of [tree];
   23.25      val pos =
   23.26        (case tree of
   23.27 @@ -207,15 +207,26 @@
   23.28        | XML.Text _ => Position.none);
   23.29    in (Symbol_Pos.explode (text, pos), pos) end;
   23.30  
   23.31 +fun read_token str = explode_token (YXML.parse str handle Fail msg => error msg);
   23.32 +
   23.33 +fun parse_token ctxt decode markup parse str =
   23.34 +  let
   23.35 +    fun parse_tree tree =
   23.36 +      let
   23.37 +        val (syms, pos) = explode_token tree;
   23.38 +        val _ = Context_Position.report ctxt pos markup;
   23.39 +      in parse (syms, pos) end;
   23.40 +  in
   23.41 +    (case YXML.parse_body str handle Fail msg => error msg of
   23.42 +      body as [tree as XML.Elem ((name, _), _)] =>
   23.43 +        if name = Markup.tokenN then parse_tree tree else decode body
   23.44 +    | [tree as XML.Text _] => parse_tree tree
   23.45 +    | body => decode body)
   23.46 +  end;
   23.47 +
   23.48  
   23.49  (* (un)parsing *)
   23.50  
   23.51 -fun parse_token ctxt markup str =
   23.52 -  let
   23.53 -    val (syms, pos) = read_token str;
   23.54 -    val _ = Context_Position.report ctxt pos markup;
   23.55 -  in (syms, pos) end;
   23.56 -
   23.57  val parse_sort = operation #parse_sort;
   23.58  val parse_typ = operation #parse_typ;
   23.59  val parse_term = operation #parse_term;
    24.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sun Jul 10 21:39:03 2011 +0200
    24.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sun Jul 10 21:46:41 2011 +0200
    24.3 @@ -320,80 +320,79 @@
    24.4    cat_error msg ("Failed to parse " ^ kind ^
    24.5      Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
    24.6  
    24.7 -fun parse_sort ctxt text =
    24.8 -  let
    24.9 -    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
   24.10 -    val S =
   24.11 +fun parse_sort ctxt =
   24.12 +  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
   24.13 +    (fn (syms, pos) =>
   24.14        parse_raw ctxt "sort" (syms, pos)
   24.15        |> report_result ctxt pos
   24.16        |> sort_of_term
   24.17 -      handle ERROR msg => parse_failed ctxt pos msg "sort";
   24.18 -  in Type.minimize_sort (Proof_Context.tsig_of ctxt) S end;
   24.19 +      |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
   24.20 +      handle ERROR msg => parse_failed ctxt pos msg "sort");
   24.21  
   24.22 -fun parse_typ ctxt text =
   24.23 -  let
   24.24 -    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
   24.25 -    val T =
   24.26 +fun parse_typ ctxt =
   24.27 +  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
   24.28 +    (fn (syms, pos) =>
   24.29        parse_raw ctxt "type" (syms, pos)
   24.30        |> report_result ctxt pos
   24.31        |> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) t)
   24.32 -      handle ERROR msg => parse_failed ctxt pos msg "type";
   24.33 -  in T end;
   24.34 +      handle ERROR msg => parse_failed ctxt pos msg "type");
   24.35  
   24.36 -fun parse_term is_prop ctxt text =
   24.37 +fun parse_term is_prop ctxt =
   24.38    let
   24.39      val (markup, kind, root, constrain) =
   24.40        if is_prop
   24.41        then (Markup.prop, "proposition", "prop", Type.constraint propT)
   24.42        else (Markup.term, "term", Config.get ctxt Syntax.root, I);
   24.43 -    val (syms, pos) = Syntax.parse_token ctxt markup text;
   24.44 +    val decode = constrain o Term_XML.Decode.term;
   24.45    in
   24.46 -    let
   24.47 -      val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
   24.48 -      val ambiguity = length (proper_results results);
   24.49 -
   24.50 -      val level = Config.get ctxt Syntax.ambiguity_level;
   24.51 -      val limit = Config.get ctxt Syntax.ambiguity_limit;
   24.52 +    Syntax.parse_token ctxt decode markup
   24.53 +      (fn (syms, pos) =>
   24.54 +        let
   24.55 +          val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
   24.56 +          val ambiguity = length (proper_results results);
   24.57  
   24.58 -      val ambig_msg =
   24.59 -        if ambiguity > 1 andalso ambiguity <= level then
   24.60 -          ["Got more than one parse tree.\n\
   24.61 -          \Retry with smaller syntax_ambiguity_level for more information."]
   24.62 -        else [];
   24.63 +          val level = Config.get ctxt Syntax.ambiguity_level;
   24.64 +          val limit = Config.get ctxt Syntax.ambiguity_limit;
   24.65  
   24.66 -      (*brute-force disambiguation via type-inference*)
   24.67 -      fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
   24.68 -        handle exn as ERROR _ => Exn.Exn exn;
   24.69 +          val ambig_msg =
   24.70 +            if ambiguity > 1 andalso ambiguity <= level then
   24.71 +              ["Got more than one parse tree.\n\
   24.72 +              \Retry with smaller syntax_ambiguity_level for more information."]
   24.73 +            else [];
   24.74 +
   24.75 +          (*brute-force disambiguation via type-inference*)
   24.76 +          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
   24.77 +            handle exn as ERROR _ => Exn.Exn exn;
   24.78  
   24.79 -      val results' =
   24.80 -        if ambiguity > 1 then
   24.81 -          (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
   24.82 -            check results
   24.83 -        else results;
   24.84 -      val reports' = fst (hd results');
   24.85 +          val results' =
   24.86 +            if ambiguity > 1 then
   24.87 +              (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
   24.88 +                check results
   24.89 +            else results;
   24.90 +          val reports' = fst (hd results');
   24.91  
   24.92 -      val errs = map snd (failed_results results');
   24.93 -      val checked = map snd (proper_results results');
   24.94 -      val len = length checked;
   24.95 +          val errs = map snd (failed_results results');
   24.96 +          val checked = map snd (proper_results results');
   24.97 +          val len = length checked;
   24.98  
   24.99 -      val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
  24.100 -    in
  24.101 -      if len = 0 then
  24.102 -        report_result ctxt pos
  24.103 -          [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
  24.104 -      else if len = 1 then
  24.105 -        (if ambiguity > level then
  24.106 -          Context_Position.if_visible ctxt warning
  24.107 -            "Fortunately, only one parse tree is type correct.\n\
  24.108 -            \You may still want to disambiguate your grammar or your input."
  24.109 -        else (); report_result ctxt pos results')
  24.110 -      else
  24.111 -        report_result ctxt pos
  24.112 -          [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
  24.113 -            (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
  24.114 -              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
  24.115 -              map show_term (take limit checked))))))]
  24.116 -    end handle ERROR msg => parse_failed ctxt pos msg kind
  24.117 +          val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
  24.118 +        in
  24.119 +          if len = 0 then
  24.120 +            report_result ctxt pos
  24.121 +              [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
  24.122 +          else if len = 1 then
  24.123 +            (if ambiguity > level then
  24.124 +              Context_Position.if_visible ctxt warning
  24.125 +                "Fortunately, only one parse tree is type correct.\n\
  24.126 +                \You may still want to disambiguate your grammar or your input."
  24.127 +            else (); report_result ctxt pos results')
  24.128 +          else
  24.129 +            report_result ctxt pos
  24.130 +              [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
  24.131 +                (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
  24.132 +                  (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
  24.133 +                  map show_term (take limit checked))))))]
  24.134 +        end handle ERROR msg => parse_failed ctxt pos msg kind)
  24.135    end;
  24.136  
  24.137  
    25.1 --- a/src/Pure/System/isabelle_process.scala	Sun Jul 10 21:39:03 2011 +0200
    25.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Jul 10 21:46:41 2011 +0200
    25.3 @@ -32,7 +32,17 @@
    25.4        ('G' : Int) -> Markup.ERROR)
    25.5    }
    25.6  
    25.7 -  class Result(val message: XML.Elem)
    25.8 +  abstract class Message
    25.9 +
   25.10 +  class Input(name: String, args: List[String]) extends Message
   25.11 +  {
   25.12 +    override def toString: String =
   25.13 +      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
   25.14 +        args.map(s =>
   25.15 +          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
   25.16 +  }
   25.17 +
   25.18 +  class Result(val message: XML.Elem) extends Message
   25.19    {
   25.20      def kind = message.markup.name
   25.21      def properties = message.markup.properties
   25.22 @@ -377,7 +387,10 @@
   25.23      command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
   25.24  
   25.25    def input(name: String, args: String*): Unit =
   25.26 +  {
   25.27 +    receiver ! new Input(name, args.toList)
   25.28      input_bytes(name, args.map(Standard_System.string_bytes): _*)
   25.29 +  }
   25.30  
   25.31    def close(): Unit = { close(command_input); close(standard_input) }
   25.32  }
    26.1 --- a/src/Pure/System/session.scala	Sun Jul 10 21:39:03 2011 +0200
    26.2 +++ b/src/Pure/System/session.scala	Sun Jul 10 21:46:41 2011 +0200
    26.3 @@ -16,7 +16,7 @@
    26.4  
    26.5  object Session
    26.6  {
    26.7 -  /* abstract file store */
    26.8 +  /* file store */
    26.9  
   26.10    abstract class File_Store
   26.11    {
   26.12 @@ -26,6 +26,7 @@
   26.13  
   26.14    /* events */
   26.15  
   26.16 +  //{{{
   26.17    case object Global_Settings
   26.18    case object Perspective
   26.19    case object Assignment
   26.20 @@ -37,6 +38,7 @@
   26.21    case object Failed extends Phase
   26.22    case object Ready extends Phase
   26.23    case object Shutdown extends Phase  // transient
   26.24 +  //}}}
   26.25  }
   26.26  
   26.27  
   26.28 @@ -44,33 +46,29 @@
   26.29  {
   26.30    /* real time parameters */  // FIXME properties or settings (!?)
   26.31  
   26.32 -  // user input (e.g. text edits, cursor movement)
   26.33 -  val input_delay = Time.seconds(0.3)
   26.34 -
   26.35 -  // prover output (markup, common messages)
   26.36 -  val output_delay = Time.seconds(0.1)
   26.37 -
   26.38 -  // GUI layout updates
   26.39 -  val update_delay = Time.seconds(0.5)
   26.40 +  val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
   26.41 +  val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
   26.42 +  val update_delay = Time.seconds(0.5)  // GUI layout updates
   26.43  
   26.44  
   26.45    /* pervasive event buses */
   26.46  
   26.47 -  val phase_changed = new Event_Bus[Session.Phase]
   26.48    val global_settings = new Event_Bus[Session.Global_Settings.type]
   26.49 -  val raw_messages = new Event_Bus[Isabelle_Process.Result]
   26.50 -  val commands_changed = new Event_Bus[Session.Commands_Changed]
   26.51    val perspective = new Event_Bus[Session.Perspective.type]
   26.52    val assignments = new Event_Bus[Session.Assignment.type]
   26.53 +  val commands_changed = new Event_Bus[Session.Commands_Changed]
   26.54 +  val phase_changed = new Event_Bus[Session.Phase]
   26.55 +  val raw_messages = new Event_Bus[Isabelle_Process.Message]
   26.56 +
   26.57  
   26.58  
   26.59    /** buffered command changes (delay_first discipline) **/
   26.60  
   26.61 +  //{{{
   26.62    private case object Stop
   26.63  
   26.64    private val (_, command_change_buffer) =
   26.65      Simple_Thread.actor("command_change_buffer", daemon = true)
   26.66 -  //{{{
   26.67    {
   26.68      var changed: Set[Command] = Set()
   26.69      var flush_time: Option[Long] = None
   26.70 @@ -115,7 +113,9 @@
   26.71  
   26.72    /* global state */
   26.73  
   26.74 -  @volatile var loaded_theories: Set[String] = Set()
   26.75 +  @volatile var verbose: Boolean = false
   26.76 +
   26.77 +  @volatile private var loaded_theories: Set[String] = Set()
   26.78  
   26.79    @volatile private var syntax = new Outer_Syntax
   26.80    def current_syntax(): Outer_Syntax = syntax
   26.81 @@ -124,16 +124,19 @@
   26.82    def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
   26.83  
   26.84    @volatile private var _phase: Session.Phase = Session.Inactive
   26.85 -  def phase = _phase
   26.86    private def phase_=(new_phase: Session.Phase)
   26.87    {
   26.88      _phase = new_phase
   26.89      phase_changed.event(new_phase)
   26.90    }
   26.91 +  def phase = _phase
   26.92    def is_ready: Boolean = phase == Session.Ready
   26.93  
   26.94    private val global_state = new Volatile(Document.State.init)
   26.95 -  def current_state(): Document.State = global_state.peek()
   26.96 +  def current_state(): Document.State = global_state()
   26.97 +
   26.98 +  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
   26.99 +    global_state().snapshot(name, pending_edits)
  26.100  
  26.101  
  26.102    /* theory files */
  26.103 @@ -158,12 +161,16 @@
  26.104  
  26.105    /* actor messages */
  26.106  
  26.107 -  private case object Interrupt_Prover
  26.108 -  private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
  26.109 +  private case class Start(timeout: Time, args: List[String])
  26.110 +  private case object Interrupt
  26.111    private case class Init_Node(name: String, header: Document.Node.Header, text: String)
  26.112 -  private case class Start(timeout: Time, args: List[String])
  26.113 -
  26.114 -  var verbose: Boolean = false
  26.115 +  private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
  26.116 +  private case class Change_Node(
  26.117 +    name: String,
  26.118 +    doc_edits: List[Document.Edit_Command],
  26.119 +    header_edits: List[(String, Thy_Header.Header)],
  26.120 +    previous: Document.Version,
  26.121 +    version: Document.Version)
  26.122  
  26.123    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
  26.124    {
  26.125 @@ -171,60 +178,82 @@
  26.126      var prover: Option[Isabelle_Process with Isar_Document] = None
  26.127  
  26.128  
  26.129 -    /* document changes */
  26.130 +    /* incoming edits */
  26.131  
  26.132 -    def handle_change(change: Document.Change)
  26.133 +    def handle_edits(name: String,
  26.134 +        header: Document.Node.Header, edits: List[Option[List[Text.Edit]]])
  26.135      //{{{
  26.136      {
  26.137 -      val previous = change.previous.get_finished
  26.138 -      val (node_edits, version) = change.result.get_finished
  26.139 +      val syntax = current_syntax()
  26.140 +      val previous = global_state().history.tip.version
  26.141 +      val doc_edits = edits.map(edit => (name, edit))
  26.142 +      val result = Future.fork {
  26.143 +        Thy_Syntax.text_edits(syntax, previous.join, doc_edits, List((name, header)))
  26.144 +      }
  26.145 +      val change =
  26.146 +        global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._3)))
  26.147  
  26.148 -      var former_assignment = global_state.peek().the_assignment(previous).get_finished
  26.149 +      result.map {
  26.150 +        case (doc_edits, header_edits, _) =>
  26.151 +          assignments.await { global_state().is_assigned(previous.get_finished) }
  26.152 +          this_actor !
  26.153 +            Change_Node(name, doc_edits, header_edits, previous.join, change.version.join)
  26.154 +      }
  26.155 +    }
  26.156 +    //}}}
  26.157 +
  26.158 +
  26.159 +    /* resulting changes */
  26.160 +
  26.161 +    def handle_change(change: Change_Node)
  26.162 +    //{{{
  26.163 +    {
  26.164 +      val previous = change.previous
  26.165 +      val version = change.version
  26.166 +      val name = change.name
  26.167 +      val doc_edits = change.doc_edits
  26.168 +      val header_edits = change.header_edits
  26.169 +
  26.170 +      var former_assignment = global_state().the_assignment(previous).get_finished
  26.171        for {
  26.172 -        (name, Some(cmd_edits)) <- node_edits
  26.173 +        (name, Some(cmd_edits)) <- doc_edits
  26.174          (prev, None) <- cmd_edits
  26.175          removed <- previous.nodes(name).commands.get_after(prev)
  26.176        } former_assignment -= removed
  26.177  
  26.178 +      def id_command(command: Command): Document.Command_ID =
  26.179 +      {
  26.180 +        if (global_state().lookup_command(command.id).isEmpty) {
  26.181 +          global_state.change(_.define_command(command))
  26.182 +          prover.get.define_command(command.id, Symbol.encode(command.source))
  26.183 +        }
  26.184 +        command.id
  26.185 +      }
  26.186        val id_edits =
  26.187 -        node_edits map {
  26.188 -          case (name, None) => (name, None)
  26.189 -          case (name, Some(cmd_edits)) =>
  26.190 +        doc_edits map {
  26.191 +          case (name, edits) =>
  26.192              val ids =
  26.193 -              cmd_edits map {
  26.194 -                case (c1, c2) =>
  26.195 -                  val id1 = c1.map(_.id)
  26.196 -                  val id2 =
  26.197 -                    c2 match {
  26.198 -                      case None => None
  26.199 -                      case Some(command) =>
  26.200 -                        if (global_state.peek().lookup_command(command.id).isEmpty) {
  26.201 -                          global_state.change(_.define_command(command))
  26.202 -                          prover.get.define_command(command.id, Symbol.encode(command.source))
  26.203 -                        }
  26.204 -                        Some(command.id)
  26.205 -                    }
  26.206 -                  (id1, id2)
  26.207 -              }
  26.208 -            (name -> Some(ids))
  26.209 +              edits.map(_.map { case (c1, c2) => (c1.map(id_command), c2.map(id_command)) })
  26.210 +            (name, ids)
  26.211          }
  26.212 +
  26.213        global_state.change(_.define_version(version, former_assignment))
  26.214 -      prover.get.edit_version(previous.id, version.id, id_edits)
  26.215 +      prover.get.edit_version(previous.id, version.id, id_edits, header_edits)
  26.216      }
  26.217      //}}}
  26.218  
  26.219  
  26.220      /* prover results */
  26.221  
  26.222 -    def bad_result(result: Isabelle_Process.Result)
  26.223 -    {
  26.224 -      if (verbose)
  26.225 -        System.err.println("Ignoring prover result: " + result.message.toString)
  26.226 -    }
  26.227 -
  26.228      def handle_result(result: Isabelle_Process.Result)
  26.229      //{{{
  26.230      {
  26.231 +      def bad_result(result: Isabelle_Process.Result)
  26.232 +      {
  26.233 +        if (verbose)
  26.234 +          System.err.println("Ignoring prover result: " + result.message.toString)
  26.235 +      }
  26.236 +
  26.237        result.properties match {
  26.238          case Position.Id(state_id) =>
  26.239            try {
  26.240 @@ -236,7 +265,7 @@
  26.241            if (result.is_syslog) {
  26.242              reverse_syslog ::= result.message
  26.243              if (result.is_ready) {
  26.244 -              // FIXME move to ML side
  26.245 +              // FIXME move to ML side (!?)
  26.246                syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
  26.247                syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
  26.248                phase = Session.Ready
  26.249 @@ -262,53 +291,16 @@
  26.250            }
  26.251            else bad_result(result)
  26.252          }
  26.253 -
  26.254 -      raw_messages.event(result)
  26.255 -    }
  26.256 -    //}}}
  26.257 -
  26.258 -
  26.259 -    def edit_version(edits: List[Document.Edit_Text])
  26.260 -    //{{{
  26.261 -    {
  26.262 -      val previous = global_state.peek().history.tip.version
  26.263 -      val syntax = current_syntax()
  26.264 -      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, edits) }
  26.265 -      val change = global_state.change_yield(_.extend_history(previous, edits, result))
  26.266 -
  26.267 -      change.version.map(_ => {
  26.268 -        assignments.await { global_state.peek().is_assigned(previous.get_finished) }
  26.269 -        this_actor ! change })
  26.270      }
  26.271      //}}}
  26.272  
  26.273  
  26.274      /* main loop */
  26.275  
  26.276 +    //{{{
  26.277      var finished = false
  26.278      while (!finished) {
  26.279        receive {
  26.280 -        case Interrupt_Prover =>
  26.281 -          prover.map(_.interrupt)
  26.282 -
  26.283 -        case Edit_Node(name, header, text_edits) if prover.isDefined =>
  26.284 -          val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
  26.285 -          edit_version(List((node_name, Some(text_edits))))
  26.286 -          reply(())
  26.287 -
  26.288 -        case Init_Node(name, header, text) if prover.isDefined =>
  26.289 -          // FIXME compare with existing node
  26.290 -          val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
  26.291 -          edit_version(List(
  26.292 -            (node_name, None),
  26.293 -            (node_name, Some(List(Text.Edit.insert(0, text))))))
  26.294 -          reply(())
  26.295 -
  26.296 -        case change: Document.Change if prover.isDefined =>
  26.297 -          handle_change(change)
  26.298 -
  26.299 -        case result: Isabelle_Process.Result => handle_result(result)
  26.300 -
  26.301          case Start(timeout, args) if prover.isEmpty =>
  26.302            if (phase == Session.Inactive || phase == Session.Failed) {
  26.303              phase = Session.Startup
  26.304 @@ -320,37 +312,52 @@
  26.305              global_state.change(_ => Document.State.init)  // FIXME event bus!?
  26.306              phase = Session.Shutdown
  26.307              prover.get.terminate
  26.308 +            prover = None
  26.309              phase = Session.Inactive
  26.310            }
  26.311            finished = true
  26.312            reply(())
  26.313  
  26.314 -        case bad if prover.isDefined =>
  26.315 -          System.err.println("session_actor: ignoring bad message " + bad)
  26.316 +        case Interrupt if prover.isDefined =>
  26.317 +          prover.get.interrupt
  26.318 +
  26.319 +        case Init_Node(name, header, text) if prover.isDefined =>
  26.320 +          // FIXME compare with existing node
  26.321 +          handle_edits(name, header, List(None, Some(List(Text.Edit.insert(0, text)))))
  26.322 +          reply(())
  26.323 +
  26.324 +        case Edit_Node(name, header, text_edits) if prover.isDefined =>
  26.325 +          handle_edits(name, header, List(Some(text_edits)))
  26.326 +          reply(())
  26.327 +
  26.328 +        case change: Change_Node if prover.isDefined =>
  26.329 +          handle_change(change)
  26.330 +
  26.331 +        case input: Isabelle_Process.Input =>
  26.332 +          raw_messages.event(input)
  26.333 +
  26.334 +        case result: Isabelle_Process.Result =>
  26.335 +          handle_result(result)
  26.336 +          raw_messages.event(result)
  26.337 +
  26.338 +        case bad => System.err.println("session_actor: ignoring bad message " + bad)
  26.339        }
  26.340      }
  26.341 +    //}}}
  26.342    }
  26.343  
  26.344  
  26.345 -
  26.346 -  /** main methods **/
  26.347 +  /* actions */
  26.348  
  26.349    def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
  26.350  
  26.351    def stop() { command_change_buffer !? Stop; session_actor !? Stop }
  26.352  
  26.353 -  def interrupt() { session_actor ! Interrupt_Prover }
  26.354 -
  26.355 -  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
  26.356 -  {
  26.357 -    session_actor !? Edit_Node(name, header, edits)
  26.358 -  }
  26.359 +  def interrupt() { session_actor ! Interrupt }
  26.360  
  26.361    def init_node(name: String, header: Document.Node.Header, text: String)
  26.362 -  {
  26.363 -    session_actor !? Init_Node(name, header, text)
  26.364 -  }
  26.365 +  { session_actor !? Init_Node(name, header, text) }
  26.366  
  26.367 -  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
  26.368 -    global_state.peek().snapshot(name, pending_edits)
  26.369 +  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
  26.370 +  { session_actor !? Edit_Node(name, header, edits) }
  26.371  }
    27.1 --- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 21:39:03 2011 +0200
    27.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 21:46:41 2011 +0200
    27.3 @@ -31,6 +31,13 @@
    27.4        Header(f(name), imports.map(f), uses.map(f))
    27.5    }
    27.6  
    27.7 +  val encode_xml_data: XML_Data.Encode.T[Header] =
    27.8 +  {
    27.9 +    case Header(name, imports, uses) =>
   27.10 +      import XML_Data.Encode._
   27.11 +      triple(string, list(string), list(string))(name, imports, uses)
   27.12 +  }
   27.13 +
   27.14  
   27.15    /* file name */
   27.16  
    28.1 --- a/src/Pure/Thy/thy_syntax.scala	Sun Jul 10 21:39:03 2011 +0200
    28.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Jul 10 21:46:41 2011 +0200
    28.3 @@ -99,8 +99,12 @@
    28.4  
    28.5    /** text edits **/
    28.6  
    28.7 -  def text_edits(syntax: Outer_Syntax, previous: Document.Version,
    28.8 -      edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
    28.9 +  def text_edits(
   28.10 +      syntax: Outer_Syntax,
   28.11 +      previous: Document.Version,
   28.12 +      edits: List[Document.Edit_Text],
   28.13 +      headers: List[(String, Document.Node.Header)])
   28.14 +    : (List[Document.Edit_Command], List[(String, Thy_Header.Header)], Document.Version) =
   28.15    {
   28.16      /* phase 1: edit individual command source */
   28.17  
   28.18 @@ -169,10 +173,25 @@
   28.19      }
   28.20  
   28.21  
   28.22 +    /* node header */
   28.23 +
   28.24 +    def node_header(name: String, node: Document.Node)
   28.25 +        : (List[(String, Thy_Header.Header)], Document.Node.Header) =
   28.26 +      (node.header.thy_header, headers.find(p => p._1 == name).map(_._2)) match {
   28.27 +        case (Exn.Res(thy_header0), Some(header @ Document.Node.Header(_, Exn.Res(thy_header))))
   28.28 +        if thy_header0 != thy_header =>
   28.29 +          (List((name, thy_header)), header)
   28.30 +        case (Exn.Exn(_), Some(header @ Document.Node.Header(_, Exn.Res(thy_header)))) =>
   28.31 +          (List((name, thy_header)), header)
   28.32 +        case _ => (Nil, node.header)
   28.33 +      }
   28.34 +
   28.35 +
   28.36      /* resulting document edits */
   28.37  
   28.38      {
   28.39        val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
   28.40 +      val header_edits = new mutable.ListBuffer[(String, Thy_Header.Header)]
   28.41        var nodes = previous.nodes
   28.42  
   28.43        edits foreach {
   28.44 @@ -194,9 +213,13 @@
   28.45              inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
   28.46  
   28.47            doc_edits += (name -> Some(cmd_edits))
   28.48 -          nodes += (name -> new Document.Node(node.header, commands2))
   28.49 +
   28.50 +          val (new_headers, new_header) = node_header(name, node)
   28.51 +          header_edits ++= new_headers
   28.52 +
   28.53 +          nodes += (name -> Document.Node(new_header, node.blobs, commands2))
   28.54        }
   28.55 -      (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
   28.56 +      (doc_edits.toList, header_edits.toList, Document.Version(Document.new_id(), nodes))
   28.57      }
   28.58    }
   28.59  }
    29.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Jul 10 21:39:03 2011 +0200
    29.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Jul 10 21:46:41 2011 +0200
    29.3 @@ -139,8 +139,8 @@
    29.4            |> (if rem_dups then cons ("rem_dups", "") else I)
    29.5            |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
    29.6        in
    29.7 -        XML.Elem (("Query", properties), XML_Data.make_list 
    29.8 -          (XML_Data.make_pair XML_Data.make_bool (single o xml_of_criterion)) criteria)
    29.9 +        XML.Elem (("Query", properties), XML_Data.Encode.list
   29.10 +          (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
   29.11        end
   29.12    | xml_of_query _ = raise Fail "cannot serialize goal";
   29.13  
   29.14 @@ -148,8 +148,9 @@
   29.15        let
   29.16          val rem_dups = Properties.defined properties "rem_dups";
   29.17          val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
   29.18 -        val criteria = XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_bool 
   29.19 -          (criterion_of_xml o the_single)) body;
   29.20 +        val criteria =
   29.21 +          XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
   29.22 +            (criterion_of_xml o the_single)) body;
   29.23        in
   29.24          {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
   29.25        end
   29.26 @@ -189,12 +190,12 @@
   29.27      val properties =
   29.28        if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
   29.29    in
   29.30 -    XML.Elem (("Result", properties), XML_Data.make_list (single o xml_of_theorem) theorems)
   29.31 +    XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
   29.32    end;
   29.33  
   29.34  fun result_of_xml (XML.Elem (("Result", properties), body)) =
   29.35        (Properties.get properties "found" |> Option.map Markup.parse_int,
   29.36 -       XML_Data.dest_list (theorem_of_xml o the_single) body)
   29.37 +       XML_Data.Decode.list (theorem_of_xml o the_single) body)
   29.38    | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
   29.39  
   29.40  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
    30.1 --- a/src/Pure/build-jars	Sun Jul 10 21:39:03 2011 +0200
    30.2 +++ b/src/Pure/build-jars	Sun Jul 10 21:46:41 2011 +0200
    30.3 @@ -30,6 +30,7 @@
    30.4    Isar/outer_syntax.scala
    30.5    Isar/parse.scala
    30.6    Isar/token.scala
    30.7 +  PIDE/blob.scala
    30.8    PIDE/command.scala
    30.9    PIDE/document.scala
   30.10    PIDE/isar_document.scala
   30.11 @@ -56,6 +57,7 @@
   30.12    Thy/thy_syntax.scala
   30.13    library.scala
   30.14    package.scala
   30.15 +  term.scala
   30.16  )
   30.17  
   30.18  
    31.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.2 +++ b/src/Pure/term.scala	Sun Jul 10 21:46:41 2011 +0200
    31.3 @@ -0,0 +1,91 @@
    31.4 +/*  Title:      Pure/term.scala
    31.5 +    Author:     Makarius
    31.6 +
    31.7 +Lambda terms with XML data representation.
    31.8 +
    31.9 +Note: Isabelle/ML is the primary environment for logical operations.
   31.10 +*/
   31.11 +
   31.12 +package isabelle
   31.13 +
   31.14 +
   31.15 +object Term
   31.16 +{
   31.17 +  /* basic type definitions */
   31.18 +
   31.19 +  type Indexname = (String, Int)
   31.20 +
   31.21 +  type Sort = List[String]
   31.22 +  val dummyS: Sort = List("")
   31.23 +
   31.24 +  sealed abstract class Typ
   31.25 +  case class Type(name: String, args: List[Typ] = Nil) extends Typ
   31.26 +  case class TFree(name: String, sort: Sort = dummyS) extends Typ
   31.27 +  case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ
   31.28 +  val dummyT = Type("dummy")
   31.29 +
   31.30 +  sealed abstract class Term
   31.31 +  case class Const(name: String, typ: Typ = dummyT) extends Term
   31.32 +  case class Free(name: String, typ: Typ = dummyT) extends Term
   31.33 +  case class Var(name: Indexname, typ: Typ = dummyT) extends Term
   31.34 +  case class Bound(index: Int) extends Term
   31.35 +  case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
   31.36 +  case class App(fun: Term, arg: Term) extends Term
   31.37 +}
   31.38 +
   31.39 +
   31.40 +object Term_XML
   31.41 +{
   31.42 +  import Term._
   31.43 +
   31.44 +
   31.45 +  /* XML data representation */
   31.46 +
   31.47 +  object Encode
   31.48 +  {
   31.49 +    import XML_Data.Encode._
   31.50 +
   31.51 +    val indexname: T[Indexname] = pair(string, int)
   31.52 +
   31.53 +    val sort: T[Sort] = list(string)
   31.54 +
   31.55 +    def typ: T[Typ] =
   31.56 +      variant[Typ](List(
   31.57 +        { case Type(a, b) => pair(string, list(typ))((a, b)) },
   31.58 +        { case TFree(a, b) => pair(string, sort)((a, b)) },
   31.59 +        { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
   31.60 +
   31.61 +    def term: T[Term] =
   31.62 +      variant[Term](List(
   31.63 +        { case Const(a, b) => pair(string, typ)((a, b)) },
   31.64 +        { case Free(a, b) => pair(string, typ)((a, b)) },
   31.65 +        { case Var(a, b) => pair(indexname, typ)((a, b)) },
   31.66 +        { case Bound(a) => int(a) },
   31.67 +        { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
   31.68 +        { case App(a, b) => pair(term, term)((a, b)) }))
   31.69 +  }
   31.70 +
   31.71 +  object Decode
   31.72 +  {
   31.73 +    import XML_Data.Decode._
   31.74 +
   31.75 +    val indexname: T[Indexname] = pair(string, int)
   31.76 +
   31.77 +    val sort: T[Sort] = list(string)
   31.78 +
   31.79 +    def typ: T[Typ] =
   31.80 +      variant[Typ](List(
   31.81 +        (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
   31.82 +        (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
   31.83 +        (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
   31.84 +
   31.85 +    def term: T[Term] =
   31.86 +      variant[Term](List(
   31.87 +        (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
   31.88 +        (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
   31.89 +        (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
   31.90 +        (x => Bound(int(x))),
   31.91 +        (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
   31.92 +        (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
   31.93 +  }
   31.94 +}
    32.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.2 +++ b/src/Pure/term_xml.ML	Sun Jul 10 21:46:41 2011 +0200
    32.3 @@ -0,0 +1,78 @@
    32.4 +(*  Title:      Pure/term_xml.ML
    32.5 +    Author:     Makarius
    32.6 +
    32.7 +XML data representation of lambda terms.
    32.8 +*)
    32.9 +
   32.10 +signature TERM_XML_OPS =
   32.11 +sig
   32.12 +  type 'a T
   32.13 +  val indexname: indexname T
   32.14 +  val sort: sort T
   32.15 +  val typ: typ T
   32.16 +  val term: term T
   32.17 +end
   32.18 +
   32.19 +signature TERM_XML =
   32.20 +sig
   32.21 +  structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
   32.22 +  structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
   32.23 +end;
   32.24 +
   32.25 +structure Term_XML: TERM_XML =
   32.26 +struct
   32.27 +
   32.28 +(* encode *)
   32.29 +
   32.30 +structure Encode =
   32.31 +struct
   32.32 +
   32.33 +open XML_Data.Encode;
   32.34 +
   32.35 +val indexname = pair string int;
   32.36 +
   32.37 +val sort = list string;
   32.38 +
   32.39 +fun typ T = T |> variant
   32.40 + [fn Type x => pair string (list typ) x,
   32.41 +  fn TFree x => pair string sort x,
   32.42 +  fn TVar x => pair indexname sort x];
   32.43 +
   32.44 +fun term t = t |> variant
   32.45 + [fn Const x => pair string typ x,
   32.46 +  fn Free x => pair string typ x,
   32.47 +  fn Var x => pair indexname typ x,
   32.48 +  fn Bound x => int x,
   32.49 +  fn Abs x => triple string typ term x,
   32.50 +  fn op $ x => pair term term x];
   32.51 +
   32.52 +end;
   32.53 +
   32.54 +
   32.55 +(* decode *)
   32.56 +
   32.57 +structure Decode =
   32.58 +struct
   32.59 +
   32.60 +open XML_Data.Decode;
   32.61 +
   32.62 +val indexname = pair string int;
   32.63 +
   32.64 +val sort = list string;
   32.65 +
   32.66 +fun typ T = T |> variant
   32.67 + [Type o pair string (list typ),
   32.68 +  TFree o pair string sort,
   32.69 +  TVar o pair indexname sort];
   32.70 +
   32.71 +fun term t = t |> variant
   32.72 + [Const o pair string typ,
   32.73 +  Free o pair string typ,
   32.74 +  Var o pair indexname typ,
   32.75 +  Bound o int,
   32.76 +  Abs o triple string typ term,
   32.77 +  op $ o pair term term];
   32.78 +
   32.79 +end;
   32.80 +
   32.81 +end;
    33.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Jul 10 21:39:03 2011 +0200
    33.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Jul 10 21:46:41 2011 +0200
    33.3 @@ -61,8 +61,10 @@
    33.4  {
    33.5    /* pending text edits */
    33.6  
    33.7 +  private val node_name = (master_dir + Path.basic(thy_name)).implode
    33.8 +
    33.9    private def node_header(): Document.Node.Header =
   33.10 -    new Document.Node.Header(master_dir,
   33.11 +    Document.Node.Header(Path.current,  // FIXME master_dir (!?)
   33.12        Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
   33.13  
   33.14    private object pending_edits  // owned by Swing thread
   33.15 @@ -77,14 +79,14 @@
   33.16          case Nil =>
   33.17          case edits =>
   33.18            pending.clear
   33.19 -          session.edit_node(thy_name, node_header(), edits)
   33.20 +          session.edit_node(node_name, node_header(), edits)
   33.21        }
   33.22      }
   33.23  
   33.24      def init()
   33.25      {
   33.26        flush()
   33.27 -      session.init_node(thy_name, node_header(), Isabelle.buffer_text(buffer))
   33.28 +      session.init_node(node_name, node_header(), Isabelle.buffer_text(buffer))
   33.29      }
   33.30  
   33.31      private val delay_flush =
   33.32 @@ -104,7 +106,6 @@
   33.33    def snapshot(): Document.Snapshot =
   33.34    {
   33.35      Swing_Thread.require()
   33.36 -    val node_name = (master_dir + Path.basic(thy_name)).implode  // FIXME
   33.37      session.snapshot(node_name, pending_edits.snapshot())
   33.38    }
   33.39  
    34.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Jul 10 21:39:03 2011 +0200
    34.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Jul 10 21:46:41 2011 +0200
    34.3 @@ -105,7 +105,7 @@
    34.4  
    34.5    /* text area ranges */
    34.6  
    34.7 -  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
    34.8 +  sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int)
    34.9  
   34.10    def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   34.11    {
    35.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Sun Jul 10 21:39:03 2011 +0200
    35.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Sun Jul 10 21:46:41 2011 +0200
    35.3 @@ -28,6 +28,9 @@
    35.4    private val main_actor = actor {
    35.5      loop {
    35.6        react {
    35.7 +        case input: Isabelle_Process.Input =>
    35.8 +          Swing_Thread.now { text_area.append(input.toString + "\n") }
    35.9 +
   35.10          case result: Isabelle_Process.Result =>
   35.11            Swing_Thread.now { text_area.append(result.message.toString + "\n") }
   35.12  
    36.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Sun Jul 10 21:39:03 2011 +0200
    36.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Sun Jul 10 21:46:41 2011 +0200
    36.3 @@ -30,6 +30,8 @@
    36.4    private val main_actor = actor {
    36.5      loop {
    36.6        react {
    36.7 +        case input: Isabelle_Process.Input =>
    36.8 +
    36.9          case result: Isabelle_Process.Result =>
   36.10            if (result.is_stdout)
   36.11              Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
    37.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sun Jul 10 21:39:03 2011 +0200
    37.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Jul 10 21:46:41 2011 +0200
    37.3 @@ -76,6 +76,8 @@
    37.4    private val main_actor = actor {
    37.5      loop {
    37.6        react {
    37.7 +        case input: Isabelle_Process.Input =>
    37.8 +
    37.9          case result: Isabelle_Process.Result =>
   37.10            if (result.is_syslog)
   37.11              Swing_Thread.now {