--- 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.
--- 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;
--- 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;
--- 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 =
{
--- 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")
--- 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)
--- 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
}
--- 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)
--- 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;
+
--- 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)
- }
}
--- 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;
--- 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 \
--- 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);
--- /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)
+}
--- 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,
--- 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;
--- 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))
}
--- 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)
--- 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))
}
}
--- 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._
--- 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]] =
--- 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";
--- 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;
--- 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;
--- 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) }
}
--- 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) }
}
--- 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 */
--- 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))
}
}
}
--- 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
--- 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
)
--- /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) })))
+ }
+}
--- /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;
--- 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())
}
--- 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] =
{
--- 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") }
--- 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) }
--- 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 {