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 +(** encode **)
9.56 +
9.57 +structure Encode =
9.58 +struct
9.59 +
9.60 +type 'a T = 'a -> XML.body;
9.61 +
9.62 +
9.63 (* basic values *)
9.64
9.65 +fun int_atom i = signed_string_of_int i;
9.66 +
9.67 +fun bool_atom false = "0"
9.68 + | bool_atom true = "1";
9.69 +
9.70 +fun unit_atom () = "";
9.71 +
9.72 +
9.73 +(* structural nodes *)
9.74 +
9.75 +fun node ts = XML.Elem ((":", []), ts);
9.76 +
9.77 +fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
9.78 +
9.79 +
9.80 +(* representation of standard types *)
9.81 +
9.82 +fun properties props = [XML.Elem ((":", props), [])];
9.83 +
9.84 +fun string "" = []
9.85 + | string s = [XML.Text s];
9.86 +
9.87 +val int = string o int_atom;
9.88 +
9.89 +val bool = string o bool_atom;
9.90 +
9.91 +val unit = string o unit_atom;
9.92 +
9.93 +fun pair f g (x, y) = [node (f x), node (g y)];
9.94 +
9.95 +fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
9.96 +
9.97 +fun list f xs = map (node o f) xs;
9.98 +
9.99 +fun option _ NONE = []
9.100 + | option f (SOME x) = [node (f x)];
9.101 +
9.102 +fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
9.103 +
9.104 +end;
9.105 +
9.106 +
9.107 +
9.108 +(** decode **)
9.109 +
9.110 exception XML_ATOM of string;
9.111 +exception XML_BODY of XML.tree list;
9.112
9.113 +structure Decode =
9.114 +struct
9.115
9.116 -fun make_int_atom i = signed_string_of_int i;
9.117 +type 'a T = XML.body -> 'a;
9.118
9.119 -fun dest_int_atom s =
9.120 +
9.121 +(* basic values *)
9.122 +
9.123 +fun int_atom s =
9.124 (case Int.fromString s of
9.125 SOME i => i
9.126 | NONE => raise XML_ATOM s);
9.127
9.128 +fun bool_atom "0" = false
9.129 + | bool_atom "1" = true
9.130 + | bool_atom s = raise XML_ATOM s;
9.131
9.132 -fun make_bool_atom false = "0"
9.133 - | make_bool_atom true = "1";
9.134 -
9.135 -fun dest_bool_atom "0" = false
9.136 - | dest_bool_atom "1" = true
9.137 - | dest_bool_atom s = raise XML_ATOM s;
9.138 -
9.139 -
9.140 -fun make_unit_atom () = "";
9.141 -
9.142 -fun dest_unit_atom "" = ()
9.143 - | dest_unit_atom s = raise XML_ATOM s;
9.144 +fun unit_atom "" = ()
9.145 + | unit_atom s = raise XML_ATOM s;
9.146
9.147
9.148 (* structural nodes *)
9.149
9.150 -exception XML_BODY of XML.tree list;
9.151 +fun node (XML.Elem ((":", []), ts)) = ts
9.152 + | node t = raise XML_BODY [t];
9.153
9.154 -fun make_node ts = XML.Elem ((":", []), ts);
9.155 -
9.156 -fun dest_node (XML.Elem ((":", []), ts)) = ts
9.157 - | dest_node t = raise XML_BODY [t];
9.158 -
9.159 -fun make_tagged (tag, ts) = XML.Elem ((make_int_atom tag, []), ts);
9.160 -
9.161 -fun dest_tagged (XML.Elem ((s, []), ts)) = (dest_int_atom s, ts)
9.162 - | dest_tagged t = raise XML_BODY [t];
9.163 +fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts)
9.164 + | tagged t = raise XML_BODY [t];
9.165
9.166
9.167 (* representation of standard types *)
9.168
9.169 -fun make_properties props = [XML.Elem ((":", props), [])];
9.170 +fun properties [XML.Elem ((":", props), [])] = props
9.171 + | properties ts = raise XML_BODY ts;
9.172
9.173 -fun dest_properties [XML.Elem ((":", props), [])] = props
9.174 - | dest_properties ts = raise XML_BODY ts;
9.175 +fun string [] = ""
9.176 + | string [XML.Text s] = s
9.177 + | string ts = raise XML_BODY ts;
9.178
9.179 +val int = int_atom o string;
9.180
9.181 -fun make_string "" = []
9.182 - | make_string s = [XML.Text s];
9.183 +val bool = bool_atom o string;
9.184
9.185 -fun dest_string [] = ""
9.186 - | dest_string [XML.Text s] = s
9.187 - | dest_string ts = raise XML_BODY ts;
9.188 +val unit = unit_atom o string;
9.189
9.190 +fun pair f g [t1, t2] = (f (node t1), g (node t2))
9.191 + | pair _ _ ts = raise XML_BODY ts;
9.192
9.193 -val make_int = make_string o make_int_atom;
9.194 -val dest_int = dest_int_atom o dest_string;
9.195 +fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
9.196 + | triple _ _ _ ts = raise XML_BODY ts;
9.197
9.198 -val make_bool = make_string o make_bool_atom;
9.199 -val dest_bool = dest_bool_atom o dest_string;
9.200 +fun list f ts = map (f o node) ts;
9.201
9.202 -val make_unit = make_string o make_unit_atom;
9.203 -val dest_unit = dest_unit_atom o dest_string;
9.204 +fun option _ [] = NONE
9.205 + | option f [t] = SOME (f (node t))
9.206 + | option _ ts = raise XML_BODY ts;
9.207
9.208 -
9.209 -fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
9.210 -
9.211 -fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
9.212 - | dest_pair _ _ ts = raise XML_BODY ts;
9.213 -
9.214 -
9.215 -fun make_triple make1 make2 make3 (x, y, z) =
9.216 - [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
9.217 -
9.218 -fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
9.219 - (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
9.220 - | dest_triple _ _ _ ts = raise XML_BODY ts;
9.221 -
9.222 -
9.223 -fun make_list make xs = map (make_node o make) xs;
9.224 -
9.225 -fun dest_list dest ts = map (dest o dest_node) ts;
9.226 -
9.227 -
9.228 -fun make_option _ NONE = []
9.229 - | make_option make (SOME x) = [make_node (make x)];
9.230 -
9.231 -fun dest_option _ [] = NONE
9.232 - | dest_option dest [t] = SOME (dest (dest_node t))
9.233 - | dest_option _ ts = raise XML_BODY ts;
9.234 -
9.235 -
9.236 -fun make_variant makes x =
9.237 - [make_tagged (the (get_index (fn make => try make x) makes))];
9.238 -
9.239 -fun dest_variant dests [t] =
9.240 - let val (tag, ts) = dest_tagged t
9.241 - in nth dests tag ts end
9.242 - | dest_variant _ ts = raise XML_BODY ts;
9.243 +fun variant fs [t] = uncurry (nth fs) (tagged t)
9.244 + | variant _ ts = raise XML_BODY ts;
9.245
9.246 end;
9.247
9.248 +end;
9.249 +
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 + /** encode **/
10.9 +
10.10 + object Encode
10.11 + {
10.12 + type T[A] = A => XML.Body
10.13 +
10.14 +
10.15 + /* basic values */
10.16 +
10.17 + private def long_atom(i: Long): String = i.toString
10.18 +
10.19 + private def int_atom(i: Int): String = i.toString
10.20 +
10.21 + private def bool_atom(b: Boolean): String = if (b) "1" else "0"
10.22 +
10.23 + private def unit_atom(u: Unit) = ""
10.24 +
10.25 +
10.26 + /* structural nodes */
10.27 +
10.28 + private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
10.29 +
10.30 + private def tagged(tag: Int, ts: XML.Body): XML.Tree =
10.31 + XML.Elem(Markup(int_atom(tag), Nil), ts)
10.32 +
10.33 +
10.34 + /* representation of standard types */
10.35 +
10.36 + val properties: T[List[(String, String)]] =
10.37 + (props => List(XML.Elem(Markup(":", props), Nil)))
10.38 +
10.39 + val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
10.40 +
10.41 + val long: T[Long] = (x => string(long_atom(x)))
10.42 +
10.43 + val int: T[Int] = (x => string(int_atom(x)))
10.44 +
10.45 + val bool: T[Boolean] = (x => string(bool_atom(x)))
10.46 +
10.47 + val unit: T[Unit] = (x => string(unit_atom(x)))
10.48 +
10.49 + def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
10.50 + (x => List(node(f(x._1)), node(g(x._2))))
10.51 +
10.52 + def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
10.53 + (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
10.54 +
10.55 + def list[A](f: T[A]): T[List[A]] =
10.56 + (xs => xs.map((x: A) => node(f(x))))
10.57 +
10.58 + def option[A](f: T[A]): T[Option[A]] =
10.59 + {
10.60 + case None => Nil
10.61 + case Some(x) => List(node(f(x)))
10.62 + }
10.63 +
10.64 + def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
10.65 + {
10.66 + case x =>
10.67 + val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
10.68 + List(tagged(tag, f(x)))
10.69 + }
10.70 + }
10.71 +
10.72 +
10.73 +
10.74 + /** decode **/
10.75
10.76 class XML_Atom(s: String) extends Exception(s)
10.77 -
10.78 -
10.79 - private def make_long_atom(i: Long): String = i.toString
10.80 -
10.81 - private def dest_long_atom(s: String): Long =
10.82 - try { java.lang.Long.parseLong(s) }
10.83 - catch { case e: NumberFormatException => throw new XML_Atom(s) }
10.84 -
10.85 -
10.86 - private def make_int_atom(i: Int): String = i.toString
10.87 -
10.88 - private def dest_int_atom(s: String): Int =
10.89 - try { Integer.parseInt(s) }
10.90 - catch { case e: NumberFormatException => throw new XML_Atom(s) }
10.91 -
10.92 -
10.93 - private def make_bool_atom(b: Boolean): String = if (b) "1" else "0"
10.94 -
10.95 - private def dest_bool_atom(s: String): Boolean =
10.96 - if (s == "1") true
10.97 - else if (s == "0") false
10.98 - else throw new XML_Atom(s)
10.99 -
10.100 -
10.101 - private def make_unit_atom(u: Unit) = ""
10.102 -
10.103 - private def dest_unit_atom(s: String): Unit =
10.104 - if (s == "") () else throw new XML_Atom(s)
10.105 -
10.106 -
10.107 - /* structural nodes */
10.108 -
10.109 class XML_Body(body: XML.Body) extends Exception
10.110
10.111 - private def make_node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
10.112 + object Decode
10.113 + {
10.114 + type T[A] = XML.Body => A
10.115
10.116 - private def dest_node(t: XML.Tree): XML.Body =
10.117 - t match {
10.118 - case XML.Elem(Markup(":", Nil), ts) => ts
10.119 - case _ => throw new XML_Body(List(t))
10.120 +
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 + private def int_atom(s: String): Int =
10.128 + try { Integer.parseInt(s) }
10.129 + catch { case e: NumberFormatException => throw new XML_Atom(s) }
10.130 +
10.131 + private def bool_atom(s: String): Boolean =
10.132 + if (s == "1") true
10.133 + else if (s == "0") false
10.134 + else throw new XML_Atom(s)
10.135 +
10.136 + private def unit_atom(s: String): Unit =
10.137 + if (s == "") () else throw new XML_Atom(s)
10.138 +
10.139 +
10.140 + /* structural nodes */
10.141 +
10.142 + private def node(t: XML.Tree): XML.Body =
10.143 + t match {
10.144 + case XML.Elem(Markup(":", Nil), ts) => ts
10.145 + case _ => throw new XML_Body(List(t))
10.146 + }
10.147 +
10.148 + private def tagged(t: XML.Tree): (Int, XML.Body) =
10.149 + t match {
10.150 + case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
10.151 + case _ => throw new XML_Body(List(t))
10.152 + }
10.153 +
10.154 +
10.155 + /* representation of standard types */
10.156 +
10.157 + val properties: T[List[(String, String)]] =
10.158 + {
10.159 + case List(XML.Elem(Markup(":", props), Nil)) => props
10.160 + case ts => throw new XML_Body(ts)
10.161 }
10.162
10.163 - private def make_tagged(tag: Int, ts: XML.Body): XML.Tree =
10.164 - XML.Elem(Markup(make_int_atom(tag), Nil), ts)
10.165 -
10.166 - private def dest_tagged(t: XML.Tree): (Int, XML.Body) =
10.167 - t match {
10.168 - case XML.Elem(Markup(s, Nil), ts) => (dest_int_atom(s), ts)
10.169 - case _ => throw new XML_Body(List(t))
10.170 + val string: T[String] =
10.171 + {
10.172 + case Nil => ""
10.173 + case List(XML.Text(s)) => s
10.174 + case ts => throw new XML_Body(ts)
10.175 }
10.176
10.177 + val long: T[Long] = (x => long_atom(string(x)))
10.178
10.179 - /* representation of standard types */
10.180 + val int: T[Int] = (x => int_atom(string(x)))
10.181
10.182 - def make_properties(props: List[(String, String)]): XML.Body =
10.183 - List(XML.Elem(Markup(":", props), Nil))
10.184 + val bool: T[Boolean] = (x => bool_atom(string(x)))
10.185
10.186 - def dest_properties(ts: XML.Body): List[(String, String)] =
10.187 - ts match {
10.188 - case List(XML.Elem(Markup(":", props), Nil)) => props
10.189 - case _ => throw new XML_Body(ts)
10.190 + val unit: T[Unit] = (x => unit_atom(string(x)))
10.191 +
10.192 + def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
10.193 + {
10.194 + case List(t1, t2) => (f(node(t1)), g(node(t2)))
10.195 + case ts => throw new XML_Body(ts)
10.196 }
10.197
10.198 -
10.199 - def make_string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
10.200 -
10.201 - def dest_string(ts: XML.Body): String =
10.202 - ts match {
10.203 - case Nil => ""
10.204 - case List(XML.Text(s)) => s
10.205 - case _ => throw new XML_Body(ts)
10.206 + def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
10.207 + {
10.208 + case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
10.209 + case ts => throw new XML_Body(ts)
10.210 }
10.211
10.212 + def list[A](f: T[A]): T[List[A]] =
10.213 + (ts => ts.map(t => f(node(t))))
10.214
10.215 - def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
10.216 - def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
10.217 -
10.218 - def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
10.219 - def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
10.220 -
10.221 - def make_bool(b: Boolean): XML.Body = make_string(make_bool_atom(b))
10.222 - def dest_bool(ts: XML.Body) = dest_bool_atom(dest_string(ts))
10.223 -
10.224 - def make_unit(u: Unit): XML.Body = make_string(make_unit_atom(u))
10.225 - def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
10.226 -
10.227 -
10.228 - def make_pair[A, B](make1: A => XML.Body)(make2: B => XML.Body)(p: (A, B)): XML.Body =
10.229 - List(make_node(make1(p._1)), make_node(make2(p._2)))
10.230 -
10.231 - def dest_pair[A, B](dest1: XML.Body => A)(dest2: XML.Body => B)(ts: XML.Body): (A, B) =
10.232 - ts match {
10.233 - case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
10.234 - case _ => throw new XML_Body(ts)
10.235 + def option[A](f: T[A]): T[Option[A]] =
10.236 + {
10.237 + case Nil => None
10.238 + case List(t) => Some(f(node(t)))
10.239 + case ts => throw new XML_Body(ts)
10.240 }
10.241
10.242 -
10.243 - def make_triple[A, B, C](make1: A => XML.Body)(make2: B => XML.Body)(make3: C => XML.Body)
10.244 - (p: (A, B, C)): XML.Body =
10.245 - List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
10.246 -
10.247 - def dest_triple[A, B, C](dest1: XML.Body => A)(dest2: XML.Body => B)(dest3: XML.Body => C)
10.248 - (ts: XML.Body): (A, B, C) =
10.249 - ts match {
10.250 - case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
10.251 - case _ => throw new XML_Body(ts)
10.252 + def variant[A](fs: List[T[A]]): T[A] =
10.253 + {
10.254 + case List(t) =>
10.255 + val (tag, ts) = tagged(t)
10.256 + fs(tag)(ts)
10.257 + case ts => throw new XML_Body(ts)
10.258 }
10.259 -
10.260 -
10.261 - def make_list[A](make: A => XML.Body)(xs: List[A]): XML.Body =
10.262 - xs.map((x: A) => make_node(make(x)))
10.263 -
10.264 - def dest_list[A](dest: XML.Body => A)(ts: XML.Body): List[A] =
10.265 - ts.map((t: XML.Tree) => dest(dest_node(t)))
10.266 -
10.267 -
10.268 - def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
10.269 - opt match {
10.270 - case None => Nil
10.271 - case Some(x) => List(make_node(make(x)))
10.272 - }
10.273 -
10.274 - def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
10.275 - ts match {
10.276 - case Nil => None
10.277 - case List(t) => Some(dest(dest_node(t)))
10.278 - case _ => throw new XML_Body(ts)
10.279 - }
10.280 -
10.281 -
10.282 - def make_variant[A](makes: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
10.283 - {
10.284 - val (make, tag) = makes.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
10.285 - List(make_tagged(tag, make(x)))
10.286 }
10.287 -
10.288 - def dest_variant[A](dests: List[XML.Body => A])(ts: XML.Body): A =
10.289 - ts match {
10.290 - case List(t) =>
10.291 - val (tag, ts) = dest_tagged(t)
10.292 - dests(tag)(ts)
10.293 - case _ => throw new XML_Body(ts)
10.294 - }
10.295 }
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 + Syntax.parse_token ctxt decode markup
24.50 + (fn (syms, pos) =>
24.51 + let
24.52 + val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
24.53 + val ambiguity = length (proper_results results);
24.54
24.55 - val level = Config.get ctxt Syntax.ambiguity_level;
24.56 - val limit = Config.get ctxt Syntax.ambiguity_limit;
24.57 + val level = Config.get ctxt Syntax.ambiguity_level;
24.58 + val limit = Config.get ctxt Syntax.ambiguity_limit;
24.59
24.60 - val ambig_msg =
24.61 - if ambiguity > 1 andalso ambiguity <= level then
24.62 - ["Got more than one parse tree.\n\
24.63 - \Retry with smaller syntax_ambiguity_level for more information."]
24.64 - else [];
24.65 + val ambig_msg =
24.66 + if ambiguity > 1 andalso ambiguity <= level then
24.67 + ["Got more than one parse tree.\n\
24.68 + \Retry with smaller syntax_ambiguity_level for more information."]
24.69 + else [];
24.70
24.71 - (*brute-force disambiguation via type-inference*)
24.72 - fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
24.73 - handle exn as ERROR _ => Exn.Exn exn;
24.74 + (*brute-force disambiguation via type-inference*)
24.75 + fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
24.76 + handle exn as ERROR _ => Exn.Exn exn;
24.77
24.78 - val results' =
24.79 - if ambiguity > 1 then
24.80 - (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
24.81 - check results
24.82 - else results;
24.83 - val reports' = fst (hd results');
24.84 + val results' =
24.85 + if ambiguity > 1 then
24.86 + (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
24.87 + check results
24.88 + else results;
24.89 + val reports' = fst (hd results');
24.90
24.91 - val errs = map snd (failed_results results');
24.92 - val checked = map snd (proper_results results');
24.93 - val len = length checked;
24.94 + val errs = map snd (failed_results results');
24.95 + val checked = map snd (proper_results results');
24.96 + val len = length checked;
24.97
24.98 - val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
24.99 - in
24.100 - if len = 0 then
24.101 - report_result ctxt pos
24.102 - [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
24.103 - else if len = 1 then
24.104 - (if ambiguity > level then
24.105 - Context_Position.if_visible ctxt warning
24.106 - "Fortunately, only one parse tree is type correct.\n\
24.107 - \You may still want to disambiguate your grammar or your input."
24.108 - else (); report_result ctxt pos results')
24.109 - else
24.110 - report_result ctxt pos
24.111 - [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
24.112 - (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
24.113 - (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
24.114 - map show_term (take limit checked))))))]
24.115 - end handle ERROR msg => parse_failed ctxt pos msg kind
24.116 + val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
24.117 + in
24.118 + if len = 0 then
24.119 + report_result ctxt pos
24.120 + [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
24.121 + else if len = 1 then
24.122 + (if ambiguity > level then
24.123 + Context_Position.if_visible ctxt warning
24.124 + "Fortunately, only one parse tree is type correct.\n\
24.125 + \You may still want to disambiguate your grammar or your input."
24.126 + else (); report_result ctxt pos results')
24.127 + else
24.128 + report_result ctxt pos
24.129 + [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
24.130 + (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
24.131 + (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
24.132 + map show_term (take limit checked))))))]
24.133 + end handle ERROR msg => parse_failed ctxt pos msg kind)
24.134 end;
24.135
24.136
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 Start(timeout: Time, args: List[String])
26.109 + private case object Interrupt
26.110 + private case class Init_Node(name: String, header: Document.Node.Header, text: String)
26.111 private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
26.112 - private case class Init_Node(name: String, header: Document.Node.Header, text: String)
26.113 - private case class Start(timeout: Time, args: List[String])
26.114 -
26.115 - var verbose: Boolean = false
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 + def interrupt() { session_actor ! Interrupt }
26.355 +
26.356 + def init_node(name: String, header: Document.Node.Header, text: String)
26.357 + { session_actor !? Init_Node(name, header, text) }
26.358
26.359 def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
26.360 - {
26.361 - session_actor !? Edit_Node(name, header, edits)
26.362 - }
26.363 -
26.364 - def init_node(name: String, header: Document.Node.Header, text: String)
26.365 - {
26.366 - session_actor !? Init_Node(name, header, text)
26.367 - }
26.368 -
26.369 - def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
26.370 - global_state.peek().snapshot(name, pending_edits)
26.371 + { session_actor !? Edit_Node(name, header, edits) }
26.372 }
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 {