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