--- a/etc/isabelle.css Sun Sep 04 21:03:54 2011 -0700
+++ b/etc/isabelle.css Sun Sep 04 21:04:02 2011 -0700
@@ -40,7 +40,6 @@
.keyword { font-weight: bold; }
.operator { }
.command { font-weight: bold; }
-.ident { }
.string { color: #008B00; }
.altstring { color: #8B8B00; }
.verbatim { color: #00008B; }
--- a/src/HOL/Unix/Nested_Environment.thy Sun Sep 04 21:03:54 2011 -0700
+++ b/src/HOL/Unix/Nested_Environment.thy Sun Sep 04 21:04:02 2011 -0700
@@ -9,7 +9,7 @@
begin
text {*
- Consider a partial function @{term [source] "e :: 'a => 'b option"};
+ Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"};
this may be understood as an \emph{environment} mapping indexes
@{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
@{text Map} of Isabelle/HOL). This basic idea is easily generalized
@@ -21,7 +21,7 @@
datatype ('a, 'b, 'c) env =
Val 'a
- | Env 'b "'c => ('a, 'b, 'c) env option"
+ | Env 'b "'c \<Rightarrow> ('a, 'b, 'c) env option"
text {*
\medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
@@ -43,14 +43,14 @@
@{term None}.
*}
-primrec lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
- and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
+primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
+ and lookup_option :: "('a, 'b, 'c) env option \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
where
"lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
| "lookup (Env b es) xs =
(case xs of
- [] => Some (Env b es)
- | y # ys => lookup_option (es y) ys)"
+ [] \<Rightarrow> Some (Env b es)
+ | y # ys \<Rightarrow> lookup_option (es y) ys)"
| "lookup_option None xs = None"
| "lookup_option (Some e) xs = lookup e xs"
@@ -70,8 +70,8 @@
theorem lookup_env_cons:
"lookup (Env b es) (x # xs) =
(case es x of
- None => None
- | Some e => lookup e xs)"
+ None \<Rightarrow> None
+ | Some e \<Rightarrow> lookup e xs)"
by (cases "es x") simp_all
lemmas lookup_lookup_option.simps [simp del]
@@ -80,14 +80,14 @@
theorem lookup_eq:
"lookup env xs =
(case xs of
- [] => Some env
- | x # xs =>
+ [] \<Rightarrow> Some env
+ | x # xs \<Rightarrow>
(case env of
- Val a => None
- | Env b es =>
+ Val a \<Rightarrow> None
+ | Env b es \<Rightarrow>
(case es x of
- None => None
- | Some e => lookup e xs)))"
+ None \<Rightarrow> None
+ | Some e \<Rightarrow> lookup e xs)))"
by (simp split: list.split env.split)
text {*
@@ -245,18 +245,18 @@
environment is left unchanged.
*}
-primrec update :: "'c list => ('a, 'b, 'c) env option =>
- ('a, 'b, 'c) env => ('a, 'b, 'c) env"
- and update_option :: "'c list => ('a, 'b, 'c) env option =>
- ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
+primrec update :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
+ ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"
+ and update_option :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
+ ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env option"
where
"update xs opt (Val a) =
- (if xs = [] then (case opt of None => Val a | Some e => e)
+ (if xs = [] then (case opt of None \<Rightarrow> Val a | Some e \<Rightarrow> e)
else Val a)"
| "update xs opt (Env b es) =
(case xs of
- [] => (case opt of None => Env b es | Some e => e)
- | y # ys => Env b (es (y := update_option ys opt (es y))))"
+ [] \<Rightarrow> (case opt of None \<Rightarrow> Env b es | Some e \<Rightarrow> e)
+ | y # ys \<Rightarrow> Env b (es (y := update_option ys opt (es y))))"
| "update_option xs opt None =
(if xs = [] then opt else None)"
| "update_option xs opt (Some e) =
@@ -286,8 +286,8 @@
"update (x # y # ys) opt (Env b es) =
Env b (es (x :=
(case es x of
- None => None
- | Some e => Some (update (y # ys) opt e))))"
+ None \<Rightarrow> None
+ | Some e \<Rightarrow> Some (update (y # ys) opt e))))"
by (cases "es x") simp_all
lemmas update_update_option.simps [simp del]
@@ -297,21 +297,21 @@
lemma update_eq:
"update xs opt env =
(case xs of
- [] =>
+ [] \<Rightarrow>
(case opt of
- None => env
- | Some e => e)
- | x # xs =>
+ None \<Rightarrow> env
+ | Some e \<Rightarrow> e)
+ | x # xs \<Rightarrow>
(case env of
- Val a => Val a
- | Env b es =>
+ Val a \<Rightarrow> Val a
+ | Env b es \<Rightarrow>
(case xs of
- [] => Env b (es (x := opt))
- | y # ys =>
+ [] \<Rightarrow> Env b (es (x := opt))
+ | y # ys \<Rightarrow>
Env b (es (x :=
(case es x of
- None => None
- | Some e => Some (update (y # ys) opt e)))))))"
+ None \<Rightarrow> None
+ | Some e \<Rightarrow> Some (update (y # ys) opt e)))))))"
by (simp split: list.split env.split option.split)
text {*
--- a/src/Pure/General/markup.ML Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Pure/General/markup.ML Sun Sep 04 21:04:02 2011 -0700
@@ -58,7 +58,6 @@
val propN: string val prop: T
val ML_keywordN: string val ML_keyword: T
val ML_delimiterN: string val ML_delimiter: T
- val ML_identN: string val ML_ident: T
val ML_tvarN: string val ML_tvar: T
val ML_numeralN: string val ML_numeral: T
val ML_charN: string val ML_char: T
@@ -80,7 +79,6 @@
val keywordN: string val keyword: T
val operatorN: string val operator: T
val commandN: string val command: T
- val identN: string val ident: T
val stringN: string val string: T
val altstringN: string val altstring: T
val verbatimN: string val verbatim: T
@@ -257,7 +255,6 @@
val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
-val (ML_identN, ML_ident) = markup_elem "ML_ident";
val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
val (ML_charN, ML_char) = markup_elem "ML_char";
@@ -292,7 +289,6 @@
val (keywordN, keyword) = markup_elem "keyword";
val (operatorN, operator) = markup_elem "operator";
val (commandN, command) = markup_elem "command";
-val (identN, ident) = markup_elem "ident";
val (stringN, string) = markup_elem "string";
val (altstringN, altstring) = markup_elem "altstring";
val (verbatimN, verbatim) = markup_elem "verbatim";
--- a/src/Pure/General/markup.scala Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Pure/General/markup.scala Sun Sep 04 21:04:02 2011 -0700
@@ -142,7 +142,6 @@
val ML_KEYWORD = "ML_keyword"
val ML_DELIMITER = "ML_delimiter"
- val ML_IDENT = "ML_ident"
val ML_TVAR = "ML_tvar"
val ML_NUMERAL = "ML_numeral"
val ML_CHAR = "ML_char"
@@ -164,7 +163,6 @@
val KEYWORD = "keyword"
val OPERATOR = "operator"
val COMMAND = "command"
- val IDENT = "ident"
val STRING = "string"
val ALTSTRING = "altstring"
val VERBATIM = "verbatim"
--- a/src/Pure/General/timing.scala Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Pure/General/timing.scala Sun Sep 04 21:04:02 2011 -0700
@@ -9,6 +9,7 @@
object Time
{
def seconds(s: Double): Time = new Time((s * 1000.0) round)
+ def ms(m: Long): Time = new Time(m)
}
class Time(val ms: Long)
--- a/src/Pure/General/xml.ML Sun Sep 04 21:03:54 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,361 +0,0 @@
-(* Title: Pure/General/xml.ML
- Author: David Aspinall, Stefan Berghofer and Markus Wenzel
-
-Untyped XML trees.
-*)
-
-signature XML_DATA_OPS =
-sig
- type 'a A
- type 'a T
- type 'a V
- val int_atom: int A
- val bool_atom: bool A
- val unit_atom: unit A
- 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 V list -> 'a T
-end;
-
-signature XML =
-sig
- type attributes = Properties.T
- datatype tree =
- Elem of Markup.T * tree list
- | Text of string
- type body = tree list
- val add_content: tree -> Buffer.T -> Buffer.T
- val content_of: body -> string
- val header: string
- val text: string -> string
- val element: string -> attributes -> string list -> string
- val output_markup: Markup.T -> Output.output * Output.output
- val string_of: tree -> string
- val pretty: int -> tree -> Pretty.T
- val output: tree -> TextIO.outstream -> unit
- val parse_comments: string list -> unit * string list
- val parse_string : string -> string option
- val parse_element: string list -> tree * string list
- val parse_document: string list -> tree * string list
- val parse: string -> tree
- exception XML_ATOM of string
- exception XML_BODY of body
- structure Encode: XML_DATA_OPS
- structure Decode: XML_DATA_OPS
-end;
-
-structure XML: XML =
-struct
-
-(** XML trees **)
-
-type attributes = Properties.T;
-
-datatype tree =
- Elem of Markup.T * tree list
- | Text of string;
-
-type body = tree list;
-
-fun add_content (Elem (_, ts)) = fold add_content ts
- | add_content (Text s) = Buffer.add s;
-
-fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
-
-
-
-(** string representation **)
-
-val header = "<?xml version=\"1.0\"?>\n";
-
-
-(* escaped text *)
-
-fun decode "<" = "<"
- | decode ">" = ">"
- | decode "&" = "&"
- | decode "'" = "'"
- | decode """ = "\""
- | decode c = c;
-
-fun encode "<" = "<"
- | encode ">" = ">"
- | encode "&" = "&"
- | encode "'" = "'"
- | encode "\"" = """
- | encode c = c;
-
-val text = translate_string encode;
-
-
-(* elements *)
-
-fun elem name atts =
- space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
-
-fun element name atts body =
- let val b = implode body in
- if b = "" then enclose "<" "/>" (elem name atts)
- else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
- end;
-
-fun output_markup (markup as (name, atts)) =
- if Markup.is_empty markup then Markup.no_output
- else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
-
-
-(* output *)
-
-fun buffer_of depth tree =
- let
- fun traverse _ (Elem ((name, atts), [])) =
- Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
- | traverse d (Elem ((name, atts), ts)) =
- Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
- traverse_body d ts #>
- Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
- | traverse _ (Text s) = Buffer.add (text s)
- and traverse_body 0 _ = Buffer.add "..."
- | traverse_body d ts = fold (traverse (d - 1)) ts;
- in Buffer.empty |> traverse depth tree end;
-
-val string_of = Buffer.content o buffer_of ~1;
-val output = Buffer.output o buffer_of ~1;
-
-fun pretty depth tree =
- Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
-
-
-
-(** XML parsing (slow) **)
-
-local
-
-fun err msg (xs, _) =
- fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
-
-fun ignored _ = [];
-
-val blanks = Scan.many Symbol.is_blank;
-val special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
-val regular = Scan.one Symbol.is_regular;
-fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
-
-val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
-
-val parse_cdata =
- Scan.this_string "<![CDATA[" |--
- (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
- Scan.this_string "]]>";
-
-val parse_att =
- (Symbol.scan_id --| (blanks -- $$ "=" -- blanks)) --
- (($$ "\"" || $$ "'") :|-- (fn s =>
- (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
-
-val parse_comment =
- Scan.this_string "<!--" --
- Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
- Scan.this_string "-->" >> ignored;
-
-val parse_processing_instruction =
- Scan.this_string "<?" --
- Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
- Scan.this_string "?>" >> ignored;
-
-val parse_doctype =
- Scan.this_string "<!DOCTYPE" --
- Scan.repeat (Scan.unless ($$ ">") regular) --
- $$ ">" >> ignored;
-
-val parse_misc =
- Scan.one Symbol.is_blank >> ignored ||
- parse_processing_instruction ||
- parse_comment;
-
-val parse_optional_text =
- Scan.optional (parse_chars >> (single o Text)) [];
-
-fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
-fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
-val parse_name = Scan.one name_start_char ::: Scan.many name_char;
-
-in
-
-val parse_comments =
- blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
-
-val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
-
-fun parse_content xs =
- (parse_optional_text @@@
- (Scan.repeat
- ((parse_element >> single ||
- parse_cdata >> (single o Text) ||
- parse_processing_instruction ||
- parse_comment)
- @@@ parse_optional_text) >> flat)) xs
-
-and parse_element xs =
- ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
- (fn (name, _) =>
- !! (err (fn () => "Expected > or />"))
- ($$ "/" -- $$ ">" >> ignored ||
- $$ ">" |-- parse_content --|
- !! (err (fn () => "Expected </" ^ implode name ^ ">"))
- ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
- >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
-
-val parse_document =
- (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
- |-- parse_element;
-
-fun parse s =
- (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
- (blanks |-- parse_document --| blanks))) (raw_explode s) of
- (x, []) => x
- | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
-
-end;
-
-
-
-(** XML as data representation language **)
-
-exception XML_ATOM of string;
-exception XML_BODY of tree list;
-
-
-structure Encode =
-struct
-
-type 'a A = 'a -> string;
-type 'a T = 'a -> body;
-type 'a V = 'a -> string list * body;
-
-
-(* atomic values *)
-
-fun int_atom i = signed_string_of_int i;
-
-fun bool_atom false = "0"
- | bool_atom true = "1";
-
-fun unit_atom () = "";
-
-
-(* structural nodes *)
-
-fun node ts = Elem ((":", []), ts);
-
-fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
-
-fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
-
-
-(* representation of standard types *)
-
-fun properties props = [Elem ((":", props), [])];
-
-fun string "" = []
- | string s = [Text s];
-
-val int = string o int_atom;
-
-val bool = string o bool_atom;
-
-val unit = string o unit_atom;
-
-fun pair f g (x, y) = [node (f x), node (g y)];
-
-fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
-
-fun list f xs = map (node o f) xs;
-
-fun option _ NONE = []
- | option f (SOME x) = [node (f x)];
-
-fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
-
-end;
-
-
-structure Decode =
-struct
-
-type 'a A = string -> 'a;
-type 'a T = body -> 'a;
-type 'a V = string list * body -> 'a;
-
-
-(* atomic values *)
-
-fun int_atom s =
- Markup.parse_int s
- handle Fail _ => 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 (Elem ((":", []), ts)) = ts
- | node t = raise XML_BODY [t];
-
-fun vector atts =
- #1 (fold_map (fn (a, x) =>
- fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
-
-fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
- | tagged t = raise XML_BODY [t];
-
-
-(* representation of standard types *)
-
-fun properties [Elem ((":", props), [])] = props
- | properties ts = raise XML_BODY ts;
-
-fun string [] = ""
- | string [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] =
- let
- val (tag, (xs, ts)) = tagged t;
- val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
- in f (xs, ts) end
- | variant _ ts = raise XML_BODY ts;
-
-end;
-
-end;
--- a/src/Pure/General/xml.scala Sun Sep 04 21:03:54 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,390 +0,0 @@
-/* Title: Pure/General/xml.scala
- Author: Makarius
-
-Untyped XML trees.
-*/
-
-package isabelle
-
-import java.lang.System
-import java.util.WeakHashMap
-import java.lang.ref.WeakReference
-import javax.xml.parsers.DocumentBuilderFactory
-
-import scala.actors.Actor._
-import scala.collection.mutable
-
-
-object XML
-{
- /** XML trees **/
-
- /* datatype representation */
-
- type Attributes = Properties.T
-
- sealed abstract class Tree { override def toString = string_of_tree(this) }
- case class Elem(markup: Markup, body: List[Tree]) extends Tree
- case class Text(content: String) extends Tree
-
- def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
- def elem(name: String) = Elem(Markup(name, Nil), Nil)
-
- type Body = List[Tree]
-
-
- /* string representation */
-
- def string_of_body(body: Body): String =
- {
- val s = new StringBuilder
-
- def text(txt: String) {
- if (txt == null) s ++= txt
- else {
- for (c <- txt.iterator) c match {
- case '<' => s ++= "<"
- case '>' => s ++= ">"
- case '&' => s ++= "&"
- case '"' => s ++= """
- case '\'' => s ++= "'"
- case _ => s += c
- }
- }
- }
- def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
- def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
- def tree(t: Tree): Unit =
- t match {
- case Elem(markup, Nil) =>
- s ++= "<"; elem(markup); s ++= "/>"
- case Elem(markup, ts) =>
- s ++= "<"; elem(markup); s ++= ">"
- ts.foreach(tree)
- s ++= "</"; s ++= markup.name; s ++= ">"
- case Text(txt) => text(txt)
- }
- body.foreach(tree)
- s.toString
- }
-
- def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
-
-
- /* text content */
-
- def content_stream(tree: Tree): Stream[String] =
- tree match {
- case Elem(_, body) => content_stream(body)
- case Text(content) => Stream(content)
- }
- def content_stream(body: Body): Stream[String] =
- body.toStream.flatten(content_stream(_))
-
- def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
- def content(body: Body): Iterator[String] = content_stream(body).iterator
-
-
- /* pipe-lined cache for partial sharing */
-
- class Cache(initial_size: Int = 131071, max_string: Int = 100)
- {
- private val cache_actor = actor
- {
- val table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
-
- def lookup[A](x: A): Option[A] =
- {
- val ref = table.get(x)
- if (ref == null) None
- else {
- val y = ref.asInstanceOf[WeakReference[A]].get
- if (y == null) None
- else Some(y)
- }
- }
- def store[A](x: A): A =
- {
- table.put(x, new WeakReference[Any](x))
- x
- }
-
- def trim_bytes(s: String): String = new String(s.toCharArray)
-
- def cache_string(x: String): String =
- lookup(x) match {
- case Some(y) => y
- case None =>
- val z = trim_bytes(x)
- if (z.length > max_string) z else store(z)
- }
- def cache_props(x: Properties.T): Properties.T =
- if (x.isEmpty) x
- else
- lookup(x) match {
- case Some(y) => y
- case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
- }
- def cache_markup(x: Markup): Markup =
- lookup(x) match {
- case Some(y) => y
- case None =>
- x match {
- case Markup(name, props) =>
- store(Markup(cache_string(name), cache_props(props)))
- }
- }
- def cache_tree(x: XML.Tree): XML.Tree =
- lookup(x) match {
- case Some(y) => y
- case None =>
- x match {
- case XML.Elem(markup, body) =>
- store(XML.Elem(cache_markup(markup), cache_body(body)))
- case XML.Text(text) => store(XML.Text(cache_string(text)))
- }
- }
- def cache_body(x: XML.Body): XML.Body =
- if (x.isEmpty) x
- else
- lookup(x) match {
- case Some(y) => y
- case None => x.map(cache_tree(_))
- }
-
- // main loop
- loop {
- react {
- case Cache_String(x, f) => f(cache_string(x))
- case Cache_Markup(x, f) => f(cache_markup(x))
- case Cache_Tree(x, f) => f(cache_tree(x))
- case Cache_Body(x, f) => f(cache_body(x))
- case Cache_Ignore(x, f) => f(x)
- case bad => System.err.println("XML.cache_actor: ignoring bad input " + bad)
- }
- }
- }
-
- private case class Cache_String(x: String, f: String => Unit)
- private case class Cache_Markup(x: Markup, f: Markup => Unit)
- private case class Cache_Tree(x: XML.Tree, f: XML.Tree => Unit)
- private case class Cache_Body(x: XML.Body, f: XML.Body => Unit)
- private case class Cache_Ignore[A](x: A, f: A => Unit)
-
- // main methods
- def cache_string(x: String)(f: String => Unit) { cache_actor ! Cache_String(x, f) }
- def cache_markup(x: Markup)(f: Markup => Unit) { cache_actor ! Cache_Markup(x, f) }
- def cache_tree(x: XML.Tree)(f: XML.Tree => Unit) { cache_actor ! Cache_Tree(x, f) }
- def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) }
- def cache_ignore[A](x: A)(f: A => Unit) { cache_actor ! Cache_Ignore(x, f) }
- }
-
-
-
- /** document object model (W3C DOM) **/
-
- def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
- node.getUserData(Markup.Data.name) match {
- case tree: XML.Tree => Some(tree)
- case _ => None
- }
-
- def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
- {
- def DOM(tr: Tree): org.w3c.dom.Node = tr match {
- case Elem(Markup.Data, List(data, t)) =>
- val node = DOM(t)
- node.setUserData(Markup.Data.name, data, null)
- node
- case Elem(Markup(name, atts), ts) =>
- if (name == Markup.Data.name)
- error("Malformed data element: " + tr.toString)
- val node = doc.createElement(name)
- for ((name, value) <- atts) node.setAttribute(name, value)
- for (t <- ts) node.appendChild(DOM(t))
- node
- case Text(txt) => doc.createTextNode(txt)
- }
- DOM(tree)
- }
-
-
-
- /** XML as data representation language **/
-
- class XML_Atom(s: String) extends Exception(s)
- class XML_Body(body: XML.Body) extends Exception
-
- object Encode
- {
- type T[A] = A => XML.Body
-
-
- /* atomic values */
-
- def long_atom(i: Long): String = i.toString
-
- def int_atom(i: Int): String = i.toString
-
- def bool_atom(b: Boolean): String = if (b) "1" else "0"
-
- def unit_atom(u: Unit) = ""
-
-
- /* structural nodes */
-
- private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
-
- private def vector(xs: List[String]): XML.Attributes =
- xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
-
- private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
- XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
-
-
- /* representation of standard types */
-
- val properties: T[Properties.T] =
- (props => List(XML.Elem(Markup(":", props), Nil)))
-
- 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)))
-
- 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))))
-
- 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)))
- }
-
- def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
- {
- case x =>
- val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
- List(tagged(tag, f(x)))
- }
- }
-
- object Decode
- {
- type T[A] = XML.Body => A
- type V[A] = (List[String], XML.Body) => A
-
-
- /* atomic values */
-
- def long_atom(s: String): Long =
- try { java.lang.Long.parseLong(s) }
- catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
- def int_atom(s: String): Int =
- try { Integer.parseInt(s) }
- catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
- def bool_atom(s: String): Boolean =
- if (s == "1") true
- else if (s == "0") false
- else throw new XML_Atom(s)
-
- def unit_atom(s: String): Unit =
- if (s == "") () else throw new XML_Atom(s)
-
-
- /* 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 vector(atts: XML.Attributes): List[String] =
- {
- val xs = new mutable.ListBuffer[String]
- var i = 0
- for ((a, x) <- atts) {
- if (int_atom(a) == i) { xs += x; i = i + 1 }
- else throw new XML_Atom(a)
- }
- xs.toList
- }
-
- private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
- t match {
- case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
- case _ => throw new XML_Body(List(t))
- }
-
-
- /* representation of standard types */
-
- val properties: T[Properties.T] =
- {
- case List(XML.Elem(Markup(":", props), Nil)) => props
- case ts => throw new XML_Body(ts)
- }
-
- val string: T[String] =
- {
- case Nil => ""
- case List(XML.Text(s)) => s
- case ts => throw new XML_Body(ts)
- }
-
- val long: T[Long] = (x => long_atom(string(x)))
-
- val int: T[Int] = (x => int_atom(string(x)))
-
- val bool: T[Boolean] = (x => bool_atom(string(x)))
-
- val unit: T[Unit] = (x => unit_atom(string(x)))
-
- 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 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 list[A](f: T[A]): T[List[A]] =
- (ts => ts.map(t => f(node(t))))
-
- 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 variant[A](fs: List[V[A]]): T[A] =
- {
- case List(t) =>
- val (tag, (xs, ts)) = tagged(t)
- val f =
- try { fs(tag) }
- catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
- f(xs, ts)
- case ts => throw new XML_Body(ts)
- }
- }
-}
--- a/src/Pure/General/yxml.ML Sun Sep 04 21:03:54 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-(* Title: Pure/General/yxml.ML
- Author: Makarius
-
-Efficient text representation of XML trees using extra characters X
-and Y -- no escaping, may nest marked text verbatim.
-
-Markup <elem att="val" ...>...body...</elem> is encoded as:
-
- X Y name Y att=val ... X
- ...
- body
- ...
- X Y X
-*)
-
-signature YXML =
-sig
- val X: Symbol.symbol
- val Y: Symbol.symbol
- val embed_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
-end;
-
-structure YXML: YXML =
-struct
-
-(** string representation **)
-
-(* idempotent recoding of certain low ASCII control characters *)
-
-fun pseudo_utf8 c =
- if Symbol.is_ascii_control c
- then chr 192 ^ chr (128 + ord c)
- else c;
-
-fun embed_controls str =
- if exists_string Symbol.is_ascii_control str
- then translate_string pseudo_utf8 str
- else str;
-
-
-(* markers *)
-
-val X = chr 5;
-val Y = chr 6;
-val XY = X ^ Y;
-val XYX = XY ^ X;
-
-val detect = exists_string (fn s => s = X orelse s = Y);
-
-
-(* output *)
-
-fun output_markup (markup as (name, atts)) =
- if Markup.is_empty markup then Markup.no_output
- else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
-
-fun element name atts body =
- let val (pre, post) = output_markup (name, atts)
- in pre ^ implode body ^ post end;
-
-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 #>
- trees ts #>
- Buffer.add XYX
- | 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;
-
-
-
-(** efficient YXML parsing **)
-
-local
-
-(* splitting *)
-
-fun is_char s c = ord s = Char.ord c;
-
-val split_string =
- Substring.full #>
- Substring.tokens (is_char X) #>
- map (Substring.fields (is_char Y) #> map Substring.string);
-
-
-(* structural errors *)
-
-fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
-fun err_attribute () = err "bad attribute";
-fun err_element () = err "bad element";
-fun err_unbalanced "" = err "unbalanced element"
- | err_unbalanced name = err ("unbalanced element " ^ quote name);
-
-
-(* stack operations *)
-
-fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
-
-fun push "" _ _ = err_element ()
- | push name atts pending = ((name, atts), []) :: pending;
-
-fun pop ((("", _), _) :: _) = err_unbalanced ""
- | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
-
-
-(* parsing *)
-
-fun parse_attrib s =
- (case first_field "=" s of
- NONE => err_attribute ()
- | SOME ("", _) => err_attribute ()
- | SOME att => att);
-
-fun parse_chunk ["", ""] = pop
- | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
- | parse_chunk txts = fold (add o XML.Text) txts;
-
-in
-
-fun parse_body source =
- (case fold parse_chunk (split_string source) [(("", []), [])] of
- [(("", _), result)] => rev result
- | ((name, _), _) :: _ => err_unbalanced name);
-
-fun parse source =
- (case parse_body source of
- [result] => result
- | [] => XML.Text ""
- | _ => err "multiple results");
-
-end;
-
-end;
-
--- a/src/Pure/General/yxml.scala Sun Sep 04 21:03:54 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-/* Title: Pure/General/yxml.scala
- Author: Makarius
-
-Efficient text representation of XML trees.
-*/
-
-package isabelle
-
-
-import scala.collection.mutable
-
-
-object YXML
-{
- /* chunk markers */
-
- val X = '\5'
- val Y = '\6'
- val X_string = X.toString
- val Y_string = Y.toString
-
- def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
-
-
- /* string representation */ // FIXME byte array version with pseudo-utf-8 (!?)
-
- def string_of_body(body: XML.Body): String =
- {
- val s = new StringBuilder
- def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
- def tree(t: XML.Tree): Unit =
- t match {
- case XML.Elem(Markup(name, atts), ts) =>
- s += X; s += Y; s++= name; atts.foreach(attrib); s += X
- ts.foreach(tree)
- s += X; s += Y; s += X
- case XML.Text(text) => s ++= text
- }
- body.foreach(tree)
- s.toString
- }
-
- def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
-
-
- /* parsing */
-
- private def err(msg: String) = error("Malformed YXML: " + msg)
- private def err_attribute() = err("bad attribute")
- private def err_element() = err("bad element")
- private def err_unbalanced(name: String) =
- if (name == "") err("unbalanced element")
- else err("unbalanced element " + quote(name))
-
- private def parse_attrib(source: CharSequence) = {
- val s = source.toString
- val i = s.indexOf('=')
- if (i <= 0) err_attribute()
- (s.substring(0, i), s.substring(i + 1))
- }
-
-
- def parse_body(source: CharSequence): XML.Body =
- {
- /* stack operations */
-
- def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
- var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
-
- def add(x: XML.Tree)
- {
- (stack: @unchecked) match { case ((_, body) :: _) => body += x }
- }
-
- def push(name: String, atts: XML.Attributes)
- {
- if (name == "") err_element()
- else stack = (Markup(name, atts), buffer()) :: stack
- }
-
- def pop()
- {
- (stack: @unchecked) match {
- case ((Markup.Empty, _) :: _) => err_unbalanced("")
- case ((markup, body) :: pending) =>
- stack = pending
- add(XML.Elem(markup, body.toList))
- }
- }
-
-
- /* parse chunks */
-
- for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
- if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
- else {
- Library.chunks(chunk, Y).toList match {
- case ch :: name :: atts if ch.length == 0 =>
- push(name.toString, atts.map(parse_attrib))
- case txts => for (txt <- txts) add(XML.Text(txt.toString))
- }
- }
- }
- (stack: @unchecked) match {
- case List((Markup.Empty, body)) => body.toList
- case (Markup(name, _), _) :: _ => err_unbalanced(name)
- }
- }
-
- def parse(source: CharSequence): XML.Tree =
- parse_body(source) match {
- case List(result) => result
- case Nil => XML.Text("")
- case _ => err("multiple results")
- }
-
-
- /* failsafe parsing */
-
- private def markup_malformed(source: CharSequence) =
- XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
-
- def parse_body_failsafe(source: CharSequence): XML.Body =
- {
- try { parse_body(source) }
- catch { case ERROR(_) => List(markup_malformed(source)) }
- }
-
- def parse_failsafe(source: CharSequence): XML.Tree =
- {
- try { parse(source) }
- catch { case ERROR(_) => markup_malformed(source) }
- }
-}
--- a/src/Pure/IsaMakefile Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Pure/IsaMakefile Sun Sep 04 21:04:02 2011 -0700
@@ -105,8 +105,6 @@
General/table.ML \
General/timing.ML \
General/url.ML \
- General/xml.ML \
- General/yxml.ML \
Isar/args.ML \
Isar/attrib.ML \
Isar/auto_bind.ML \
@@ -158,6 +156,8 @@
ML/ml_thms.ML \
PIDE/document.ML \
PIDE/isar_document.ML \
+ PIDE/xml.ML \
+ PIDE/yxml.ML \
Proof/extraction.ML \
Proof/proof_checker.ML \
Proof/proof_rewrite_rules.ML \
--- a/src/Pure/ML/ml_lex.ML Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Pure/ML/ml_lex.ML Sun Sep 04 21:04:02 2011 -0700
@@ -106,8 +106,8 @@
val token_kind_markup =
fn Keyword => Markup.ML_keyword
- | Ident => Markup.ML_ident
- | LongIdent => Markup.ML_ident
+ | Ident => Markup.empty
+ | LongIdent => Markup.empty
| TypeVar => Markup.ML_tvar
| Word => Markup.ML_numeral
| Int => Markup.ML_numeral
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/xml.ML Sun Sep 04 21:04:02 2011 -0700
@@ -0,0 +1,363 @@
+(* Title: Pure/PIDE/xml.ML
+ Author: David Aspinall
+ Author: Stefan Berghofer
+ Author: Makarius
+
+Untyped XML trees and basic data representation.
+*)
+
+signature XML_DATA_OPS =
+sig
+ type 'a A
+ type 'a T
+ type 'a V
+ val int_atom: int A
+ val bool_atom: bool A
+ val unit_atom: unit A
+ 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 V list -> 'a T
+end;
+
+signature XML =
+sig
+ type attributes = Properties.T
+ datatype tree =
+ Elem of Markup.T * tree list
+ | Text of string
+ type body = tree list
+ val add_content: tree -> Buffer.T -> Buffer.T
+ val content_of: body -> string
+ val header: string
+ val text: string -> string
+ val element: string -> attributes -> string list -> string
+ val output_markup: Markup.T -> Output.output * Output.output
+ val string_of: tree -> string
+ val pretty: int -> tree -> Pretty.T
+ val output: tree -> TextIO.outstream -> unit
+ val parse_comments: string list -> unit * string list
+ val parse_string : string -> string option
+ val parse_element: string list -> tree * string list
+ val parse_document: string list -> tree * string list
+ val parse: string -> tree
+ exception XML_ATOM of string
+ exception XML_BODY of body
+ structure Encode: XML_DATA_OPS
+ structure Decode: XML_DATA_OPS
+end;
+
+structure XML: XML =
+struct
+
+(** XML trees **)
+
+type attributes = Properties.T;
+
+datatype tree =
+ Elem of Markup.T * tree list
+ | Text of string;
+
+type body = tree list;
+
+fun add_content (Elem (_, ts)) = fold add_content ts
+ | add_content (Text s) = Buffer.add s;
+
+fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
+
+
+
+(** string representation **)
+
+val header = "<?xml version=\"1.0\"?>\n";
+
+
+(* escaped text *)
+
+fun decode "<" = "<"
+ | decode ">" = ">"
+ | decode "&" = "&"
+ | decode "'" = "'"
+ | decode """ = "\""
+ | decode c = c;
+
+fun encode "<" = "<"
+ | encode ">" = ">"
+ | encode "&" = "&"
+ | encode "'" = "'"
+ | encode "\"" = """
+ | encode c = c;
+
+val text = translate_string encode;
+
+
+(* elements *)
+
+fun elem name atts =
+ space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
+
+fun element name atts body =
+ let val b = implode body in
+ if b = "" then enclose "<" "/>" (elem name atts)
+ else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
+ end;
+
+fun output_markup (markup as (name, atts)) =
+ if Markup.is_empty markup then Markup.no_output
+ else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
+
+
+(* output *)
+
+fun buffer_of depth tree =
+ let
+ fun traverse _ (Elem ((name, atts), [])) =
+ Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
+ | traverse d (Elem ((name, atts), ts)) =
+ Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
+ traverse_body d ts #>
+ Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
+ | traverse _ (Text s) = Buffer.add (text s)
+ and traverse_body 0 _ = Buffer.add "..."
+ | traverse_body d ts = fold (traverse (d - 1)) ts;
+ in Buffer.empty |> traverse depth tree end;
+
+val string_of = Buffer.content o buffer_of ~1;
+val output = Buffer.output o buffer_of ~1;
+
+fun pretty depth tree =
+ Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
+
+
+
+(** XML parsing **)
+
+local
+
+fun err msg (xs, _) =
+ fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
+
+fun ignored _ = [];
+
+val blanks = Scan.many Symbol.is_blank;
+val special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
+val regular = Scan.one Symbol.is_regular;
+fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
+
+val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
+
+val parse_cdata =
+ Scan.this_string "<![CDATA[" |--
+ (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
+ Scan.this_string "]]>";
+
+val parse_att =
+ (Symbol.scan_id --| (blanks -- $$ "=" -- blanks)) --
+ (($$ "\"" || $$ "'") :|-- (fn s =>
+ (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
+
+val parse_comment =
+ Scan.this_string "<!--" --
+ Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
+ Scan.this_string "-->" >> ignored;
+
+val parse_processing_instruction =
+ Scan.this_string "<?" --
+ Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
+ Scan.this_string "?>" >> ignored;
+
+val parse_doctype =
+ Scan.this_string "<!DOCTYPE" --
+ Scan.repeat (Scan.unless ($$ ">") regular) --
+ $$ ">" >> ignored;
+
+val parse_misc =
+ Scan.one Symbol.is_blank >> ignored ||
+ parse_processing_instruction ||
+ parse_comment;
+
+val parse_optional_text =
+ Scan.optional (parse_chars >> (single o Text)) [];
+
+fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
+fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
+val parse_name = Scan.one name_start_char ::: Scan.many name_char;
+
+in
+
+val parse_comments =
+ blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
+
+val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
+
+fun parse_content xs =
+ (parse_optional_text @@@
+ (Scan.repeat
+ ((parse_element >> single ||
+ parse_cdata >> (single o Text) ||
+ parse_processing_instruction ||
+ parse_comment)
+ @@@ parse_optional_text) >> flat)) xs
+
+and parse_element xs =
+ ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
+ (fn (name, _) =>
+ !! (err (fn () => "Expected > or />"))
+ ($$ "/" -- $$ ">" >> ignored ||
+ $$ ">" |-- parse_content --|
+ !! (err (fn () => "Expected </" ^ implode name ^ ">"))
+ ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
+ >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
+
+val parse_document =
+ (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
+ |-- parse_element;
+
+fun parse s =
+ (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
+ (blanks |-- parse_document --| blanks))) (raw_explode s) of
+ (x, []) => x
+ | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
+
+end;
+
+
+
+(** XML as data representation language **)
+
+exception XML_ATOM of string;
+exception XML_BODY of tree list;
+
+
+structure Encode =
+struct
+
+type 'a A = 'a -> string;
+type 'a T = 'a -> body;
+type 'a V = 'a -> string list * body;
+
+
+(* atomic values *)
+
+fun int_atom i = signed_string_of_int i;
+
+fun bool_atom false = "0"
+ | bool_atom true = "1";
+
+fun unit_atom () = "";
+
+
+(* structural nodes *)
+
+fun node ts = Elem ((":", []), ts);
+
+fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
+
+fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
+
+
+(* representation of standard types *)
+
+fun properties props = [Elem ((":", props), [])];
+
+fun string "" = []
+ | string s = [Text s];
+
+val int = string o int_atom;
+
+val bool = string o bool_atom;
+
+val unit = string o unit_atom;
+
+fun pair f g (x, y) = [node (f x), node (g y)];
+
+fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
+
+fun list f xs = map (node o f) xs;
+
+fun option _ NONE = []
+ | option f (SOME x) = [node (f x)];
+
+fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
+
+end;
+
+
+structure Decode =
+struct
+
+type 'a A = string -> 'a;
+type 'a T = body -> 'a;
+type 'a V = string list * body -> 'a;
+
+
+(* atomic values *)
+
+fun int_atom s =
+ Markup.parse_int s
+ handle Fail _ => 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 (Elem ((":", []), ts)) = ts
+ | node t = raise XML_BODY [t];
+
+fun vector atts =
+ #1 (fold_map (fn (a, x) =>
+ fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
+
+fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
+ | tagged t = raise XML_BODY [t];
+
+
+(* representation of standard types *)
+
+fun properties [Elem ((":", props), [])] = props
+ | properties ts = raise XML_BODY ts;
+
+fun string [] = ""
+ | string [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] =
+ let
+ val (tag, (xs, ts)) = tagged t;
+ val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
+ in f (xs, ts) end
+ | variant _ ts = raise XML_BODY ts;
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/xml.scala Sun Sep 04 21:04:02 2011 -0700
@@ -0,0 +1,368 @@
+/* Title: Pure/PIDE/xml.scala
+ Author: Makarius
+
+Untyped XML trees and basic data representation.
+*/
+
+package isabelle
+
+import java.lang.System
+import java.util.WeakHashMap
+import java.lang.ref.WeakReference
+import javax.xml.parsers.DocumentBuilderFactory
+
+import scala.actors.Actor._
+import scala.collection.mutable
+
+
+object XML
+{
+ /** XML trees **/
+
+ /* datatype representation */
+
+ type Attributes = Properties.T
+
+ sealed abstract class Tree { override def toString = string_of_tree(this) }
+ case class Elem(markup: Markup, body: List[Tree]) extends Tree
+ case class Text(content: String) extends Tree
+
+ def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
+ def elem(name: String) = Elem(Markup(name, Nil), Nil)
+
+ type Body = List[Tree]
+
+
+ /* string representation */
+
+ def string_of_body(body: Body): String =
+ {
+ val s = new StringBuilder
+
+ def text(txt: String) {
+ if (txt == null) s ++= txt
+ else {
+ for (c <- txt.iterator) c match {
+ case '<' => s ++= "<"
+ case '>' => s ++= ">"
+ case '&' => s ++= "&"
+ case '"' => s ++= """
+ case '\'' => s ++= "'"
+ case _ => s += c
+ }
+ }
+ }
+ def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
+ def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
+ def tree(t: Tree): Unit =
+ t match {
+ case Elem(markup, Nil) =>
+ s ++= "<"; elem(markup); s ++= "/>"
+ case Elem(markup, ts) =>
+ s ++= "<"; elem(markup); s ++= ">"
+ ts.foreach(tree)
+ s ++= "</"; s ++= markup.name; s ++= ">"
+ case Text(txt) => text(txt)
+ }
+ body.foreach(tree)
+ s.toString
+ }
+
+ def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
+
+
+ /* text content */
+
+ def content_stream(tree: Tree): Stream[String] =
+ tree match {
+ case Elem(_, body) => content_stream(body)
+ case Text(content) => Stream(content)
+ }
+ def content_stream(body: Body): Stream[String] =
+ body.toStream.flatten(content_stream(_))
+
+ def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
+ def content(body: Body): Iterator[String] = content_stream(body).iterator
+
+
+ /* pipe-lined cache for partial sharing */
+
+ class Cache(initial_size: Int = 131071, max_string: Int = 100)
+ {
+ private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
+
+ private def lookup[A](x: A): Option[A] =
+ {
+ val ref = table.get(x)
+ if (ref == null) None
+ else {
+ val y = ref.asInstanceOf[WeakReference[A]].get
+ if (y == null) None
+ else Some(y)
+ }
+ }
+ private def store[A](x: A): A =
+ {
+ table.put(x, new WeakReference[Any](x))
+ x
+ }
+
+ private def trim_bytes(s: String): String = new String(s.toCharArray)
+
+ private def _cache_string(x: String): String =
+ lookup(x) match {
+ case Some(y) => y
+ case None =>
+ val z = trim_bytes(x)
+ if (z.length > max_string) z else store(z)
+ }
+ private def _cache_props(x: Properties.T): Properties.T =
+ if (x.isEmpty) x
+ else
+ lookup(x) match {
+ case Some(y) => y
+ case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
+ }
+ private def _cache_markup(x: Markup): Markup =
+ lookup(x) match {
+ case Some(y) => y
+ case None =>
+ x match {
+ case Markup(name, props) =>
+ store(Markup(_cache_string(name), _cache_props(props)))
+ }
+ }
+ private def _cache_tree(x: XML.Tree): XML.Tree =
+ lookup(x) match {
+ case Some(y) => y
+ case None =>
+ x match {
+ case XML.Elem(markup, body) =>
+ store(XML.Elem(_cache_markup(markup), _cache_body(body)))
+ case XML.Text(text) => store(XML.Text(_cache_string(text)))
+ }
+ }
+ private def _cache_body(x: XML.Body): XML.Body =
+ if (x.isEmpty) x
+ else
+ lookup(x) match {
+ case Some(y) => y
+ case None => x.map(_cache_tree(_))
+ }
+
+ // main methods
+ def cache_string(x: String): String = synchronized { _cache_string(x) }
+ def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
+ def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
+ def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
+ }
+
+
+
+ /** document object model (W3C DOM) **/
+
+ def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
+ node.getUserData(Markup.Data.name) match {
+ case tree: XML.Tree => Some(tree)
+ case _ => None
+ }
+
+ def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
+ {
+ def DOM(tr: Tree): org.w3c.dom.Node = tr match {
+ case Elem(Markup.Data, List(data, t)) =>
+ val node = DOM(t)
+ node.setUserData(Markup.Data.name, data, null)
+ node
+ case Elem(Markup(name, atts), ts) =>
+ if (name == Markup.Data.name)
+ error("Malformed data element: " + tr.toString)
+ val node = doc.createElement(name)
+ for ((name, value) <- atts) node.setAttribute(name, value)
+ for (t <- ts) node.appendChild(DOM(t))
+ node
+ case Text(txt) => doc.createTextNode(txt)
+ }
+ DOM(tree)
+ }
+
+
+
+ /** XML as data representation language **/
+
+ class XML_Atom(s: String) extends Exception(s)
+ class XML_Body(body: XML.Body) extends Exception
+
+ object Encode
+ {
+ type T[A] = A => XML.Body
+
+
+ /* atomic values */
+
+ def long_atom(i: Long): String = i.toString
+
+ def int_atom(i: Int): String = i.toString
+
+ def bool_atom(b: Boolean): String = if (b) "1" else "0"
+
+ def unit_atom(u: Unit) = ""
+
+
+ /* structural nodes */
+
+ private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
+
+ private def vector(xs: List[String]): XML.Attributes =
+ xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
+
+ private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
+ XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
+
+
+ /* representation of standard types */
+
+ val properties: T[Properties.T] =
+ (props => List(XML.Elem(Markup(":", props), Nil)))
+
+ 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)))
+
+ 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))))
+
+ 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)))
+ }
+
+ def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
+ {
+ case x =>
+ val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
+ List(tagged(tag, f(x)))
+ }
+ }
+
+ object Decode
+ {
+ type T[A] = XML.Body => A
+ type V[A] = (List[String], XML.Body) => A
+
+
+ /* atomic values */
+
+ def long_atom(s: String): Long =
+ try { java.lang.Long.parseLong(s) }
+ catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+ def int_atom(s: String): Int =
+ try { Integer.parseInt(s) }
+ catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+ def bool_atom(s: String): Boolean =
+ if (s == "1") true
+ else if (s == "0") false
+ else throw new XML_Atom(s)
+
+ def unit_atom(s: String): Unit =
+ if (s == "") () else throw new XML_Atom(s)
+
+
+ /* 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 vector(atts: XML.Attributes): List[String] =
+ {
+ val xs = new mutable.ListBuffer[String]
+ var i = 0
+ for ((a, x) <- atts) {
+ if (int_atom(a) == i) { xs += x; i = i + 1 }
+ else throw new XML_Atom(a)
+ }
+ xs.toList
+ }
+
+ private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
+ t match {
+ case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
+ case _ => throw new XML_Body(List(t))
+ }
+
+
+ /* representation of standard types */
+
+ val properties: T[Properties.T] =
+ {
+ case List(XML.Elem(Markup(":", props), Nil)) => props
+ case ts => throw new XML_Body(ts)
+ }
+
+ val string: T[String] =
+ {
+ case Nil => ""
+ case List(XML.Text(s)) => s
+ case ts => throw new XML_Body(ts)
+ }
+
+ val long: T[Long] = (x => long_atom(string(x)))
+
+ val int: T[Int] = (x => int_atom(string(x)))
+
+ val bool: T[Boolean] = (x => bool_atom(string(x)))
+
+ val unit: T[Unit] = (x => unit_atom(string(x)))
+
+ 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 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 list[A](f: T[A]): T[List[A]] =
+ (ts => ts.map(t => f(node(t))))
+
+ 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 variant[A](fs: List[V[A]]): T[A] =
+ {
+ case List(t) =>
+ val (tag, (xs, ts)) = tagged(t)
+ val f =
+ try { fs(tag) }
+ catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
+ f(xs, ts)
+ case ts => throw new XML_Body(ts)
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/yxml.ML Sun Sep 04 21:04:02 2011 -0700
@@ -0,0 +1,148 @@
+(* Title: Pure/PIDE/yxml.ML
+ Author: Makarius
+
+Efficient text representation of XML trees using extra characters X
+and Y -- no escaping, may nest marked text verbatim. Suitable for
+direct inlining into plain text.
+
+Markup <elem att="val" ...>...body...</elem> is encoded as:
+
+ X Y name Y att=val ... X
+ ...
+ body
+ ...
+ X Y X
+*)
+
+signature YXML =
+sig
+ val X: Symbol.symbol
+ val Y: Symbol.symbol
+ val embed_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
+end;
+
+structure YXML: YXML =
+struct
+
+(** string representation **)
+
+(* idempotent recoding of certain low ASCII control characters *)
+
+fun pseudo_utf8 c =
+ if Symbol.is_ascii_control c
+ then chr 192 ^ chr (128 + ord c)
+ else c;
+
+fun embed_controls str =
+ if exists_string Symbol.is_ascii_control str
+ then translate_string pseudo_utf8 str
+ else str;
+
+
+(* markers *)
+
+val X = chr 5;
+val Y = chr 6;
+val XY = X ^ Y;
+val XYX = XY ^ X;
+
+val detect = exists_string (fn s => s = X orelse s = Y);
+
+
+(* output *)
+
+fun output_markup (markup as (name, atts)) =
+ if Markup.is_empty markup then Markup.no_output
+ else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
+
+fun element name atts body =
+ let val (pre, post) = output_markup (name, atts)
+ in pre ^ implode body ^ post end;
+
+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 #>
+ trees ts #>
+ Buffer.add XYX
+ | 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;
+
+
+
+(** efficient YXML parsing **)
+
+local
+
+(* splitting *)
+
+fun is_char s c = ord s = Char.ord c;
+
+val split_string =
+ Substring.full #>
+ Substring.tokens (is_char X) #>
+ map (Substring.fields (is_char Y) #> map Substring.string);
+
+
+(* structural errors *)
+
+fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
+fun err_attribute () = err "bad attribute";
+fun err_element () = err "bad element";
+fun err_unbalanced "" = err "unbalanced element"
+ | err_unbalanced name = err ("unbalanced element " ^ quote name);
+
+
+(* stack operations *)
+
+fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
+
+fun push "" _ _ = err_element ()
+ | push name atts pending = ((name, atts), []) :: pending;
+
+fun pop ((("", _), _) :: _) = err_unbalanced ""
+ | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
+
+
+(* parsing *)
+
+fun parse_attrib s =
+ (case first_field "=" s of
+ NONE => err_attribute ()
+ | SOME ("", _) => err_attribute ()
+ | SOME att => att);
+
+fun parse_chunk ["", ""] = pop
+ | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
+ | parse_chunk txts = fold (add o XML.Text) txts;
+
+in
+
+fun parse_body source =
+ (case fold parse_chunk (split_string source) [(("", []), [])] of
+ [(("", _), result)] => rev result
+ | ((name, _), _) :: _ => err_unbalanced name);
+
+fun parse source =
+ (case parse_body source of
+ [result] => result
+ | [] => XML.Text ""
+ | _ => err "multiple results");
+
+end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/yxml.scala Sun Sep 04 21:04:02 2011 -0700
@@ -0,0 +1,135 @@
+/* Title: Pure/PIDE/yxml.scala
+ Author: Makarius
+
+Efficient text representation of XML trees. Suitable for direct
+inlining into plain text.
+*/
+
+package isabelle
+
+
+import scala.collection.mutable
+
+
+object YXML
+{
+ /* chunk markers */
+
+ val X = '\5'
+ val Y = '\6'
+ val X_string = X.toString
+ val Y_string = Y.toString
+
+ def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
+
+
+ /* string representation */ // FIXME byte array version with pseudo-utf-8 (!?)
+
+ def string_of_body(body: XML.Body): String =
+ {
+ val s = new StringBuilder
+ def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
+ def tree(t: XML.Tree): Unit =
+ t match {
+ case XML.Elem(Markup(name, atts), ts) =>
+ s += X; s += Y; s++= name; atts.foreach(attrib); s += X
+ ts.foreach(tree)
+ s += X; s += Y; s += X
+ case XML.Text(text) => s ++= text
+ }
+ body.foreach(tree)
+ s.toString
+ }
+
+ def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
+
+
+ /* parsing */
+
+ private def err(msg: String) = error("Malformed YXML: " + msg)
+ private def err_attribute() = err("bad attribute")
+ private def err_element() = err("bad element")
+ private def err_unbalanced(name: String) =
+ if (name == "") err("unbalanced element")
+ else err("unbalanced element " + quote(name))
+
+ private def parse_attrib(source: CharSequence) = {
+ val s = source.toString
+ val i = s.indexOf('=')
+ if (i <= 0) err_attribute()
+ (s.substring(0, i), s.substring(i + 1))
+ }
+
+
+ def parse_body(source: CharSequence): XML.Body =
+ {
+ /* stack operations */
+
+ def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
+ var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
+
+ def add(x: XML.Tree)
+ {
+ (stack: @unchecked) match { case ((_, body) :: _) => body += x }
+ }
+
+ def push(name: String, atts: XML.Attributes)
+ {
+ if (name == "") err_element()
+ else stack = (Markup(name, atts), buffer()) :: stack
+ }
+
+ def pop()
+ {
+ (stack: @unchecked) match {
+ case ((Markup.Empty, _) :: _) => err_unbalanced("")
+ case ((markup, body) :: pending) =>
+ stack = pending
+ add(XML.Elem(markup, body.toList))
+ }
+ }
+
+
+ /* parse chunks */
+
+ for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
+ if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
+ else {
+ Library.chunks(chunk, Y).toList match {
+ case ch :: name :: atts if ch.length == 0 =>
+ push(name.toString, atts.map(parse_attrib))
+ case txts => for (txt <- txts) add(XML.Text(txt.toString))
+ }
+ }
+ }
+ (stack: @unchecked) match {
+ case List((Markup.Empty, body)) => body.toList
+ case (Markup(name, _), _) :: _ => err_unbalanced(name)
+ }
+ }
+
+ def parse(source: CharSequence): XML.Tree =
+ parse_body(source) match {
+ case List(result) => result
+ case Nil => XML.Text("")
+ case _ => err("multiple results")
+ }
+
+
+ /* failsafe parsing */
+
+ private def markup_malformed(source: CharSequence) =
+ XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
+
+ def parse_body_failsafe(source: CharSequence): XML.Body =
+ {
+ try { parse_body(source) }
+ catch { case ERROR(_) => List(markup_malformed(source)) }
+ }
+
+ def parse_failsafe(source: CharSequence): XML.Tree =
+ {
+ try { parse(source) }
+ catch { case ERROR(_) => markup_malformed(source) }
+ }
+}
--- a/src/Pure/ROOT.ML Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Pure/ROOT.ML Sun Sep 04 21:04:02 2011 -0700
@@ -54,17 +54,18 @@
use "General/linear_set.ML";
use "General/buffer.ML";
use "General/pretty.ML";
-use "General/xml.ML";
use "General/path.ML";
use "General/url.ML";
use "General/file.ML";
-use "General/yxml.ML";
use "General/long_name.ML";
use "General/binding.ML";
use "General/sha1.ML";
if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
+use "PIDE/xml.ML";
+use "PIDE/yxml.ML";
+
(* concurrency within the ML runtime *)
--- a/src/Pure/Syntax/lexicon.ML Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Pure/Syntax/lexicon.ML Sun Sep 04 21:04:02 2011 -0700
@@ -190,8 +190,8 @@
val token_kind_markup =
fn Literal => Markup.literal
- | IdentSy => Markup.ident
- | LongIdentSy => Markup.ident
+ | IdentSy => Markup.empty
+ | LongIdentSy => Markup.empty
| VarSy => Markup.var
| TFreeSy => Markup.tfree
| TVarSy => Markup.tvar
--- a/src/Pure/System/isabelle_process.scala Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Pure/System/isabelle_process.scala Sun Sep 04 21:04:02 2011 -0700
@@ -99,12 +99,10 @@
{
if (kind == Markup.INIT) rm_fifos()
if (kind == Markup.RAW)
- xml_cache.cache_ignore(
- new Result(XML.Elem(Markup(kind, props), body)))((result: Result) => receiver ! result)
+ receiver ! new Result(XML.Elem(Markup(kind, props), body))
else {
val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
- xml_cache.cache_tree(msg)((message: XML.Tree) =>
- receiver ! new Result(message.asInstanceOf[XML.Elem]))
+ receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
}
}
--- a/src/Pure/Thy/thy_syntax.ML Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.ML Sun Sep 04 21:04:02 2011 -0700
@@ -45,14 +45,14 @@
val token_kind_markup =
fn Token.Command => Markup.command
| Token.Keyword => Markup.keyword
- | Token.Ident => Markup.ident
- | Token.LongIdent => Markup.ident
- | Token.SymIdent => Markup.ident
+ | Token.Ident => Markup.empty
+ | Token.LongIdent => Markup.empty
+ | Token.SymIdent => Markup.empty
| Token.Var => Markup.var
| Token.TypeIdent => Markup.tfree
| Token.TypeVar => Markup.tvar
- | Token.Nat => Markup.ident
- | Token.Float => Markup.ident
+ | Token.Nat => Markup.empty
+ | Token.Float => Markup.empty
| Token.String => Markup.string
| Token.AltString => Markup.altstring
| Token.Verbatim => Markup.verbatim
--- a/src/Pure/build-jars Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Pure/build-jars Sun Sep 04 21:04:02 2011 -0700
@@ -24,8 +24,6 @@
General/scan.scala
General/sha1.scala
General/symbol.scala
- General/xml.scala
- General/yxml.scala
Isar/keyword.scala
Isar/outer_syntax.scala
Isar/parse.scala
@@ -36,6 +34,8 @@
PIDE/isar_document.scala
PIDE/markup_tree.scala
PIDE/text.scala
+ PIDE/xml.scala
+ PIDE/yxml.scala
System/cygwin.scala
System/download.scala
System/event_bus.scala
--- a/src/Tools/jEdit/README Sun Sep 04 21:03:54 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-Isabelle/jEdit based on Isabelle/Scala
-======================================
-
-The Isabelle/Scala layer that is already part of Isabelle/Pure
-provides some general infrastructure for advanced prover interaction
-and integration. The Isabelle/jEdit application serves as an example
-for asynchronous proof checking with support for parallel processing.
-
-See also the paper:
-
- Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala
- and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors,
- User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite
- Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS.
- http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf
-
-
-Known problems with Mac OS
-==========================
-
-- The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
- e.g. between the editor and the Console plugin, which is a standard
- swing text box. Similar for search boxes etc.
-
-- ToggleButton selected state is not rendered if window focus is lost,
- which is probably a genuine feature of the Apple look-and-feel.
-
-- Anti-aliasing does not really work as well as for Linux or Windows.
- (General Apple/Swing problem?)
-
-- Font.createFont mangles the font family of non-regular fonts,
- e.g. bold. IsabelleText font files need to be installed manually.
-
-- Missing glyphs are collected from other fonts (like Emacs, Firefox).
- This is actually an advantage over the Oracle/Sun JVM on Windows or
- Linux, but probably also the deeper reason for the other oddities of
- Apple font management.
-
-- The native font renderer of -Dapple.awt.graphics.UseQuartz=true
- fails to handle the infinitesimal font size of "hidden" text (e.g.
- used in Isabelle sub/superscripts).
-
-
-Known problems with OpenJDK
-===========================
-
-- The 2D rendering engine of OpenJDK 1.6.x distorts the appearance of
- the jEdit text area. Always use official JRE 1.6.x from
- Sun/Oracle/Apple.
-
-
-Licenses and home sites of contributing systems
-===============================================
-
-* Scala: BSD-style
- http://www.scala-lang.org
-
-* jEdit: GPL (with special cases)
- http://www.jedit.org/
-
-* Lobo/Cobra: GPL and LGPL
- http://lobobrowser.org/
--- a/src/Tools/jEdit/README.html Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Tools/jEdit/README.html Sun Sep 04 21:04:02 2011 -0700
@@ -12,7 +12,12 @@
<body>
-<h2>The Isabelle/jEdit Prover IDE</h2>
+<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
+
+The Isabelle/Scala layer that is already part of Isabelle/Pure
+provides some general infrastructure for advanced prover interaction
+and integration. The Isabelle/jEdit application serves as an example
+for asynchronous proof checking with support for parallel processing.
<ul>
@@ -116,30 +121,23 @@
</ul>
-<h2>Limitations and workrounds (January 2011)</h2>
+<h2>Limitations and workrounds (September 2011)</h2>
<ul>
<li>No way to start/stop prover or switch to a different logic.<br/>
<em>Workaround:</em> Change options and restart editor.</li>
- <li>Limited support for dependencies between multiple theory buffers.<br/>
- <em>Workaround:</em> Load required files manually.</li>
-
- <li>No reclaiming of old/unused document versions in prover or
- editor.<br/>
- <em>Workaround:</em> Avoid large files; restart after a few hours of use.</li>
-
<li>Incremental reparsing sometimes produces unexpected command
spans.<br/>
<em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
- <li>Command execution sometimes gets stuck (purple background).<br/>
- <em>Workaround:</em> Force reparsing as above.</li>
+ <li>Odd behavior of some diagnostic commands, notably those starting
+ external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/>
+ <em>Workaround:</em> Avoid such commands.</li>
- <li>Odd behavior of some diagnostic commands, notably those
- starting external processes asynchronously
- (e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/>
- <em>Workaround:</em> Avoid such commands.</li>
+ <li>Lack of dependency managed for auxiliary files that contribute
+ to a theory ("<b>uses</b>").<br/>
+ <em>Workaround:</em> Re-use files manually within the prover.</li>
<li>No support for non-local markup, e.g. commands reporting on
previous commands (proof end on proof head), or markup produced by
@@ -149,6 +147,59 @@
General.</li>
</ul>
+
+<h2>Known problems with Mac OS</h2>
+
+<ul>
+
+<li>The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
+ e.g. between the editor and the Console plugin, which is a standard
+ swing text box. Similar for search boxes etc.</li>
+
+<li>ToggleButton selected state is not rendered if window focus is
+ lost, which is probably a genuine feature of the Apple
+ look-and-feel.</li>
+
+<li>Font.createFont mangles the font family of non-regular fonts,
+ e.g. bold. IsabelleText font files need to be installed/updated
+ manually.</li>
+
+<li>Missing glyphs are collected from other fonts (like Emacs,
+ Firefox). This is actually an advantage over the Oracle/Sun JVM on
+ Windows or Linux, but probably also the deeper reason for the other
+ oddities of Apple font management.</li>
+
+<li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true
+ (not enabled by default) fails to handle the infinitesimal font size
+ of "hidden" text (e.g. used in Isabelle sub/superscripts).</li>
+
+</ul>
+
+
+<h2>Known problems with OpenJDK 1.6.x</h2>
+
+<ul>
+
+<li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
+ of the jEdit text area. Always use official JRE 1.6.x from
+ Sun/Oracle/Apple.</li>
+
+<li>jEdit on OpenJDK is generally not supported.</li>
+
+</ul>
+
+
+<h2>Licenses and home sites of contributing systems</h2>
+
+<ul>
+
+<li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
+
+<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
+
+<li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org/</li>
+
+</ul>
+
</body>
</html>
-
--- a/src/Tools/jEdit/README_BUILD Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Tools/jEdit/README_BUILD Sun Sep 04 21:04:02 2011 -0700
@@ -1,14 +1,14 @@
Requirements for instantaneous build from sources
=================================================
-* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_26
- http://java.sun.com/javase/downloads/index.jsp
+* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_27
+ http://www.oracle.com/technetwork/java/javase/downloads/index.html
* Scala Compiler 2.8.1.final
http://www.scala-lang.org
* Auxiliary jedit_build component
- http://www4.in.tum.de/~wenzelm/test/jedit_build-20110521.tar.gz
+ http://www4.in.tum.de/~wenzelm/test/jedit_build-20110622.tar.gz
Important settings within Isabelle environment
--- a/src/Tools/jEdit/src/isabelle_markup.scala Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Sun Sep 04 21:04:02 2011 -0700
@@ -128,10 +128,7 @@
}
private val text_entity_colors: Map[String, Color] =
- Map(
- Markup.CLASS -> get_color("red"),
- Markup.TYPE -> get_color("black"),
- Markup.CONSTANT -> get_color("black"))
+ Map(Markup.CLASS -> get_color("red"))
private val text_colors: Map[String, Color] =
Map(
@@ -140,7 +137,6 @@
Markup.VERBATIM -> get_color("black"),
Markup.LITERAL -> keyword1_color,
Markup.DELIMITER -> get_color("black"),
- Markup.IDENT -> get_color("black"),
Markup.TFREE -> get_color("#A020F0"),
Markup.TVAR -> get_color("#A020F0"),
Markup.FREE -> get_color("blue"),
--- a/src/Tools/jEdit/src/isabelle_options.scala Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Tools/jEdit/src/isabelle_options.scala Sun Sep 04 21:04:02 2011 -0700
@@ -63,6 +63,6 @@
tooltip_margin.getValue().asInstanceOf[Int]
Isabelle.Time_Property("tooltip-dismiss-delay") =
- Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
+ Time.ms(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
}
}
--- a/src/Tools/jEdit/src/plugin.scala Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala Sun Sep 04 21:04:02 2011 -0700
@@ -123,8 +123,10 @@
Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?)
HTML.encode(text) + "</pre></html>"
+ private val tooltip_lb = Time.seconds(0.5)
+ private val tooltip_ub = Time.seconds(60.0)
def tooltip_dismiss_delay(): Time =
- Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
+ Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub
def setup_tooltips()
{
--- a/src/Tools/jEdit/src/token_markup.scala Sun Sep 04 21:03:54 2011 -0700
+++ b/src/Tools/jEdit/src/token_markup.scala Sun Sep 04 21:04:02 2011 -0700
@@ -173,41 +173,42 @@
case _ => Some(Scan.Finished)
}
val context1 =
- if (line_ctxt.isDefined && Isabelle.session.is_ready) {
- val syntax = Isabelle.session.current_syntax()
-
- val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
- val context1 = new Line_Context(Some(ctxt1))
-
- val extended = extended_styles(line)
-
- var offset = 0
- for (token <- tokens) {
- val style = Isabelle_Markup.token_markup(syntax, token)
- val length = token.source.length
- val end_offset = offset + length
- if ((offset until end_offset) exists extended.isDefinedAt) {
- for (i <- offset until end_offset) {
- val style1 =
- extended.get(i) match {
- case None => style
- case Some(ext) => ext(style)
- }
- handler.handleToken(line, style1, i, 1, context1)
- }
+ {
+ val (styled_tokens, context1) =
+ if (line_ctxt.isDefined && Isabelle.session.is_ready) {
+ val syntax = Isabelle.session.current_syntax()
+ val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
+ val styled_tokens = tokens.map(tok => (Isabelle_Markup.token_markup(syntax, tok), tok))
+ (styled_tokens, new Line_Context(Some(ctxt1)))
+ }
+ else {
+ val token = Token(Token.Kind.UNPARSED, line.subSequence(0, line.count).toString)
+ (List((JEditToken.NULL, token)), new Line_Context(None))
+ }
+
+ val extended = extended_styles(line)
+
+ var offset = 0
+ for ((style, token) <- styled_tokens) {
+ val length = token.source.length
+ val end_offset = offset + length
+ if ((offset until end_offset) exists
+ (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
+ for (i <- offset until end_offset) {
+ val style1 =
+ extended.get(i) match {
+ case None => style
+ case Some(ext) => ext(style)
+ }
+ handler.handleToken(line, style1, i, 1, context1)
}
- else handler.handleToken(line, style, offset, length, context1)
- offset += length
}
- handler.handleToken(line, JEditToken.END, line.count, 0, context1)
- context1
+ else handler.handleToken(line, style, offset, length, context1)
+ offset += length
}
- else {
- val context1 = new Line_Context(None)
- handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
- handler.handleToken(line, JEditToken.END, line.count, 0, context1)
- context1
- }
+ handler.handleToken(line, JEditToken.END, line.count, 0, context1)
+ context1
+ }
val context2 = context1.intern
handler.setLineContext(context2)
context2