merged
authorwenzelm
Sun Sep 04 20:37:20 2011 +0200 (2011-09-04)
changeset 447138c3d4063bf52
parent 44712 1e490e891c88
parent 44706 fe319b45315c
child 44716 d37afb90c23e
merged
src/Pure/General/xml.ML
src/Pure/General/xml.scala
src/Pure/General/yxml.ML
src/Pure/General/yxml.scala
src/Tools/jEdit/README
     1.1 --- a/etc/isabelle.css	Sun Sep 04 10:29:38 2011 -0700
     1.2 +++ b/etc/isabelle.css	Sun Sep 04 20:37:20 2011 +0200
     1.3 @@ -40,7 +40,6 @@
     1.4  .keyword        { font-weight: bold; }
     1.5  .operator       { }
     1.6  .command        { font-weight: bold; }
     1.7 -.ident          { }
     1.8  .string         { color: #008B00; }
     1.9  .altstring      { color: #8B8B00; }
    1.10  .verbatim       { color: #00008B; }
     2.1 --- a/src/HOL/Unix/Nested_Environment.thy	Sun Sep 04 10:29:38 2011 -0700
     2.2 +++ b/src/HOL/Unix/Nested_Environment.thy	Sun Sep 04 20:37:20 2011 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  begin
     2.5  
     2.6  text {*
     2.7 -  Consider a partial function @{term [source] "e :: 'a => 'b option"};
     2.8 +  Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"};
     2.9    this may be understood as an \emph{environment} mapping indexes
    2.10    @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
    2.11    @{text Map} of Isabelle/HOL).  This basic idea is easily generalized
    2.12 @@ -21,7 +21,7 @@
    2.13  
    2.14  datatype ('a, 'b, 'c) env =
    2.15      Val 'a
    2.16 -  | Env 'b  "'c => ('a, 'b, 'c) env option"
    2.17 +  | Env 'b  "'c \<Rightarrow> ('a, 'b, 'c) env option"
    2.18  
    2.19  text {*
    2.20    \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
    2.21 @@ -43,14 +43,14 @@
    2.22    @{term None}.
    2.23  *}
    2.24  
    2.25 -primrec lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
    2.26 -  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
    2.27 +primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
    2.28 +  and lookup_option :: "('a, 'b, 'c) env option \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
    2.29  where
    2.30      "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
    2.31    | "lookup (Env b es) xs =
    2.32        (case xs of
    2.33 -        [] => Some (Env b es)
    2.34 -      | y # ys => lookup_option (es y) ys)"
    2.35 +        [] \<Rightarrow> Some (Env b es)
    2.36 +      | y # ys \<Rightarrow> lookup_option (es y) ys)"
    2.37    | "lookup_option None xs = None"
    2.38    | "lookup_option (Some e) xs = lookup e xs"
    2.39  
    2.40 @@ -70,8 +70,8 @@
    2.41  theorem lookup_env_cons:
    2.42    "lookup (Env b es) (x # xs) =
    2.43      (case es x of
    2.44 -      None => None
    2.45 -    | Some e => lookup e xs)"
    2.46 +      None \<Rightarrow> None
    2.47 +    | Some e \<Rightarrow> lookup e xs)"
    2.48    by (cases "es x") simp_all
    2.49  
    2.50  lemmas lookup_lookup_option.simps [simp del]
    2.51 @@ -80,14 +80,14 @@
    2.52  theorem lookup_eq:
    2.53    "lookup env xs =
    2.54      (case xs of
    2.55 -      [] => Some env
    2.56 -    | x # xs =>
    2.57 +      [] \<Rightarrow> Some env
    2.58 +    | x # xs \<Rightarrow>
    2.59        (case env of
    2.60 -        Val a => None
    2.61 -      | Env b es =>
    2.62 +        Val a \<Rightarrow> None
    2.63 +      | Env b es \<Rightarrow>
    2.64            (case es x of
    2.65 -            None => None
    2.66 -          | Some e => lookup e xs)))"
    2.67 +            None \<Rightarrow> None
    2.68 +          | Some e \<Rightarrow> lookup e xs)))"
    2.69    by (simp split: list.split env.split)
    2.70  
    2.71  text {*
    2.72 @@ -245,18 +245,18 @@
    2.73    environment is left unchanged.
    2.74  *}
    2.75  
    2.76 -primrec update :: "'c list => ('a, 'b, 'c) env option =>
    2.77 -    ('a, 'b, 'c) env => ('a, 'b, 'c) env"
    2.78 -  and update_option :: "'c list => ('a, 'b, 'c) env option =>
    2.79 -    ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
    2.80 +primrec update :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
    2.81 +    ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"
    2.82 +  and update_option :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
    2.83 +    ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env option"
    2.84  where
    2.85    "update xs opt (Val a) =
    2.86 -    (if xs = [] then (case opt of None => Val a | Some e => e)
    2.87 +    (if xs = [] then (case opt of None \<Rightarrow> Val a | Some e \<Rightarrow> e)
    2.88       else Val a)"
    2.89  | "update xs opt (Env b es) =
    2.90      (case xs of
    2.91 -      [] => (case opt of None => Env b es | Some e => e)
    2.92 -    | y # ys => Env b (es (y := update_option ys opt (es y))))"
    2.93 +      [] \<Rightarrow> (case opt of None \<Rightarrow> Env b es | Some e \<Rightarrow> e)
    2.94 +    | y # ys \<Rightarrow> Env b (es (y := update_option ys opt (es y))))"
    2.95  | "update_option xs opt None =
    2.96      (if xs = [] then opt else None)"
    2.97  | "update_option xs opt (Some e) =
    2.98 @@ -286,8 +286,8 @@
    2.99    "update (x # y # ys) opt (Env b es) =
   2.100      Env b (es (x :=
   2.101        (case es x of
   2.102 -        None => None
   2.103 -      | Some e => Some (update (y # ys) opt e))))"
   2.104 +        None \<Rightarrow> None
   2.105 +      | Some e \<Rightarrow> Some (update (y # ys) opt e))))"
   2.106    by (cases "es x") simp_all
   2.107  
   2.108  lemmas update_update_option.simps [simp del]
   2.109 @@ -297,21 +297,21 @@
   2.110  lemma update_eq:
   2.111    "update xs opt env =
   2.112      (case xs of
   2.113 -      [] =>
   2.114 +      [] \<Rightarrow>
   2.115          (case opt of
   2.116 -          None => env
   2.117 -        | Some e => e)
   2.118 -    | x # xs =>
   2.119 +          None \<Rightarrow> env
   2.120 +        | Some e \<Rightarrow> e)
   2.121 +    | x # xs \<Rightarrow>
   2.122          (case env of
   2.123 -          Val a => Val a
   2.124 -        | Env b es =>
   2.125 +          Val a \<Rightarrow> Val a
   2.126 +        | Env b es \<Rightarrow>
   2.127              (case xs of
   2.128 -              [] => Env b (es (x := opt))
   2.129 -            | y # ys =>
   2.130 +              [] \<Rightarrow> Env b (es (x := opt))
   2.131 +            | y # ys \<Rightarrow>
   2.132                  Env b (es (x :=
   2.133                    (case es x of
   2.134 -                    None => None
   2.135 -                  | Some e => Some (update (y # ys) opt e)))))))"
   2.136 +                    None \<Rightarrow> None
   2.137 +                  | Some e \<Rightarrow> Some (update (y # ys) opt e)))))))"
   2.138    by (simp split: list.split env.split option.split)
   2.139  
   2.140  text {*
     3.1 --- a/src/Pure/General/markup.ML	Sun Sep 04 10:29:38 2011 -0700
     3.2 +++ b/src/Pure/General/markup.ML	Sun Sep 04 20:37:20 2011 +0200
     3.3 @@ -58,7 +58,6 @@
     3.4    val propN: string val prop: T
     3.5    val ML_keywordN: string val ML_keyword: T
     3.6    val ML_delimiterN: string val ML_delimiter: T
     3.7 -  val ML_identN: string val ML_ident: T
     3.8    val ML_tvarN: string val ML_tvar: T
     3.9    val ML_numeralN: string val ML_numeral: T
    3.10    val ML_charN: string val ML_char: T
    3.11 @@ -80,7 +79,6 @@
    3.12    val keywordN: string val keyword: T
    3.13    val operatorN: string val operator: T
    3.14    val commandN: string val command: T
    3.15 -  val identN: string val ident: T
    3.16    val stringN: string val string: T
    3.17    val altstringN: string val altstring: T
    3.18    val verbatimN: string val verbatim: T
    3.19 @@ -257,7 +255,6 @@
    3.20  
    3.21  val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
    3.22  val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
    3.23 -val (ML_identN, ML_ident) = markup_elem "ML_ident";
    3.24  val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
    3.25  val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
    3.26  val (ML_charN, ML_char) = markup_elem "ML_char";
    3.27 @@ -292,7 +289,6 @@
    3.28  val (keywordN, keyword) = markup_elem "keyword";
    3.29  val (operatorN, operator) = markup_elem "operator";
    3.30  val (commandN, command) = markup_elem "command";
    3.31 -val (identN, ident) = markup_elem "ident";
    3.32  val (stringN, string) = markup_elem "string";
    3.33  val (altstringN, altstring) = markup_elem "altstring";
    3.34  val (verbatimN, verbatim) = markup_elem "verbatim";
     4.1 --- a/src/Pure/General/markup.scala	Sun Sep 04 10:29:38 2011 -0700
     4.2 +++ b/src/Pure/General/markup.scala	Sun Sep 04 20:37:20 2011 +0200
     4.3 @@ -142,7 +142,6 @@
     4.4  
     4.5    val ML_KEYWORD = "ML_keyword"
     4.6    val ML_DELIMITER = "ML_delimiter"
     4.7 -  val ML_IDENT = "ML_ident"
     4.8    val ML_TVAR = "ML_tvar"
     4.9    val ML_NUMERAL = "ML_numeral"
    4.10    val ML_CHAR = "ML_char"
    4.11 @@ -164,7 +163,6 @@
    4.12    val KEYWORD = "keyword"
    4.13    val OPERATOR = "operator"
    4.14    val COMMAND = "command"
    4.15 -  val IDENT = "ident"
    4.16    val STRING = "string"
    4.17    val ALTSTRING = "altstring"
    4.18    val VERBATIM = "verbatim"
     5.1 --- a/src/Pure/General/timing.scala	Sun Sep 04 10:29:38 2011 -0700
     5.2 +++ b/src/Pure/General/timing.scala	Sun Sep 04 20:37:20 2011 +0200
     5.3 @@ -9,6 +9,7 @@
     5.4  object Time
     5.5  {
     5.6    def seconds(s: Double): Time = new Time((s * 1000.0) round)
     5.7 +  def ms(m: Long): Time = new Time(m)
     5.8  }
     5.9  
    5.10  class Time(val ms: Long)
     6.1 --- a/src/Pure/General/xml.ML	Sun Sep 04 10:29:38 2011 -0700
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,361 +0,0 @@
     6.4 -(*  Title:      Pure/General/xml.ML
     6.5 -    Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
     6.6 -
     6.7 -Untyped XML trees.
     6.8 -*)
     6.9 -
    6.10 -signature XML_DATA_OPS =
    6.11 -sig
    6.12 -  type 'a A
    6.13 -  type 'a T
    6.14 -  type 'a V
    6.15 -  val int_atom: int A
    6.16 -  val bool_atom: bool A
    6.17 -  val unit_atom: unit A
    6.18 -  val properties: Properties.T T
    6.19 -  val string: string T
    6.20 -  val int: int T
    6.21 -  val bool: bool T
    6.22 -  val unit: unit T
    6.23 -  val pair: 'a T -> 'b T -> ('a * 'b) T
    6.24 -  val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
    6.25 -  val list: 'a T -> 'a list T
    6.26 -  val option: 'a T -> 'a option T
    6.27 -  val variant: 'a V list -> 'a T
    6.28 -end;
    6.29 -
    6.30 -signature XML =
    6.31 -sig
    6.32 -  type attributes = Properties.T
    6.33 -  datatype tree =
    6.34 -      Elem of Markup.T * tree list
    6.35 -    | Text of string
    6.36 -  type body = tree list
    6.37 -  val add_content: tree -> Buffer.T -> Buffer.T
    6.38 -  val content_of: body -> string
    6.39 -  val header: string
    6.40 -  val text: string -> string
    6.41 -  val element: string -> attributes -> string list -> string
    6.42 -  val output_markup: Markup.T -> Output.output * Output.output
    6.43 -  val string_of: tree -> string
    6.44 -  val pretty: int -> tree -> Pretty.T
    6.45 -  val output: tree -> TextIO.outstream -> unit
    6.46 -  val parse_comments: string list -> unit * string list
    6.47 -  val parse_string : string -> string option
    6.48 -  val parse_element: string list -> tree * string list
    6.49 -  val parse_document: string list -> tree * string list
    6.50 -  val parse: string -> tree
    6.51 -  exception XML_ATOM of string
    6.52 -  exception XML_BODY of body
    6.53 -  structure Encode: XML_DATA_OPS
    6.54 -  structure Decode: XML_DATA_OPS
    6.55 -end;
    6.56 -
    6.57 -structure XML: XML =
    6.58 -struct
    6.59 -
    6.60 -(** XML trees **)
    6.61 -
    6.62 -type attributes = Properties.T;
    6.63 -
    6.64 -datatype tree =
    6.65 -    Elem of Markup.T * tree list
    6.66 -  | Text of string;
    6.67 -
    6.68 -type body = tree list;
    6.69 -
    6.70 -fun add_content (Elem (_, ts)) = fold add_content ts
    6.71 -  | add_content (Text s) = Buffer.add s;
    6.72 -
    6.73 -fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
    6.74 -
    6.75 -
    6.76 -
    6.77 -(** string representation **)
    6.78 -
    6.79 -val header = "<?xml version=\"1.0\"?>\n";
    6.80 -
    6.81 -
    6.82 -(* escaped text *)
    6.83 -
    6.84 -fun decode "&lt;" = "<"
    6.85 -  | decode "&gt;" = ">"
    6.86 -  | decode "&amp;" = "&"
    6.87 -  | decode "&apos;" = "'"
    6.88 -  | decode "&quot;" = "\""
    6.89 -  | decode c = c;
    6.90 -
    6.91 -fun encode "<" = "&lt;"
    6.92 -  | encode ">" = "&gt;"
    6.93 -  | encode "&" = "&amp;"
    6.94 -  | encode "'" = "&apos;"
    6.95 -  | encode "\"" = "&quot;"
    6.96 -  | encode c = c;
    6.97 -
    6.98 -val text = translate_string encode;
    6.99 -
   6.100 -
   6.101 -(* elements *)
   6.102 -
   6.103 -fun elem name atts =
   6.104 -  space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
   6.105 -
   6.106 -fun element name atts body =
   6.107 -  let val b = implode body in
   6.108 -    if b = "" then enclose "<" "/>" (elem name atts)
   6.109 -    else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
   6.110 -  end;
   6.111 -
   6.112 -fun output_markup (markup as (name, atts)) =
   6.113 -  if Markup.is_empty markup then Markup.no_output
   6.114 -  else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
   6.115 -
   6.116 -
   6.117 -(* output *)
   6.118 -
   6.119 -fun buffer_of depth tree =
   6.120 -  let
   6.121 -    fun traverse _ (Elem ((name, atts), [])) =
   6.122 -          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
   6.123 -      | traverse d (Elem ((name, atts), ts)) =
   6.124 -          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
   6.125 -          traverse_body d ts #>
   6.126 -          Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
   6.127 -      | traverse _ (Text s) = Buffer.add (text s)
   6.128 -    and traverse_body 0 _ = Buffer.add "..."
   6.129 -      | traverse_body d ts = fold (traverse (d - 1)) ts;
   6.130 -  in Buffer.empty |> traverse depth tree end;
   6.131 -
   6.132 -val string_of = Buffer.content o buffer_of ~1;
   6.133 -val output = Buffer.output o buffer_of ~1;
   6.134 -
   6.135 -fun pretty depth tree =
   6.136 -  Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
   6.137 -
   6.138 -
   6.139 -
   6.140 -(** XML parsing (slow) **)
   6.141 -
   6.142 -local
   6.143 -
   6.144 -fun err msg (xs, _) =
   6.145 -  fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
   6.146 -
   6.147 -fun ignored _ = [];
   6.148 -
   6.149 -val blanks = Scan.many Symbol.is_blank;
   6.150 -val special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
   6.151 -val regular = Scan.one Symbol.is_regular;
   6.152 -fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
   6.153 -
   6.154 -val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
   6.155 -
   6.156 -val parse_cdata =
   6.157 -  Scan.this_string "<![CDATA[" |--
   6.158 -  (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
   6.159 -  Scan.this_string "]]>";
   6.160 -
   6.161 -val parse_att =
   6.162 -  (Symbol.scan_id --| (blanks -- $$ "=" -- blanks)) --
   6.163 -  (($$ "\"" || $$ "'") :|-- (fn s =>
   6.164 -    (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
   6.165 -
   6.166 -val parse_comment =
   6.167 -  Scan.this_string "<!--" --
   6.168 -  Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
   6.169 -  Scan.this_string "-->" >> ignored;
   6.170 -
   6.171 -val parse_processing_instruction =
   6.172 -  Scan.this_string "<?" --
   6.173 -  Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
   6.174 -  Scan.this_string "?>" >> ignored;
   6.175 -
   6.176 -val parse_doctype =
   6.177 -  Scan.this_string "<!DOCTYPE" --
   6.178 -  Scan.repeat (Scan.unless ($$ ">") regular) --
   6.179 -  $$ ">" >> ignored;
   6.180 -
   6.181 -val parse_misc =
   6.182 -  Scan.one Symbol.is_blank >> ignored ||
   6.183 -  parse_processing_instruction ||
   6.184 -  parse_comment;
   6.185 -
   6.186 -val parse_optional_text =
   6.187 -  Scan.optional (parse_chars >> (single o Text)) [];
   6.188 -
   6.189 -fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
   6.190 -fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
   6.191 -val parse_name = Scan.one name_start_char ::: Scan.many name_char;
   6.192 -
   6.193 -in
   6.194 -
   6.195 -val parse_comments =
   6.196 -  blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
   6.197 -
   6.198 -val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
   6.199 -
   6.200 -fun parse_content xs =
   6.201 -  (parse_optional_text @@@
   6.202 -    (Scan.repeat
   6.203 -      ((parse_element >> single ||
   6.204 -        parse_cdata >> (single o Text) ||
   6.205 -        parse_processing_instruction ||
   6.206 -        parse_comment)
   6.207 -      @@@ parse_optional_text) >> flat)) xs
   6.208 -
   6.209 -and parse_element xs =
   6.210 -  ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
   6.211 -    (fn (name, _) =>
   6.212 -      !! (err (fn () => "Expected > or />"))
   6.213 -       ($$ "/" -- $$ ">" >> ignored ||
   6.214 -        $$ ">" |-- parse_content --|
   6.215 -          !! (err (fn () => "Expected </" ^ implode name ^ ">"))
   6.216 -              ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
   6.217 -    >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
   6.218 -
   6.219 -val parse_document =
   6.220 -  (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
   6.221 -  |-- parse_element;
   6.222 -
   6.223 -fun parse s =
   6.224 -  (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
   6.225 -      (blanks |-- parse_document --| blanks))) (raw_explode s) of
   6.226 -    (x, []) => x
   6.227 -  | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
   6.228 -
   6.229 -end;
   6.230 -
   6.231 -
   6.232 -
   6.233 -(** XML as data representation language **)
   6.234 -
   6.235 -exception XML_ATOM of string;
   6.236 -exception XML_BODY of tree list;
   6.237 -
   6.238 -
   6.239 -structure Encode =
   6.240 -struct
   6.241 -
   6.242 -type 'a A = 'a -> string;
   6.243 -type 'a T = 'a -> body;
   6.244 -type 'a V = 'a -> string list * body;
   6.245 -
   6.246 -
   6.247 -(* atomic values *)
   6.248 -
   6.249 -fun int_atom i = signed_string_of_int i;
   6.250 -
   6.251 -fun bool_atom false = "0"
   6.252 -  | bool_atom true = "1";
   6.253 -
   6.254 -fun unit_atom () = "";
   6.255 -
   6.256 -
   6.257 -(* structural nodes *)
   6.258 -
   6.259 -fun node ts = Elem ((":", []), ts);
   6.260 -
   6.261 -fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
   6.262 -
   6.263 -fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
   6.264 -
   6.265 -
   6.266 -(* representation of standard types *)
   6.267 -
   6.268 -fun properties props = [Elem ((":", props), [])];
   6.269 -
   6.270 -fun string "" = []
   6.271 -  | string s = [Text s];
   6.272 -
   6.273 -val int = string o int_atom;
   6.274 -
   6.275 -val bool = string o bool_atom;
   6.276 -
   6.277 -val unit = string o unit_atom;
   6.278 -
   6.279 -fun pair f g (x, y) = [node (f x), node (g y)];
   6.280 -
   6.281 -fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
   6.282 -
   6.283 -fun list f xs = map (node o f) xs;
   6.284 -
   6.285 -fun option _ NONE = []
   6.286 -  | option f (SOME x) = [node (f x)];
   6.287 -
   6.288 -fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
   6.289 -
   6.290 -end;
   6.291 -
   6.292 -
   6.293 -structure Decode =
   6.294 -struct
   6.295 -
   6.296 -type 'a A = string -> 'a;
   6.297 -type 'a T = body -> 'a;
   6.298 -type 'a V = string list * body -> 'a;
   6.299 -
   6.300 -
   6.301 -(* atomic values *)
   6.302 -
   6.303 -fun int_atom s =
   6.304 -  Markup.parse_int s
   6.305 -    handle Fail _ => raise XML_ATOM s;
   6.306 -
   6.307 -fun bool_atom "0" = false
   6.308 -  | bool_atom "1" = true
   6.309 -  | bool_atom s = raise XML_ATOM s;
   6.310 -
   6.311 -fun unit_atom "" = ()
   6.312 -  | unit_atom s = raise XML_ATOM s;
   6.313 -
   6.314 -
   6.315 -(* structural nodes *)
   6.316 -
   6.317 -fun node (Elem ((":", []), ts)) = ts
   6.318 -  | node t = raise XML_BODY [t];
   6.319 -
   6.320 -fun vector atts =
   6.321 -  #1 (fold_map (fn (a, x) =>
   6.322 -        fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
   6.323 -
   6.324 -fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
   6.325 -  | tagged t = raise XML_BODY [t];
   6.326 -
   6.327 -
   6.328 -(* representation of standard types *)
   6.329 -
   6.330 -fun properties [Elem ((":", props), [])] = props
   6.331 -  | properties ts = raise XML_BODY ts;
   6.332 -
   6.333 -fun string [] = ""
   6.334 -  | string [Text s] = s
   6.335 -  | string ts = raise XML_BODY ts;
   6.336 -
   6.337 -val int = int_atom o string;
   6.338 -
   6.339 -val bool = bool_atom o string;
   6.340 -
   6.341 -val unit = unit_atom o string;
   6.342 -
   6.343 -fun pair f g [t1, t2] = (f (node t1), g (node t2))
   6.344 -  | pair _ _ ts = raise XML_BODY ts;
   6.345 -
   6.346 -fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
   6.347 -  | triple _ _ _ ts = raise XML_BODY ts;
   6.348 -
   6.349 -fun list f ts = map (f o node) ts;
   6.350 -
   6.351 -fun option _ [] = NONE
   6.352 -  | option f [t] = SOME (f (node t))
   6.353 -  | option _ ts = raise XML_BODY ts;
   6.354 -
   6.355 -fun variant fs [t] =
   6.356 -      let
   6.357 -        val (tag, (xs, ts)) = tagged t;
   6.358 -        val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
   6.359 -      in f (xs, ts) end
   6.360 -  | variant _ ts = raise XML_BODY ts;
   6.361 -
   6.362 -end;
   6.363 -
   6.364 -end;
     7.1 --- a/src/Pure/General/xml.scala	Sun Sep 04 10:29:38 2011 -0700
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,390 +0,0 @@
     7.4 -/*  Title:      Pure/General/xml.scala
     7.5 -    Author:     Makarius
     7.6 -
     7.7 -Untyped XML trees.
     7.8 -*/
     7.9 -
    7.10 -package isabelle
    7.11 -
    7.12 -import java.lang.System
    7.13 -import java.util.WeakHashMap
    7.14 -import java.lang.ref.WeakReference
    7.15 -import javax.xml.parsers.DocumentBuilderFactory
    7.16 -
    7.17 -import scala.actors.Actor._
    7.18 -import scala.collection.mutable
    7.19 -
    7.20 -
    7.21 -object XML
    7.22 -{
    7.23 -  /** XML trees **/
    7.24 -
    7.25 -  /* datatype representation */
    7.26 -
    7.27 -  type Attributes = Properties.T
    7.28 -
    7.29 -  sealed abstract class Tree { override def toString = string_of_tree(this) }
    7.30 -  case class Elem(markup: Markup, body: List[Tree]) extends Tree
    7.31 -  case class Text(content: String) extends Tree
    7.32 -
    7.33 -  def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
    7.34 -  def elem(name: String) = Elem(Markup(name, Nil), Nil)
    7.35 -
    7.36 -  type Body = List[Tree]
    7.37 -
    7.38 -
    7.39 -  /* string representation */
    7.40 -
    7.41 -  def string_of_body(body: Body): String =
    7.42 -  {
    7.43 -    val s = new StringBuilder
    7.44 -
    7.45 -    def text(txt: String) {
    7.46 -      if (txt == null) s ++= txt
    7.47 -      else {
    7.48 -        for (c <- txt.iterator) c match {
    7.49 -          case '<' => s ++= "&lt;"
    7.50 -          case '>' => s ++= "&gt;"
    7.51 -          case '&' => s ++= "&amp;"
    7.52 -          case '"' => s ++= "&quot;"
    7.53 -          case '\'' => s ++= "&apos;"
    7.54 -          case _ => s += c
    7.55 -        }
    7.56 -      }
    7.57 -    }
    7.58 -    def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
    7.59 -    def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
    7.60 -    def tree(t: Tree): Unit =
    7.61 -      t match {
    7.62 -        case Elem(markup, Nil) =>
    7.63 -          s ++= "<"; elem(markup); s ++= "/>"
    7.64 -        case Elem(markup, ts) =>
    7.65 -          s ++= "<"; elem(markup); s ++= ">"
    7.66 -          ts.foreach(tree)
    7.67 -          s ++= "</"; s ++= markup.name; s ++= ">"
    7.68 -        case Text(txt) => text(txt)
    7.69 -      }
    7.70 -    body.foreach(tree)
    7.71 -    s.toString
    7.72 -  }
    7.73 -
    7.74 -  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
    7.75 -
    7.76 -
    7.77 -  /* text content */
    7.78 -
    7.79 -  def content_stream(tree: Tree): Stream[String] =
    7.80 -    tree match {
    7.81 -      case Elem(_, body) => content_stream(body)
    7.82 -      case Text(content) => Stream(content)
    7.83 -    }
    7.84 -  def content_stream(body: Body): Stream[String] =
    7.85 -    body.toStream.flatten(content_stream(_))
    7.86 -
    7.87 -  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
    7.88 -  def content(body: Body): Iterator[String] = content_stream(body).iterator
    7.89 -
    7.90 -
    7.91 -  /* pipe-lined cache for partial sharing */
    7.92 -
    7.93 -  class Cache(initial_size: Int = 131071, max_string: Int = 100)
    7.94 -  {
    7.95 -    private val cache_actor = actor
    7.96 -    {
    7.97 -      val table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
    7.98 -
    7.99 -      def lookup[A](x: A): Option[A] =
   7.100 -      {
   7.101 -        val ref = table.get(x)
   7.102 -        if (ref == null) None
   7.103 -        else {
   7.104 -          val y = ref.asInstanceOf[WeakReference[A]].get
   7.105 -          if (y == null) None
   7.106 -          else Some(y)
   7.107 -        }
   7.108 -      }
   7.109 -      def store[A](x: A): A =
   7.110 -      {
   7.111 -        table.put(x, new WeakReference[Any](x))
   7.112 -        x
   7.113 -      }
   7.114 -
   7.115 -      def trim_bytes(s: String): String = new String(s.toCharArray)
   7.116 -
   7.117 -      def cache_string(x: String): String =
   7.118 -        lookup(x) match {
   7.119 -          case Some(y) => y
   7.120 -          case None =>
   7.121 -            val z = trim_bytes(x)
   7.122 -            if (z.length > max_string) z else store(z)
   7.123 -        }
   7.124 -      def cache_props(x: Properties.T): Properties.T =
   7.125 -        if (x.isEmpty) x
   7.126 -        else
   7.127 -          lookup(x) match {
   7.128 -            case Some(y) => y
   7.129 -            case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
   7.130 -          }
   7.131 -      def cache_markup(x: Markup): Markup =
   7.132 -        lookup(x) match {
   7.133 -          case Some(y) => y
   7.134 -          case None =>
   7.135 -            x match {
   7.136 -              case Markup(name, props) =>
   7.137 -                store(Markup(cache_string(name), cache_props(props)))
   7.138 -            }
   7.139 -        }
   7.140 -      def cache_tree(x: XML.Tree): XML.Tree =
   7.141 -        lookup(x) match {
   7.142 -          case Some(y) => y
   7.143 -          case None =>
   7.144 -            x match {
   7.145 -              case XML.Elem(markup, body) =>
   7.146 -                store(XML.Elem(cache_markup(markup), cache_body(body)))
   7.147 -              case XML.Text(text) => store(XML.Text(cache_string(text)))
   7.148 -            }
   7.149 -        }
   7.150 -      def cache_body(x: XML.Body): XML.Body =
   7.151 -        if (x.isEmpty) x
   7.152 -        else
   7.153 -          lookup(x) match {
   7.154 -            case Some(y) => y
   7.155 -            case None => x.map(cache_tree(_))
   7.156 -          }
   7.157 -
   7.158 -      // main loop
   7.159 -      loop {
   7.160 -        react {
   7.161 -          case Cache_String(x, f) => f(cache_string(x))
   7.162 -          case Cache_Markup(x, f) => f(cache_markup(x))
   7.163 -          case Cache_Tree(x, f) => f(cache_tree(x))
   7.164 -          case Cache_Body(x, f) => f(cache_body(x))
   7.165 -          case Cache_Ignore(x, f) => f(x)
   7.166 -          case bad => System.err.println("XML.cache_actor: ignoring bad input " + bad)
   7.167 -        }
   7.168 -      }
   7.169 -    }
   7.170 -
   7.171 -    private case class Cache_String(x: String, f: String => Unit)
   7.172 -    private case class Cache_Markup(x: Markup, f: Markup => Unit)
   7.173 -    private case class Cache_Tree(x: XML.Tree, f: XML.Tree => Unit)
   7.174 -    private case class Cache_Body(x: XML.Body, f: XML.Body => Unit)
   7.175 -    private case class Cache_Ignore[A](x: A, f: A => Unit)
   7.176 -
   7.177 -    // main methods
   7.178 -    def cache_string(x: String)(f: String => Unit) { cache_actor ! Cache_String(x, f) }
   7.179 -    def cache_markup(x: Markup)(f: Markup => Unit) { cache_actor ! Cache_Markup(x, f) }
   7.180 -    def cache_tree(x: XML.Tree)(f: XML.Tree => Unit) { cache_actor ! Cache_Tree(x, f) }
   7.181 -    def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) }
   7.182 -    def cache_ignore[A](x: A)(f: A => Unit) { cache_actor ! Cache_Ignore(x, f) }
   7.183 -  }
   7.184 -
   7.185 -
   7.186 -
   7.187 -  /** document object model (W3C DOM) **/
   7.188 -
   7.189 -  def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
   7.190 -    node.getUserData(Markup.Data.name) match {
   7.191 -      case tree: XML.Tree => Some(tree)
   7.192 -      case _ => None
   7.193 -    }
   7.194 -
   7.195 -  def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
   7.196 -  {
   7.197 -    def DOM(tr: Tree): org.w3c.dom.Node = tr match {
   7.198 -      case Elem(Markup.Data, List(data, t)) =>
   7.199 -        val node = DOM(t)
   7.200 -        node.setUserData(Markup.Data.name, data, null)
   7.201 -        node
   7.202 -      case Elem(Markup(name, atts), ts) =>
   7.203 -        if (name == Markup.Data.name)
   7.204 -          error("Malformed data element: " + tr.toString)
   7.205 -        val node = doc.createElement(name)
   7.206 -        for ((name, value) <- atts) node.setAttribute(name, value)
   7.207 -        for (t <- ts) node.appendChild(DOM(t))
   7.208 -        node
   7.209 -      case Text(txt) => doc.createTextNode(txt)
   7.210 -    }
   7.211 -    DOM(tree)
   7.212 -  }
   7.213 -
   7.214 -
   7.215 -
   7.216 -  /** XML as data representation language **/
   7.217 -
   7.218 -  class XML_Atom(s: String) extends Exception(s)
   7.219 -  class XML_Body(body: XML.Body) extends Exception
   7.220 -
   7.221 -  object Encode
   7.222 -  {
   7.223 -    type T[A] = A => XML.Body
   7.224 -
   7.225 -
   7.226 -    /* atomic values */
   7.227 -
   7.228 -    def long_atom(i: Long): String = i.toString
   7.229 -
   7.230 -    def int_atom(i: Int): String = i.toString
   7.231 -
   7.232 -    def bool_atom(b: Boolean): String = if (b) "1" else "0"
   7.233 -
   7.234 -    def unit_atom(u: Unit) = ""
   7.235 -
   7.236 -
   7.237 -    /* structural nodes */
   7.238 -
   7.239 -    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
   7.240 -
   7.241 -    private def vector(xs: List[String]): XML.Attributes =
   7.242 -      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
   7.243 -
   7.244 -    private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
   7.245 -      XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
   7.246 -
   7.247 -
   7.248 -    /* representation of standard types */
   7.249 -
   7.250 -    val properties: T[Properties.T] =
   7.251 -      (props => List(XML.Elem(Markup(":", props), Nil)))
   7.252 -
   7.253 -    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
   7.254 -
   7.255 -    val long: T[Long] = (x => string(long_atom(x)))
   7.256 -
   7.257 -    val int: T[Int] = (x => string(int_atom(x)))
   7.258 -
   7.259 -    val bool: T[Boolean] = (x => string(bool_atom(x)))
   7.260 -
   7.261 -    val unit: T[Unit] = (x => string(unit_atom(x)))
   7.262 -
   7.263 -    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   7.264 -      (x => List(node(f(x._1)), node(g(x._2))))
   7.265 -
   7.266 -    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   7.267 -      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
   7.268 -
   7.269 -    def list[A](f: T[A]): T[List[A]] =
   7.270 -      (xs => xs.map((x: A) => node(f(x))))
   7.271 -
   7.272 -    def option[A](f: T[A]): T[Option[A]] =
   7.273 -    {
   7.274 -      case None => Nil
   7.275 -      case Some(x) => List(node(f(x)))
   7.276 -    }
   7.277 -
   7.278 -    def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
   7.279 -    {
   7.280 -      case x =>
   7.281 -        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
   7.282 -        List(tagged(tag, f(x)))
   7.283 -    }
   7.284 -  }
   7.285 -
   7.286 -  object Decode
   7.287 -  {
   7.288 -    type T[A] = XML.Body => A
   7.289 -    type V[A] = (List[String], XML.Body) => A
   7.290 -
   7.291 -
   7.292 -    /* atomic values */
   7.293 -
   7.294 -    def long_atom(s: String): Long =
   7.295 -      try { java.lang.Long.parseLong(s) }
   7.296 -      catch { case e: NumberFormatException => throw new XML_Atom(s) }
   7.297 -
   7.298 -    def int_atom(s: String): Int =
   7.299 -      try { Integer.parseInt(s) }
   7.300 -      catch { case e: NumberFormatException => throw new XML_Atom(s) }
   7.301 -
   7.302 -    def bool_atom(s: String): Boolean =
   7.303 -      if (s == "1") true
   7.304 -      else if (s == "0") false
   7.305 -      else throw new XML_Atom(s)
   7.306 -
   7.307 -    def unit_atom(s: String): Unit =
   7.308 -      if (s == "") () else throw new XML_Atom(s)
   7.309 -
   7.310 -
   7.311 -    /* structural nodes */
   7.312 -
   7.313 -    private def node(t: XML.Tree): XML.Body =
   7.314 -      t match {
   7.315 -        case XML.Elem(Markup(":", Nil), ts) => ts
   7.316 -        case _ => throw new XML_Body(List(t))
   7.317 -      }
   7.318 -
   7.319 -    private def vector(atts: XML.Attributes): List[String] =
   7.320 -    {
   7.321 -      val xs = new mutable.ListBuffer[String]
   7.322 -      var i = 0
   7.323 -      for ((a, x) <- atts) {
   7.324 -        if (int_atom(a) == i) { xs += x; i = i + 1 }
   7.325 -        else throw new XML_Atom(a)
   7.326 -      }
   7.327 -      xs.toList
   7.328 -    }
   7.329 -
   7.330 -    private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
   7.331 -      t match {
   7.332 -        case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
   7.333 -        case _ => throw new XML_Body(List(t))
   7.334 -      }
   7.335 -
   7.336 -
   7.337 -    /* representation of standard types */
   7.338 -
   7.339 -    val properties: T[Properties.T] =
   7.340 -    {
   7.341 -      case List(XML.Elem(Markup(":", props), Nil)) => props
   7.342 -      case ts => throw new XML_Body(ts)
   7.343 -    }
   7.344 -
   7.345 -    val string: T[String] =
   7.346 -    {
   7.347 -      case Nil => ""
   7.348 -      case List(XML.Text(s)) => s
   7.349 -      case ts => throw new XML_Body(ts)
   7.350 -    }
   7.351 -
   7.352 -    val long: T[Long] = (x => long_atom(string(x)))
   7.353 -
   7.354 -    val int: T[Int] = (x => int_atom(string(x)))
   7.355 -
   7.356 -    val bool: T[Boolean] = (x => bool_atom(string(x)))
   7.357 -
   7.358 -    val unit: T[Unit] = (x => unit_atom(string(x)))
   7.359 -
   7.360 -    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   7.361 -    {
   7.362 -      case List(t1, t2) => (f(node(t1)), g(node(t2)))
   7.363 -      case ts => throw new XML_Body(ts)
   7.364 -    }
   7.365 -
   7.366 -    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   7.367 -    {
   7.368 -      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
   7.369 -      case ts => throw new XML_Body(ts)
   7.370 -    }
   7.371 -
   7.372 -    def list[A](f: T[A]): T[List[A]] =
   7.373 -      (ts => ts.map(t => f(node(t))))
   7.374 -
   7.375 -    def option[A](f: T[A]): T[Option[A]] =
   7.376 -    {
   7.377 -      case Nil => None
   7.378 -      case List(t) => Some(f(node(t)))
   7.379 -      case ts => throw new XML_Body(ts)
   7.380 -    }
   7.381 -
   7.382 -    def variant[A](fs: List[V[A]]): T[A] =
   7.383 -    {
   7.384 -      case List(t) =>
   7.385 -        val (tag, (xs, ts)) = tagged(t)
   7.386 -        val f =
   7.387 -          try { fs(tag) }
   7.388 -          catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
   7.389 -        f(xs, ts)
   7.390 -      case ts => throw new XML_Body(ts)
   7.391 -    }
   7.392 -  }
   7.393 -}
     8.1 --- a/src/Pure/General/yxml.ML	Sun Sep 04 10:29:38 2011 -0700
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,147 +0,0 @@
     8.4 -(*  Title:      Pure/General/yxml.ML
     8.5 -    Author:     Makarius
     8.6 -
     8.7 -Efficient text representation of XML trees using extra characters X
     8.8 -and Y -- no escaping, may nest marked text verbatim.
     8.9 -
    8.10 -Markup <elem att="val" ...>...body...</elem> is encoded as:
    8.11 -
    8.12 -  X Y name Y att=val ... X
    8.13 -  ...
    8.14 -  body
    8.15 -  ...
    8.16 -  X Y X
    8.17 -*)
    8.18 -
    8.19 -signature YXML =
    8.20 -sig
    8.21 -  val X: Symbol.symbol
    8.22 -  val Y: Symbol.symbol
    8.23 -  val embed_controls: string -> string
    8.24 -  val detect: string -> bool
    8.25 -  val output_markup: Markup.T -> string * string
    8.26 -  val element: string -> XML.attributes -> string list -> string
    8.27 -  val string_of_body: XML.body -> string
    8.28 -  val string_of: XML.tree -> string
    8.29 -  val parse_body: string -> XML.body
    8.30 -  val parse: string -> XML.tree
    8.31 -end;
    8.32 -
    8.33 -structure YXML: YXML =
    8.34 -struct
    8.35 -
    8.36 -(** string representation **)
    8.37 -
    8.38 -(* idempotent recoding of certain low ASCII control characters *)
    8.39 -
    8.40 -fun pseudo_utf8 c =
    8.41 -  if Symbol.is_ascii_control c
    8.42 -  then chr 192 ^ chr (128 + ord c)
    8.43 -  else c;
    8.44 -
    8.45 -fun embed_controls str =
    8.46 -  if exists_string Symbol.is_ascii_control str
    8.47 -  then translate_string pseudo_utf8 str
    8.48 -  else str;
    8.49 -
    8.50 -
    8.51 -(* markers *)
    8.52 -
    8.53 -val X = chr 5;
    8.54 -val Y = chr 6;
    8.55 -val XY = X ^ Y;
    8.56 -val XYX = XY ^ X;
    8.57 -
    8.58 -val detect = exists_string (fn s => s = X orelse s = Y);
    8.59 -
    8.60 -
    8.61 -(* output *)
    8.62 -
    8.63 -fun output_markup (markup as (name, atts)) =
    8.64 -  if Markup.is_empty markup then Markup.no_output
    8.65 -  else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
    8.66 -
    8.67 -fun element name atts body =
    8.68 -  let val (pre, post) = output_markup (name, atts)
    8.69 -  in pre ^ implode body ^ post end;
    8.70 -
    8.71 -fun string_of_body body =
    8.72 -  let
    8.73 -    fun attrib (a, x) =
    8.74 -      Buffer.add Y #>
    8.75 -      Buffer.add a #> Buffer.add "=" #> Buffer.add x;
    8.76 -    fun tree (XML.Elem ((name, atts), ts)) =
    8.77 -          Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
    8.78 -          trees ts #>
    8.79 -          Buffer.add XYX
    8.80 -      | tree (XML.Text s) = Buffer.add s
    8.81 -    and trees ts = fold tree ts;
    8.82 -  in Buffer.empty |> trees body |> Buffer.content end;
    8.83 -
    8.84 -val string_of = string_of_body o single;
    8.85 -
    8.86 -
    8.87 -
    8.88 -(** efficient YXML parsing **)
    8.89 -
    8.90 -local
    8.91 -
    8.92 -(* splitting *)
    8.93 -
    8.94 -fun is_char s c = ord s = Char.ord c;
    8.95 -
    8.96 -val split_string =
    8.97 -  Substring.full #>
    8.98 -  Substring.tokens (is_char X) #>
    8.99 -  map (Substring.fields (is_char Y) #> map Substring.string);
   8.100 -
   8.101 -
   8.102 -(* structural errors *)
   8.103 -
   8.104 -fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
   8.105 -fun err_attribute () = err "bad attribute";
   8.106 -fun err_element () = err "bad element";
   8.107 -fun err_unbalanced "" = err "unbalanced element"
   8.108 -  | err_unbalanced name = err ("unbalanced element " ^ quote name);
   8.109 -
   8.110 -
   8.111 -(* stack operations *)
   8.112 -
   8.113 -fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
   8.114 -
   8.115 -fun push "" _ _ = err_element ()
   8.116 -  | push name atts pending = ((name, atts), []) :: pending;
   8.117 -
   8.118 -fun pop ((("", _), _) :: _) = err_unbalanced ""
   8.119 -  | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
   8.120 -
   8.121 -
   8.122 -(* parsing *)
   8.123 -
   8.124 -fun parse_attrib s =
   8.125 -  (case first_field "=" s of
   8.126 -    NONE => err_attribute ()
   8.127 -  | SOME ("", _) => err_attribute ()
   8.128 -  | SOME att => att);
   8.129 -
   8.130 -fun parse_chunk ["", ""] = pop
   8.131 -  | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
   8.132 -  | parse_chunk txts = fold (add o XML.Text) txts;
   8.133 -
   8.134 -in
   8.135 -
   8.136 -fun parse_body source =
   8.137 -  (case fold parse_chunk (split_string source) [(("", []), [])] of
   8.138 -    [(("", _), result)] => rev result
   8.139 -  | ((name, _), _) :: _ => err_unbalanced name);
   8.140 -
   8.141 -fun parse source =
   8.142 -  (case parse_body source of
   8.143 -    [result] => result
   8.144 -  | [] => XML.Text ""
   8.145 -  | _ => err "multiple results");
   8.146 -
   8.147 -end;
   8.148 -
   8.149 -end;
   8.150 -
     9.1 --- a/src/Pure/General/yxml.scala	Sun Sep 04 10:29:38 2011 -0700
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,134 +0,0 @@
     9.4 -/*  Title:      Pure/General/yxml.scala
     9.5 -    Author:     Makarius
     9.6 -
     9.7 -Efficient text representation of XML trees.
     9.8 -*/
     9.9 -
    9.10 -package isabelle
    9.11 -
    9.12 -
    9.13 -import scala.collection.mutable
    9.14 -
    9.15 -
    9.16 -object YXML
    9.17 -{
    9.18 -  /* chunk markers */
    9.19 -
    9.20 -  val X = '\5'
    9.21 -  val Y = '\6'
    9.22 -  val X_string = X.toString
    9.23 -  val Y_string = Y.toString
    9.24 -
    9.25 -  def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
    9.26 -
    9.27 -
    9.28 -  /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
    9.29 -
    9.30 -  def string_of_body(body: XML.Body): String =
    9.31 -  {
    9.32 -    val s = new StringBuilder
    9.33 -    def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
    9.34 -    def tree(t: XML.Tree): Unit =
    9.35 -      t match {
    9.36 -        case XML.Elem(Markup(name, atts), ts) =>
    9.37 -          s += X; s += Y; s++= name; atts.foreach(attrib); s += X
    9.38 -          ts.foreach(tree)
    9.39 -          s += X; s += Y; s += X
    9.40 -        case XML.Text(text) => s ++= text
    9.41 -      }
    9.42 -    body.foreach(tree)
    9.43 -    s.toString
    9.44 -  }
    9.45 -
    9.46 -  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
    9.47 -
    9.48 -
    9.49 -  /* parsing */
    9.50 -
    9.51 -  private def err(msg: String) = error("Malformed YXML: " + msg)
    9.52 -  private def err_attribute() = err("bad attribute")
    9.53 -  private def err_element() = err("bad element")
    9.54 -  private def err_unbalanced(name: String) =
    9.55 -    if (name == "") err("unbalanced element")
    9.56 -    else err("unbalanced element " + quote(name))
    9.57 -
    9.58 -  private def parse_attrib(source: CharSequence) = {
    9.59 -    val s = source.toString
    9.60 -    val i = s.indexOf('=')
    9.61 -    if (i <= 0) err_attribute()
    9.62 -    (s.substring(0, i), s.substring(i + 1))
    9.63 -  }
    9.64 -
    9.65 -
    9.66 -  def parse_body(source: CharSequence): XML.Body =
    9.67 -  {
    9.68 -    /* stack operations */
    9.69 -
    9.70 -    def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
    9.71 -    var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
    9.72 -
    9.73 -    def add(x: XML.Tree)
    9.74 -    {
    9.75 -      (stack: @unchecked) match { case ((_, body) :: _) => body += x }
    9.76 -    }
    9.77 -
    9.78 -    def push(name: String, atts: XML.Attributes)
    9.79 -    {
    9.80 -      if (name == "") err_element()
    9.81 -      else stack = (Markup(name, atts), buffer()) :: stack
    9.82 -    }
    9.83 -
    9.84 -    def pop()
    9.85 -    {
    9.86 -      (stack: @unchecked) match {
    9.87 -        case ((Markup.Empty, _) :: _) => err_unbalanced("")
    9.88 -        case ((markup, body) :: pending) =>
    9.89 -          stack = pending
    9.90 -          add(XML.Elem(markup, body.toList))
    9.91 -      }
    9.92 -    }
    9.93 -
    9.94 -
    9.95 -    /* parse chunks */
    9.96 -
    9.97 -    for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
    9.98 -      if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
    9.99 -      else {
   9.100 -        Library.chunks(chunk, Y).toList match {
   9.101 -          case ch :: name :: atts if ch.length == 0 =>
   9.102 -            push(name.toString, atts.map(parse_attrib))
   9.103 -          case txts => for (txt <- txts) add(XML.Text(txt.toString))
   9.104 -        }
   9.105 -      }
   9.106 -    }
   9.107 -    (stack: @unchecked) match {
   9.108 -      case List((Markup.Empty, body)) => body.toList
   9.109 -      case (Markup(name, _), _) :: _ => err_unbalanced(name)
   9.110 -    }
   9.111 -  }
   9.112 -
   9.113 -  def parse(source: CharSequence): XML.Tree =
   9.114 -    parse_body(source) match {
   9.115 -      case List(result) => result
   9.116 -      case Nil => XML.Text("")
   9.117 -      case _ => err("multiple results")
   9.118 -    }
   9.119 -
   9.120 -
   9.121 -  /* failsafe parsing */
   9.122 -
   9.123 -  private def markup_malformed(source: CharSequence) =
   9.124 -    XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
   9.125 -
   9.126 -  def parse_body_failsafe(source: CharSequence): XML.Body =
   9.127 -  {
   9.128 -    try { parse_body(source) }
   9.129 -    catch { case ERROR(_) => List(markup_malformed(source)) }
   9.130 -  }
   9.131 -
   9.132 -  def parse_failsafe(source: CharSequence): XML.Tree =
   9.133 -  {
   9.134 -    try { parse(source) }
   9.135 -    catch { case ERROR(_) => markup_malformed(source) }
   9.136 -  }
   9.137 -}
    10.1 --- a/src/Pure/IsaMakefile	Sun Sep 04 10:29:38 2011 -0700
    10.2 +++ b/src/Pure/IsaMakefile	Sun Sep 04 20:37:20 2011 +0200
    10.3 @@ -105,8 +105,6 @@
    10.4    General/table.ML					\
    10.5    General/timing.ML					\
    10.6    General/url.ML					\
    10.7 -  General/xml.ML					\
    10.8 -  General/yxml.ML					\
    10.9    Isar/args.ML						\
   10.10    Isar/attrib.ML					\
   10.11    Isar/auto_bind.ML					\
   10.12 @@ -158,6 +156,8 @@
   10.13    ML/ml_thms.ML						\
   10.14    PIDE/document.ML					\
   10.15    PIDE/isar_document.ML					\
   10.16 +  PIDE/xml.ML						\
   10.17 +  PIDE/yxml.ML						\
   10.18    Proof/extraction.ML					\
   10.19    Proof/proof_checker.ML				\
   10.20    Proof/proof_rewrite_rules.ML				\
    11.1 --- a/src/Pure/ML/ml_lex.ML	Sun Sep 04 10:29:38 2011 -0700
    11.2 +++ b/src/Pure/ML/ml_lex.ML	Sun Sep 04 20:37:20 2011 +0200
    11.3 @@ -106,8 +106,8 @@
    11.4  
    11.5  val token_kind_markup =
    11.6   fn Keyword   => Markup.ML_keyword
    11.7 -  | Ident     => Markup.ML_ident
    11.8 -  | LongIdent => Markup.ML_ident
    11.9 +  | Ident     => Markup.empty
   11.10 +  | LongIdent => Markup.empty
   11.11    | TypeVar   => Markup.ML_tvar
   11.12    | Word      => Markup.ML_numeral
   11.13    | Int       => Markup.ML_numeral
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Pure/PIDE/xml.ML	Sun Sep 04 20:37:20 2011 +0200
    12.3 @@ -0,0 +1,363 @@
    12.4 +(*  Title:      Pure/PIDE/xml.ML
    12.5 +    Author:     David Aspinall
    12.6 +    Author:     Stefan Berghofer
    12.7 +    Author:     Makarius
    12.8 +
    12.9 +Untyped XML trees and basic data representation.
   12.10 +*)
   12.11 +
   12.12 +signature XML_DATA_OPS =
   12.13 +sig
   12.14 +  type 'a A
   12.15 +  type 'a T
   12.16 +  type 'a V
   12.17 +  val int_atom: int A
   12.18 +  val bool_atom: bool A
   12.19 +  val unit_atom: unit A
   12.20 +  val properties: Properties.T T
   12.21 +  val string: string T
   12.22 +  val int: int T
   12.23 +  val bool: bool T
   12.24 +  val unit: unit T
   12.25 +  val pair: 'a T -> 'b T -> ('a * 'b) T
   12.26 +  val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
   12.27 +  val list: 'a T -> 'a list T
   12.28 +  val option: 'a T -> 'a option T
   12.29 +  val variant: 'a V list -> 'a T
   12.30 +end;
   12.31 +
   12.32 +signature XML =
   12.33 +sig
   12.34 +  type attributes = Properties.T
   12.35 +  datatype tree =
   12.36 +      Elem of Markup.T * tree list
   12.37 +    | Text of string
   12.38 +  type body = tree list
   12.39 +  val add_content: tree -> Buffer.T -> Buffer.T
   12.40 +  val content_of: body -> string
   12.41 +  val header: string
   12.42 +  val text: string -> string
   12.43 +  val element: string -> attributes -> string list -> string
   12.44 +  val output_markup: Markup.T -> Output.output * Output.output
   12.45 +  val string_of: tree -> string
   12.46 +  val pretty: int -> tree -> Pretty.T
   12.47 +  val output: tree -> TextIO.outstream -> unit
   12.48 +  val parse_comments: string list -> unit * string list
   12.49 +  val parse_string : string -> string option
   12.50 +  val parse_element: string list -> tree * string list
   12.51 +  val parse_document: string list -> tree * string list
   12.52 +  val parse: string -> tree
   12.53 +  exception XML_ATOM of string
   12.54 +  exception XML_BODY of body
   12.55 +  structure Encode: XML_DATA_OPS
   12.56 +  structure Decode: XML_DATA_OPS
   12.57 +end;
   12.58 +
   12.59 +structure XML: XML =
   12.60 +struct
   12.61 +
   12.62 +(** XML trees **)
   12.63 +
   12.64 +type attributes = Properties.T;
   12.65 +
   12.66 +datatype tree =
   12.67 +    Elem of Markup.T * tree list
   12.68 +  | Text of string;
   12.69 +
   12.70 +type body = tree list;
   12.71 +
   12.72 +fun add_content (Elem (_, ts)) = fold add_content ts
   12.73 +  | add_content (Text s) = Buffer.add s;
   12.74 +
   12.75 +fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
   12.76 +
   12.77 +
   12.78 +
   12.79 +(** string representation **)
   12.80 +
   12.81 +val header = "<?xml version=\"1.0\"?>\n";
   12.82 +
   12.83 +
   12.84 +(* escaped text *)
   12.85 +
   12.86 +fun decode "&lt;" = "<"
   12.87 +  | decode "&gt;" = ">"
   12.88 +  | decode "&amp;" = "&"
   12.89 +  | decode "&apos;" = "'"
   12.90 +  | decode "&quot;" = "\""
   12.91 +  | decode c = c;
   12.92 +
   12.93 +fun encode "<" = "&lt;"
   12.94 +  | encode ">" = "&gt;"
   12.95 +  | encode "&" = "&amp;"
   12.96 +  | encode "'" = "&apos;"
   12.97 +  | encode "\"" = "&quot;"
   12.98 +  | encode c = c;
   12.99 +
  12.100 +val text = translate_string encode;
  12.101 +
  12.102 +
  12.103 +(* elements *)
  12.104 +
  12.105 +fun elem name atts =
  12.106 +  space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
  12.107 +
  12.108 +fun element name atts body =
  12.109 +  let val b = implode body in
  12.110 +    if b = "" then enclose "<" "/>" (elem name atts)
  12.111 +    else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
  12.112 +  end;
  12.113 +
  12.114 +fun output_markup (markup as (name, atts)) =
  12.115 +  if Markup.is_empty markup then Markup.no_output
  12.116 +  else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
  12.117 +
  12.118 +
  12.119 +(* output *)
  12.120 +
  12.121 +fun buffer_of depth tree =
  12.122 +  let
  12.123 +    fun traverse _ (Elem ((name, atts), [])) =
  12.124 +          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
  12.125 +      | traverse d (Elem ((name, atts), ts)) =
  12.126 +          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
  12.127 +          traverse_body d ts #>
  12.128 +          Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
  12.129 +      | traverse _ (Text s) = Buffer.add (text s)
  12.130 +    and traverse_body 0 _ = Buffer.add "..."
  12.131 +      | traverse_body d ts = fold (traverse (d - 1)) ts;
  12.132 +  in Buffer.empty |> traverse depth tree end;
  12.133 +
  12.134 +val string_of = Buffer.content o buffer_of ~1;
  12.135 +val output = Buffer.output o buffer_of ~1;
  12.136 +
  12.137 +fun pretty depth tree =
  12.138 +  Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
  12.139 +
  12.140 +
  12.141 +
  12.142 +(** XML parsing **)
  12.143 +
  12.144 +local
  12.145 +
  12.146 +fun err msg (xs, _) =
  12.147 +  fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
  12.148 +
  12.149 +fun ignored _ = [];
  12.150 +
  12.151 +val blanks = Scan.many Symbol.is_blank;
  12.152 +val special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
  12.153 +val regular = Scan.one Symbol.is_regular;
  12.154 +fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
  12.155 +
  12.156 +val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
  12.157 +
  12.158 +val parse_cdata =
  12.159 +  Scan.this_string "<![CDATA[" |--
  12.160 +  (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
  12.161 +  Scan.this_string "]]>";
  12.162 +
  12.163 +val parse_att =
  12.164 +  (Symbol.scan_id --| (blanks -- $$ "=" -- blanks)) --
  12.165 +  (($$ "\"" || $$ "'") :|-- (fn s =>
  12.166 +    (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
  12.167 +
  12.168 +val parse_comment =
  12.169 +  Scan.this_string "<!--" --
  12.170 +  Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
  12.171 +  Scan.this_string "-->" >> ignored;
  12.172 +
  12.173 +val parse_processing_instruction =
  12.174 +  Scan.this_string "<?" --
  12.175 +  Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
  12.176 +  Scan.this_string "?>" >> ignored;
  12.177 +
  12.178 +val parse_doctype =
  12.179 +  Scan.this_string "<!DOCTYPE" --
  12.180 +  Scan.repeat (Scan.unless ($$ ">") regular) --
  12.181 +  $$ ">" >> ignored;
  12.182 +
  12.183 +val parse_misc =
  12.184 +  Scan.one Symbol.is_blank >> ignored ||
  12.185 +  parse_processing_instruction ||
  12.186 +  parse_comment;
  12.187 +
  12.188 +val parse_optional_text =
  12.189 +  Scan.optional (parse_chars >> (single o Text)) [];
  12.190 +
  12.191 +fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
  12.192 +fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
  12.193 +val parse_name = Scan.one name_start_char ::: Scan.many name_char;
  12.194 +
  12.195 +in
  12.196 +
  12.197 +val parse_comments =
  12.198 +  blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
  12.199 +
  12.200 +val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
  12.201 +
  12.202 +fun parse_content xs =
  12.203 +  (parse_optional_text @@@
  12.204 +    (Scan.repeat
  12.205 +      ((parse_element >> single ||
  12.206 +        parse_cdata >> (single o Text) ||
  12.207 +        parse_processing_instruction ||
  12.208 +        parse_comment)
  12.209 +      @@@ parse_optional_text) >> flat)) xs
  12.210 +
  12.211 +and parse_element xs =
  12.212 +  ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
  12.213 +    (fn (name, _) =>
  12.214 +      !! (err (fn () => "Expected > or />"))
  12.215 +       ($$ "/" -- $$ ">" >> ignored ||
  12.216 +        $$ ">" |-- parse_content --|
  12.217 +          !! (err (fn () => "Expected </" ^ implode name ^ ">"))
  12.218 +              ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
  12.219 +    >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
  12.220 +
  12.221 +val parse_document =
  12.222 +  (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
  12.223 +  |-- parse_element;
  12.224 +
  12.225 +fun parse s =
  12.226 +  (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
  12.227 +      (blanks |-- parse_document --| blanks))) (raw_explode s) of
  12.228 +    (x, []) => x
  12.229 +  | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
  12.230 +
  12.231 +end;
  12.232 +
  12.233 +
  12.234 +
  12.235 +(** XML as data representation language **)
  12.236 +
  12.237 +exception XML_ATOM of string;
  12.238 +exception XML_BODY of tree list;
  12.239 +
  12.240 +
  12.241 +structure Encode =
  12.242 +struct
  12.243 +
  12.244 +type 'a A = 'a -> string;
  12.245 +type 'a T = 'a -> body;
  12.246 +type 'a V = 'a -> string list * body;
  12.247 +
  12.248 +
  12.249 +(* atomic values *)
  12.250 +
  12.251 +fun int_atom i = signed_string_of_int i;
  12.252 +
  12.253 +fun bool_atom false = "0"
  12.254 +  | bool_atom true = "1";
  12.255 +
  12.256 +fun unit_atom () = "";
  12.257 +
  12.258 +
  12.259 +(* structural nodes *)
  12.260 +
  12.261 +fun node ts = Elem ((":", []), ts);
  12.262 +
  12.263 +fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
  12.264 +
  12.265 +fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
  12.266 +
  12.267 +
  12.268 +(* representation of standard types *)
  12.269 +
  12.270 +fun properties props = [Elem ((":", props), [])];
  12.271 +
  12.272 +fun string "" = []
  12.273 +  | string s = [Text s];
  12.274 +
  12.275 +val int = string o int_atom;
  12.276 +
  12.277 +val bool = string o bool_atom;
  12.278 +
  12.279 +val unit = string o unit_atom;
  12.280 +
  12.281 +fun pair f g (x, y) = [node (f x), node (g y)];
  12.282 +
  12.283 +fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
  12.284 +
  12.285 +fun list f xs = map (node o f) xs;
  12.286 +
  12.287 +fun option _ NONE = []
  12.288 +  | option f (SOME x) = [node (f x)];
  12.289 +
  12.290 +fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
  12.291 +
  12.292 +end;
  12.293 +
  12.294 +
  12.295 +structure Decode =
  12.296 +struct
  12.297 +
  12.298 +type 'a A = string -> 'a;
  12.299 +type 'a T = body -> 'a;
  12.300 +type 'a V = string list * body -> 'a;
  12.301 +
  12.302 +
  12.303 +(* atomic values *)
  12.304 +
  12.305 +fun int_atom s =
  12.306 +  Markup.parse_int s
  12.307 +    handle Fail _ => raise XML_ATOM s;
  12.308 +
  12.309 +fun bool_atom "0" = false
  12.310 +  | bool_atom "1" = true
  12.311 +  | bool_atom s = raise XML_ATOM s;
  12.312 +
  12.313 +fun unit_atom "" = ()
  12.314 +  | unit_atom s = raise XML_ATOM s;
  12.315 +
  12.316 +
  12.317 +(* structural nodes *)
  12.318 +
  12.319 +fun node (Elem ((":", []), ts)) = ts
  12.320 +  | node t = raise XML_BODY [t];
  12.321 +
  12.322 +fun vector atts =
  12.323 +  #1 (fold_map (fn (a, x) =>
  12.324 +        fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
  12.325 +
  12.326 +fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
  12.327 +  | tagged t = raise XML_BODY [t];
  12.328 +
  12.329 +
  12.330 +(* representation of standard types *)
  12.331 +
  12.332 +fun properties [Elem ((":", props), [])] = props
  12.333 +  | properties ts = raise XML_BODY ts;
  12.334 +
  12.335 +fun string [] = ""
  12.336 +  | string [Text s] = s
  12.337 +  | string ts = raise XML_BODY ts;
  12.338 +
  12.339 +val int = int_atom o string;
  12.340 +
  12.341 +val bool = bool_atom o string;
  12.342 +
  12.343 +val unit = unit_atom o string;
  12.344 +
  12.345 +fun pair f g [t1, t2] = (f (node t1), g (node t2))
  12.346 +  | pair _ _ ts = raise XML_BODY ts;
  12.347 +
  12.348 +fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
  12.349 +  | triple _ _ _ ts = raise XML_BODY ts;
  12.350 +
  12.351 +fun list f ts = map (f o node) ts;
  12.352 +
  12.353 +fun option _ [] = NONE
  12.354 +  | option f [t] = SOME (f (node t))
  12.355 +  | option _ ts = raise XML_BODY ts;
  12.356 +
  12.357 +fun variant fs [t] =
  12.358 +      let
  12.359 +        val (tag, (xs, ts)) = tagged t;
  12.360 +        val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
  12.361 +      in f (xs, ts) end
  12.362 +  | variant _ ts = raise XML_BODY ts;
  12.363 +
  12.364 +end;
  12.365 +
  12.366 +end;
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Pure/PIDE/xml.scala	Sun Sep 04 20:37:20 2011 +0200
    13.3 @@ -0,0 +1,368 @@
    13.4 +/*  Title:      Pure/PIDE/xml.scala
    13.5 +    Author:     Makarius
    13.6 +
    13.7 +Untyped XML trees and basic data representation.
    13.8 +*/
    13.9 +
   13.10 +package isabelle
   13.11 +
   13.12 +import java.lang.System
   13.13 +import java.util.WeakHashMap
   13.14 +import java.lang.ref.WeakReference
   13.15 +import javax.xml.parsers.DocumentBuilderFactory
   13.16 +
   13.17 +import scala.actors.Actor._
   13.18 +import scala.collection.mutable
   13.19 +
   13.20 +
   13.21 +object XML
   13.22 +{
   13.23 +  /** XML trees **/
   13.24 +
   13.25 +  /* datatype representation */
   13.26 +
   13.27 +  type Attributes = Properties.T
   13.28 +
   13.29 +  sealed abstract class Tree { override def toString = string_of_tree(this) }
   13.30 +  case class Elem(markup: Markup, body: List[Tree]) extends Tree
   13.31 +  case class Text(content: String) extends Tree
   13.32 +
   13.33 +  def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
   13.34 +  def elem(name: String) = Elem(Markup(name, Nil), Nil)
   13.35 +
   13.36 +  type Body = List[Tree]
   13.37 +
   13.38 +
   13.39 +  /* string representation */
   13.40 +
   13.41 +  def string_of_body(body: Body): String =
   13.42 +  {
   13.43 +    val s = new StringBuilder
   13.44 +
   13.45 +    def text(txt: String) {
   13.46 +      if (txt == null) s ++= txt
   13.47 +      else {
   13.48 +        for (c <- txt.iterator) c match {
   13.49 +          case '<' => s ++= "&lt;"
   13.50 +          case '>' => s ++= "&gt;"
   13.51 +          case '&' => s ++= "&amp;"
   13.52 +          case '"' => s ++= "&quot;"
   13.53 +          case '\'' => s ++= "&apos;"
   13.54 +          case _ => s += c
   13.55 +        }
   13.56 +      }
   13.57 +    }
   13.58 +    def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
   13.59 +    def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
   13.60 +    def tree(t: Tree): Unit =
   13.61 +      t match {
   13.62 +        case Elem(markup, Nil) =>
   13.63 +          s ++= "<"; elem(markup); s ++= "/>"
   13.64 +        case Elem(markup, ts) =>
   13.65 +          s ++= "<"; elem(markup); s ++= ">"
   13.66 +          ts.foreach(tree)
   13.67 +          s ++= "</"; s ++= markup.name; s ++= ">"
   13.68 +        case Text(txt) => text(txt)
   13.69 +      }
   13.70 +    body.foreach(tree)
   13.71 +    s.toString
   13.72 +  }
   13.73 +
   13.74 +  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
   13.75 +
   13.76 +
   13.77 +  /* text content */
   13.78 +
   13.79 +  def content_stream(tree: Tree): Stream[String] =
   13.80 +    tree match {
   13.81 +      case Elem(_, body) => content_stream(body)
   13.82 +      case Text(content) => Stream(content)
   13.83 +    }
   13.84 +  def content_stream(body: Body): Stream[String] =
   13.85 +    body.toStream.flatten(content_stream(_))
   13.86 +
   13.87 +  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
   13.88 +  def content(body: Body): Iterator[String] = content_stream(body).iterator
   13.89 +
   13.90 +
   13.91 +  /* pipe-lined cache for partial sharing */
   13.92 +
   13.93 +  class Cache(initial_size: Int = 131071, max_string: Int = 100)
   13.94 +  {
   13.95 +    private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
   13.96 +
   13.97 +    private def lookup[A](x: A): Option[A] =
   13.98 +    {
   13.99 +      val ref = table.get(x)
  13.100 +      if (ref == null) None
  13.101 +      else {
  13.102 +        val y = ref.asInstanceOf[WeakReference[A]].get
  13.103 +        if (y == null) None
  13.104 +        else Some(y)
  13.105 +      }
  13.106 +    }
  13.107 +    private def store[A](x: A): A =
  13.108 +    {
  13.109 +      table.put(x, new WeakReference[Any](x))
  13.110 +      x
  13.111 +    }
  13.112 +
  13.113 +    private def trim_bytes(s: String): String = new String(s.toCharArray)
  13.114 +
  13.115 +    private def _cache_string(x: String): String =
  13.116 +      lookup(x) match {
  13.117 +        case Some(y) => y
  13.118 +        case None =>
  13.119 +          val z = trim_bytes(x)
  13.120 +          if (z.length > max_string) z else store(z)
  13.121 +      }
  13.122 +    private def _cache_props(x: Properties.T): Properties.T =
  13.123 +      if (x.isEmpty) x
  13.124 +      else
  13.125 +        lookup(x) match {
  13.126 +          case Some(y) => y
  13.127 +          case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
  13.128 +        }
  13.129 +    private def _cache_markup(x: Markup): Markup =
  13.130 +      lookup(x) match {
  13.131 +        case Some(y) => y
  13.132 +        case None =>
  13.133 +          x match {
  13.134 +            case Markup(name, props) =>
  13.135 +              store(Markup(_cache_string(name), _cache_props(props)))
  13.136 +          }
  13.137 +      }
  13.138 +    private def _cache_tree(x: XML.Tree): XML.Tree =
  13.139 +      lookup(x) match {
  13.140 +        case Some(y) => y
  13.141 +        case None =>
  13.142 +          x match {
  13.143 +            case XML.Elem(markup, body) =>
  13.144 +              store(XML.Elem(_cache_markup(markup), _cache_body(body)))
  13.145 +            case XML.Text(text) => store(XML.Text(_cache_string(text)))
  13.146 +          }
  13.147 +      }
  13.148 +    private def _cache_body(x: XML.Body): XML.Body =
  13.149 +      if (x.isEmpty) x
  13.150 +      else
  13.151 +        lookup(x) match {
  13.152 +          case Some(y) => y
  13.153 +          case None => x.map(_cache_tree(_))
  13.154 +        }
  13.155 +
  13.156 +    // main methods
  13.157 +    def cache_string(x: String): String = synchronized { _cache_string(x) }
  13.158 +    def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
  13.159 +    def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
  13.160 +    def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
  13.161 +  }
  13.162 +
  13.163 +
  13.164 +
  13.165 +  /** document object model (W3C DOM) **/
  13.166 +
  13.167 +  def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
  13.168 +    node.getUserData(Markup.Data.name) match {
  13.169 +      case tree: XML.Tree => Some(tree)
  13.170 +      case _ => None
  13.171 +    }
  13.172 +
  13.173 +  def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
  13.174 +  {
  13.175 +    def DOM(tr: Tree): org.w3c.dom.Node = tr match {
  13.176 +      case Elem(Markup.Data, List(data, t)) =>
  13.177 +        val node = DOM(t)
  13.178 +        node.setUserData(Markup.Data.name, data, null)
  13.179 +        node
  13.180 +      case Elem(Markup(name, atts), ts) =>
  13.181 +        if (name == Markup.Data.name)
  13.182 +          error("Malformed data element: " + tr.toString)
  13.183 +        val node = doc.createElement(name)
  13.184 +        for ((name, value) <- atts) node.setAttribute(name, value)
  13.185 +        for (t <- ts) node.appendChild(DOM(t))
  13.186 +        node
  13.187 +      case Text(txt) => doc.createTextNode(txt)
  13.188 +    }
  13.189 +    DOM(tree)
  13.190 +  }
  13.191 +
  13.192 +
  13.193 +
  13.194 +  /** XML as data representation language **/
  13.195 +
  13.196 +  class XML_Atom(s: String) extends Exception(s)
  13.197 +  class XML_Body(body: XML.Body) extends Exception
  13.198 +
  13.199 +  object Encode
  13.200 +  {
  13.201 +    type T[A] = A => XML.Body
  13.202 +
  13.203 +
  13.204 +    /* atomic values */
  13.205 +
  13.206 +    def long_atom(i: Long): String = i.toString
  13.207 +
  13.208 +    def int_atom(i: Int): String = i.toString
  13.209 +
  13.210 +    def bool_atom(b: Boolean): String = if (b) "1" else "0"
  13.211 +
  13.212 +    def unit_atom(u: Unit) = ""
  13.213 +
  13.214 +
  13.215 +    /* structural nodes */
  13.216 +
  13.217 +    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
  13.218 +
  13.219 +    private def vector(xs: List[String]): XML.Attributes =
  13.220 +      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
  13.221 +
  13.222 +    private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
  13.223 +      XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
  13.224 +
  13.225 +
  13.226 +    /* representation of standard types */
  13.227 +
  13.228 +    val properties: T[Properties.T] =
  13.229 +      (props => List(XML.Elem(Markup(":", props), Nil)))
  13.230 +
  13.231 +    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
  13.232 +
  13.233 +    val long: T[Long] = (x => string(long_atom(x)))
  13.234 +
  13.235 +    val int: T[Int] = (x => string(int_atom(x)))
  13.236 +
  13.237 +    val bool: T[Boolean] = (x => string(bool_atom(x)))
  13.238 +
  13.239 +    val unit: T[Unit] = (x => string(unit_atom(x)))
  13.240 +
  13.241 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
  13.242 +      (x => List(node(f(x._1)), node(g(x._2))))
  13.243 +
  13.244 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
  13.245 +      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
  13.246 +
  13.247 +    def list[A](f: T[A]): T[List[A]] =
  13.248 +      (xs => xs.map((x: A) => node(f(x))))
  13.249 +
  13.250 +    def option[A](f: T[A]): T[Option[A]] =
  13.251 +    {
  13.252 +      case None => Nil
  13.253 +      case Some(x) => List(node(f(x)))
  13.254 +    }
  13.255 +
  13.256 +    def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
  13.257 +    {
  13.258 +      case x =>
  13.259 +        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
  13.260 +        List(tagged(tag, f(x)))
  13.261 +    }
  13.262 +  }
  13.263 +
  13.264 +  object Decode
  13.265 +  {
  13.266 +    type T[A] = XML.Body => A
  13.267 +    type V[A] = (List[String], XML.Body) => A
  13.268 +
  13.269 +
  13.270 +    /* atomic values */
  13.271 +
  13.272 +    def long_atom(s: String): Long =
  13.273 +      try { java.lang.Long.parseLong(s) }
  13.274 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  13.275 +
  13.276 +    def int_atom(s: String): Int =
  13.277 +      try { Integer.parseInt(s) }
  13.278 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  13.279 +
  13.280 +    def bool_atom(s: String): Boolean =
  13.281 +      if (s == "1") true
  13.282 +      else if (s == "0") false
  13.283 +      else throw new XML_Atom(s)
  13.284 +
  13.285 +    def unit_atom(s: String): Unit =
  13.286 +      if (s == "") () else throw new XML_Atom(s)
  13.287 +
  13.288 +
  13.289 +    /* structural nodes */
  13.290 +
  13.291 +    private def node(t: XML.Tree): XML.Body =
  13.292 +      t match {
  13.293 +        case XML.Elem(Markup(":", Nil), ts) => ts
  13.294 +        case _ => throw new XML_Body(List(t))
  13.295 +      }
  13.296 +
  13.297 +    private def vector(atts: XML.Attributes): List[String] =
  13.298 +    {
  13.299 +      val xs = new mutable.ListBuffer[String]
  13.300 +      var i = 0
  13.301 +      for ((a, x) <- atts) {
  13.302 +        if (int_atom(a) == i) { xs += x; i = i + 1 }
  13.303 +        else throw new XML_Atom(a)
  13.304 +      }
  13.305 +      xs.toList
  13.306 +    }
  13.307 +
  13.308 +    private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
  13.309 +      t match {
  13.310 +        case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
  13.311 +        case _ => throw new XML_Body(List(t))
  13.312 +      }
  13.313 +
  13.314 +
  13.315 +    /* representation of standard types */
  13.316 +
  13.317 +    val properties: T[Properties.T] =
  13.318 +    {
  13.319 +      case List(XML.Elem(Markup(":", props), Nil)) => props
  13.320 +      case ts => throw new XML_Body(ts)
  13.321 +    }
  13.322 +
  13.323 +    val string: T[String] =
  13.324 +    {
  13.325 +      case Nil => ""
  13.326 +      case List(XML.Text(s)) => s
  13.327 +      case ts => throw new XML_Body(ts)
  13.328 +    }
  13.329 +
  13.330 +    val long: T[Long] = (x => long_atom(string(x)))
  13.331 +
  13.332 +    val int: T[Int] = (x => int_atom(string(x)))
  13.333 +
  13.334 +    val bool: T[Boolean] = (x => bool_atom(string(x)))
  13.335 +
  13.336 +    val unit: T[Unit] = (x => unit_atom(string(x)))
  13.337 +
  13.338 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
  13.339 +    {
  13.340 +      case List(t1, t2) => (f(node(t1)), g(node(t2)))
  13.341 +      case ts => throw new XML_Body(ts)
  13.342 +    }
  13.343 +
  13.344 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
  13.345 +    {
  13.346 +      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
  13.347 +      case ts => throw new XML_Body(ts)
  13.348 +    }
  13.349 +
  13.350 +    def list[A](f: T[A]): T[List[A]] =
  13.351 +      (ts => ts.map(t => f(node(t))))
  13.352 +
  13.353 +    def option[A](f: T[A]): T[Option[A]] =
  13.354 +    {
  13.355 +      case Nil => None
  13.356 +      case List(t) => Some(f(node(t)))
  13.357 +      case ts => throw new XML_Body(ts)
  13.358 +    }
  13.359 +
  13.360 +    def variant[A](fs: List[V[A]]): T[A] =
  13.361 +    {
  13.362 +      case List(t) =>
  13.363 +        val (tag, (xs, ts)) = tagged(t)
  13.364 +        val f =
  13.365 +          try { fs(tag) }
  13.366 +          catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
  13.367 +        f(xs, ts)
  13.368 +      case ts => throw new XML_Body(ts)
  13.369 +    }
  13.370 +  }
  13.371 +}
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Pure/PIDE/yxml.ML	Sun Sep 04 20:37:20 2011 +0200
    14.3 @@ -0,0 +1,148 @@
    14.4 +(*  Title:      Pure/PIDE/yxml.ML
    14.5 +    Author:     Makarius
    14.6 +
    14.7 +Efficient text representation of XML trees using extra characters X
    14.8 +and Y -- no escaping, may nest marked text verbatim.  Suitable for
    14.9 +direct inlining into plain text.
   14.10 +
   14.11 +Markup <elem att="val" ...>...body...</elem> is encoded as:
   14.12 +
   14.13 +  X Y name Y att=val ... X
   14.14 +  ...
   14.15 +  body
   14.16 +  ...
   14.17 +  X Y X
   14.18 +*)
   14.19 +
   14.20 +signature YXML =
   14.21 +sig
   14.22 +  val X: Symbol.symbol
   14.23 +  val Y: Symbol.symbol
   14.24 +  val embed_controls: string -> string
   14.25 +  val detect: string -> bool
   14.26 +  val output_markup: Markup.T -> string * string
   14.27 +  val element: string -> XML.attributes -> string list -> string
   14.28 +  val string_of_body: XML.body -> string
   14.29 +  val string_of: XML.tree -> string
   14.30 +  val parse_body: string -> XML.body
   14.31 +  val parse: string -> XML.tree
   14.32 +end;
   14.33 +
   14.34 +structure YXML: YXML =
   14.35 +struct
   14.36 +
   14.37 +(** string representation **)
   14.38 +
   14.39 +(* idempotent recoding of certain low ASCII control characters *)
   14.40 +
   14.41 +fun pseudo_utf8 c =
   14.42 +  if Symbol.is_ascii_control c
   14.43 +  then chr 192 ^ chr (128 + ord c)
   14.44 +  else c;
   14.45 +
   14.46 +fun embed_controls str =
   14.47 +  if exists_string Symbol.is_ascii_control str
   14.48 +  then translate_string pseudo_utf8 str
   14.49 +  else str;
   14.50 +
   14.51 +
   14.52 +(* markers *)
   14.53 +
   14.54 +val X = chr 5;
   14.55 +val Y = chr 6;
   14.56 +val XY = X ^ Y;
   14.57 +val XYX = XY ^ X;
   14.58 +
   14.59 +val detect = exists_string (fn s => s = X orelse s = Y);
   14.60 +
   14.61 +
   14.62 +(* output *)
   14.63 +
   14.64 +fun output_markup (markup as (name, atts)) =
   14.65 +  if Markup.is_empty markup then Markup.no_output
   14.66 +  else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
   14.67 +
   14.68 +fun element name atts body =
   14.69 +  let val (pre, post) = output_markup (name, atts)
   14.70 +  in pre ^ implode body ^ post end;
   14.71 +
   14.72 +fun string_of_body body =
   14.73 +  let
   14.74 +    fun attrib (a, x) =
   14.75 +      Buffer.add Y #>
   14.76 +      Buffer.add a #> Buffer.add "=" #> Buffer.add x;
   14.77 +    fun tree (XML.Elem ((name, atts), ts)) =
   14.78 +          Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
   14.79 +          trees ts #>
   14.80 +          Buffer.add XYX
   14.81 +      | tree (XML.Text s) = Buffer.add s
   14.82 +    and trees ts = fold tree ts;
   14.83 +  in Buffer.empty |> trees body |> Buffer.content end;
   14.84 +
   14.85 +val string_of = string_of_body o single;
   14.86 +
   14.87 +
   14.88 +
   14.89 +(** efficient YXML parsing **)
   14.90 +
   14.91 +local
   14.92 +
   14.93 +(* splitting *)
   14.94 +
   14.95 +fun is_char s c = ord s = Char.ord c;
   14.96 +
   14.97 +val split_string =
   14.98 +  Substring.full #>
   14.99 +  Substring.tokens (is_char X) #>
  14.100 +  map (Substring.fields (is_char Y) #> map Substring.string);
  14.101 +
  14.102 +
  14.103 +(* structural errors *)
  14.104 +
  14.105 +fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
  14.106 +fun err_attribute () = err "bad attribute";
  14.107 +fun err_element () = err "bad element";
  14.108 +fun err_unbalanced "" = err "unbalanced element"
  14.109 +  | err_unbalanced name = err ("unbalanced element " ^ quote name);
  14.110 +
  14.111 +
  14.112 +(* stack operations *)
  14.113 +
  14.114 +fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
  14.115 +
  14.116 +fun push "" _ _ = err_element ()
  14.117 +  | push name atts pending = ((name, atts), []) :: pending;
  14.118 +
  14.119 +fun pop ((("", _), _) :: _) = err_unbalanced ""
  14.120 +  | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
  14.121 +
  14.122 +
  14.123 +(* parsing *)
  14.124 +
  14.125 +fun parse_attrib s =
  14.126 +  (case first_field "=" s of
  14.127 +    NONE => err_attribute ()
  14.128 +  | SOME ("", _) => err_attribute ()
  14.129 +  | SOME att => att);
  14.130 +
  14.131 +fun parse_chunk ["", ""] = pop
  14.132 +  | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
  14.133 +  | parse_chunk txts = fold (add o XML.Text) txts;
  14.134 +
  14.135 +in
  14.136 +
  14.137 +fun parse_body source =
  14.138 +  (case fold parse_chunk (split_string source) [(("", []), [])] of
  14.139 +    [(("", _), result)] => rev result
  14.140 +  | ((name, _), _) :: _ => err_unbalanced name);
  14.141 +
  14.142 +fun parse source =
  14.143 +  (case parse_body source of
  14.144 +    [result] => result
  14.145 +  | [] => XML.Text ""
  14.146 +  | _ => err "multiple results");
  14.147 +
  14.148 +end;
  14.149 +
  14.150 +end;
  14.151 +
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/Pure/PIDE/yxml.scala	Sun Sep 04 20:37:20 2011 +0200
    15.3 @@ -0,0 +1,135 @@
    15.4 +/*  Title:      Pure/PIDE/yxml.scala
    15.5 +    Author:     Makarius
    15.6 +
    15.7 +Efficient text representation of XML trees.  Suitable for direct
    15.8 +inlining into plain text.
    15.9 +*/
   15.10 +
   15.11 +package isabelle
   15.12 +
   15.13 +
   15.14 +import scala.collection.mutable
   15.15 +
   15.16 +
   15.17 +object YXML
   15.18 +{
   15.19 +  /* chunk markers */
   15.20 +
   15.21 +  val X = '\5'
   15.22 +  val Y = '\6'
   15.23 +  val X_string = X.toString
   15.24 +  val Y_string = Y.toString
   15.25 +
   15.26 +  def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
   15.27 +
   15.28 +
   15.29 +  /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
   15.30 +
   15.31 +  def string_of_body(body: XML.Body): String =
   15.32 +  {
   15.33 +    val s = new StringBuilder
   15.34 +    def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
   15.35 +    def tree(t: XML.Tree): Unit =
   15.36 +      t match {
   15.37 +        case XML.Elem(Markup(name, atts), ts) =>
   15.38 +          s += X; s += Y; s++= name; atts.foreach(attrib); s += X
   15.39 +          ts.foreach(tree)
   15.40 +          s += X; s += Y; s += X
   15.41 +        case XML.Text(text) => s ++= text
   15.42 +      }
   15.43 +    body.foreach(tree)
   15.44 +    s.toString
   15.45 +  }
   15.46 +
   15.47 +  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
   15.48 +
   15.49 +
   15.50 +  /* parsing */
   15.51 +
   15.52 +  private def err(msg: String) = error("Malformed YXML: " + msg)
   15.53 +  private def err_attribute() = err("bad attribute")
   15.54 +  private def err_element() = err("bad element")
   15.55 +  private def err_unbalanced(name: String) =
   15.56 +    if (name == "") err("unbalanced element")
   15.57 +    else err("unbalanced element " + quote(name))
   15.58 +
   15.59 +  private def parse_attrib(source: CharSequence) = {
   15.60 +    val s = source.toString
   15.61 +    val i = s.indexOf('=')
   15.62 +    if (i <= 0) err_attribute()
   15.63 +    (s.substring(0, i), s.substring(i + 1))
   15.64 +  }
   15.65 +
   15.66 +
   15.67 +  def parse_body(source: CharSequence): XML.Body =
   15.68 +  {
   15.69 +    /* stack operations */
   15.70 +
   15.71 +    def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
   15.72 +    var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
   15.73 +
   15.74 +    def add(x: XML.Tree)
   15.75 +    {
   15.76 +      (stack: @unchecked) match { case ((_, body) :: _) => body += x }
   15.77 +    }
   15.78 +
   15.79 +    def push(name: String, atts: XML.Attributes)
   15.80 +    {
   15.81 +      if (name == "") err_element()
   15.82 +      else stack = (Markup(name, atts), buffer()) :: stack
   15.83 +    }
   15.84 +
   15.85 +    def pop()
   15.86 +    {
   15.87 +      (stack: @unchecked) match {
   15.88 +        case ((Markup.Empty, _) :: _) => err_unbalanced("")
   15.89 +        case ((markup, body) :: pending) =>
   15.90 +          stack = pending
   15.91 +          add(XML.Elem(markup, body.toList))
   15.92 +      }
   15.93 +    }
   15.94 +
   15.95 +
   15.96 +    /* parse chunks */
   15.97 +
   15.98 +    for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
   15.99 +      if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
  15.100 +      else {
  15.101 +        Library.chunks(chunk, Y).toList match {
  15.102 +          case ch :: name :: atts if ch.length == 0 =>
  15.103 +            push(name.toString, atts.map(parse_attrib))
  15.104 +          case txts => for (txt <- txts) add(XML.Text(txt.toString))
  15.105 +        }
  15.106 +      }
  15.107 +    }
  15.108 +    (stack: @unchecked) match {
  15.109 +      case List((Markup.Empty, body)) => body.toList
  15.110 +      case (Markup(name, _), _) :: _ => err_unbalanced(name)
  15.111 +    }
  15.112 +  }
  15.113 +
  15.114 +  def parse(source: CharSequence): XML.Tree =
  15.115 +    parse_body(source) match {
  15.116 +      case List(result) => result
  15.117 +      case Nil => XML.Text("")
  15.118 +      case _ => err("multiple results")
  15.119 +    }
  15.120 +
  15.121 +
  15.122 +  /* failsafe parsing */
  15.123 +
  15.124 +  private def markup_malformed(source: CharSequence) =
  15.125 +    XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
  15.126 +
  15.127 +  def parse_body_failsafe(source: CharSequence): XML.Body =
  15.128 +  {
  15.129 +    try { parse_body(source) }
  15.130 +    catch { case ERROR(_) => List(markup_malformed(source)) }
  15.131 +  }
  15.132 +
  15.133 +  def parse_failsafe(source: CharSequence): XML.Tree =
  15.134 +  {
  15.135 +    try { parse(source) }
  15.136 +    catch { case ERROR(_) => markup_malformed(source) }
  15.137 +  }
  15.138 +}
    16.1 --- a/src/Pure/ROOT.ML	Sun Sep 04 10:29:38 2011 -0700
    16.2 +++ b/src/Pure/ROOT.ML	Sun Sep 04 20:37:20 2011 +0200
    16.3 @@ -54,17 +54,18 @@
    16.4  use "General/linear_set.ML";
    16.5  use "General/buffer.ML";
    16.6  use "General/pretty.ML";
    16.7 -use "General/xml.ML";
    16.8  use "General/path.ML";
    16.9  use "General/url.ML";
   16.10  use "General/file.ML";
   16.11 -use "General/yxml.ML";
   16.12  use "General/long_name.ML";
   16.13  use "General/binding.ML";
   16.14  
   16.15  use "General/sha1.ML";
   16.16  if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
   16.17  
   16.18 +use "PIDE/xml.ML";
   16.19 +use "PIDE/yxml.ML";
   16.20 +
   16.21  
   16.22  (* concurrency within the ML runtime *)
   16.23  
    17.1 --- a/src/Pure/Syntax/lexicon.ML	Sun Sep 04 10:29:38 2011 -0700
    17.2 +++ b/src/Pure/Syntax/lexicon.ML	Sun Sep 04 20:37:20 2011 +0200
    17.3 @@ -190,8 +190,8 @@
    17.4  
    17.5  val token_kind_markup =
    17.6   fn Literal     => Markup.literal
    17.7 -  | IdentSy     => Markup.ident
    17.8 -  | LongIdentSy => Markup.ident
    17.9 +  | IdentSy     => Markup.empty
   17.10 +  | LongIdentSy => Markup.empty
   17.11    | VarSy       => Markup.var
   17.12    | TFreeSy     => Markup.tfree
   17.13    | TVarSy      => Markup.tvar
    18.1 --- a/src/Pure/System/isabelle_process.scala	Sun Sep 04 10:29:38 2011 -0700
    18.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Sep 04 20:37:20 2011 +0200
    18.3 @@ -99,12 +99,10 @@
    18.4    {
    18.5      if (kind == Markup.INIT) rm_fifos()
    18.6      if (kind == Markup.RAW)
    18.7 -      xml_cache.cache_ignore(
    18.8 -        new Result(XML.Elem(Markup(kind, props), body)))((result: Result) => receiver ! result)
    18.9 +      receiver ! new Result(XML.Elem(Markup(kind, props), body))
   18.10      else {
   18.11        val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
   18.12 -      xml_cache.cache_tree(msg)((message: XML.Tree) =>
   18.13 -        receiver ! new Result(message.asInstanceOf[XML.Elem]))
   18.14 +      receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
   18.15      }
   18.16    }
   18.17  
    19.1 --- a/src/Pure/Thy/thy_syntax.ML	Sun Sep 04 10:29:38 2011 -0700
    19.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sun Sep 04 20:37:20 2011 +0200
    19.3 @@ -45,14 +45,14 @@
    19.4  val token_kind_markup =
    19.5   fn Token.Command       => Markup.command
    19.6    | Token.Keyword       => Markup.keyword
    19.7 -  | Token.Ident         => Markup.ident
    19.8 -  | Token.LongIdent     => Markup.ident
    19.9 -  | Token.SymIdent      => Markup.ident
   19.10 +  | Token.Ident         => Markup.empty
   19.11 +  | Token.LongIdent     => Markup.empty
   19.12 +  | Token.SymIdent      => Markup.empty
   19.13    | Token.Var           => Markup.var
   19.14    | Token.TypeIdent     => Markup.tfree
   19.15    | Token.TypeVar       => Markup.tvar
   19.16 -  | Token.Nat           => Markup.ident
   19.17 -  | Token.Float         => Markup.ident
   19.18 +  | Token.Nat           => Markup.empty
   19.19 +  | Token.Float         => Markup.empty
   19.20    | Token.String        => Markup.string
   19.21    | Token.AltString     => Markup.altstring
   19.22    | Token.Verbatim      => Markup.verbatim
    20.1 --- a/src/Pure/build-jars	Sun Sep 04 10:29:38 2011 -0700
    20.2 +++ b/src/Pure/build-jars	Sun Sep 04 20:37:20 2011 +0200
    20.3 @@ -24,8 +24,6 @@
    20.4    General/scan.scala
    20.5    General/sha1.scala
    20.6    General/symbol.scala
    20.7 -  General/xml.scala
    20.8 -  General/yxml.scala
    20.9    Isar/keyword.scala
   20.10    Isar/outer_syntax.scala
   20.11    Isar/parse.scala
   20.12 @@ -36,6 +34,8 @@
   20.13    PIDE/isar_document.scala
   20.14    PIDE/markup_tree.scala
   20.15    PIDE/text.scala
   20.16 +  PIDE/xml.scala
   20.17 +  PIDE/yxml.scala
   20.18    System/cygwin.scala
   20.19    System/download.scala
   20.20    System/event_bus.scala
    21.1 --- a/src/Tools/jEdit/README	Sun Sep 04 10:29:38 2011 -0700
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,62 +0,0 @@
    21.4 -Isabelle/jEdit based on Isabelle/Scala
    21.5 -======================================
    21.6 -
    21.7 -The Isabelle/Scala layer that is already part of Isabelle/Pure
    21.8 -provides some general infrastructure for advanced prover interaction
    21.9 -and integration.  The Isabelle/jEdit application serves as an example
   21.10 -for asynchronous proof checking with support for parallel processing.
   21.11 -
   21.12 -See also the paper:
   21.13 -
   21.14 -  Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala
   21.15 -  and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors,
   21.16 -  User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite
   21.17 -  Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS.
   21.18 -  http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf
   21.19 -
   21.20 -
   21.21 -Known problems with Mac OS
   21.22 -==========================
   21.23 -
   21.24 -- The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
   21.25 -  e.g. between the editor and the Console plugin, which is a standard
   21.26 -  swing text box.  Similar for search boxes etc.
   21.27 -
   21.28 -- ToggleButton selected state is not rendered if window focus is lost,
   21.29 -  which is probably a genuine feature of the Apple look-and-feel.
   21.30 -
   21.31 -- Anti-aliasing does not really work as well as for Linux or Windows.
   21.32 -  (General Apple/Swing problem?)
   21.33 -
   21.34 -- Font.createFont mangles the font family of non-regular fonts,
   21.35 -  e.g. bold.  IsabelleText font files need to be installed manually.
   21.36 -
   21.37 -- Missing glyphs are collected from other fonts (like Emacs, Firefox).
   21.38 -  This is actually an advantage over the Oracle/Sun JVM on Windows or
   21.39 -  Linux, but probably also the deeper reason for the other oddities of
   21.40 -  Apple font management.
   21.41 -
   21.42 -- The native font renderer of -Dapple.awt.graphics.UseQuartz=true
   21.43 -  fails to handle the infinitesimal font size of "hidden" text (e.g.
   21.44 -  used in Isabelle sub/superscripts).
   21.45 -
   21.46 -
   21.47 -Known problems with OpenJDK
   21.48 -===========================
   21.49 -
   21.50 -- The 2D rendering engine of OpenJDK 1.6.x distorts the appearance of
   21.51 -  the jEdit text area.  Always use official JRE 1.6.x from
   21.52 -  Sun/Oracle/Apple.
   21.53 -
   21.54 -
   21.55 -Licenses and home sites of contributing systems
   21.56 -===============================================
   21.57 -
   21.58 -* Scala: BSD-style
   21.59 -  http://www.scala-lang.org
   21.60 -
   21.61 -* jEdit: GPL (with special cases)
   21.62 -  http://www.jedit.org/
   21.63 -
   21.64 -* Lobo/Cobra: GPL and LGPL
   21.65 -  http://lobobrowser.org/
    22.1 --- a/src/Tools/jEdit/README.html	Sun Sep 04 10:29:38 2011 -0700
    22.2 +++ b/src/Tools/jEdit/README.html	Sun Sep 04 20:37:20 2011 +0200
    22.3 @@ -12,7 +12,12 @@
    22.4  
    22.5  <body>
    22.6  
    22.7 -<h2>The Isabelle/jEdit Prover IDE</h2>
    22.8 +<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
    22.9 +
   22.10 +The Isabelle/Scala layer that is already part of Isabelle/Pure
   22.11 +provides some general infrastructure for advanced prover interaction
   22.12 +and integration.  The Isabelle/jEdit application serves as an example
   22.13 +for asynchronous proof checking with support for parallel processing.
   22.14  
   22.15  <ul>
   22.16  
   22.17 @@ -116,30 +121,23 @@
   22.18  </ul>
   22.19  
   22.20  
   22.21 -<h2>Limitations and workrounds (January 2011)</h2>
   22.22 +<h2>Limitations and workrounds (September 2011)</h2>
   22.23  
   22.24  <ul>
   22.25    <li>No way to start/stop prover or switch to a different logic.<br/>
   22.26    <em>Workaround:</em> Change options and restart editor.</li>
   22.27  
   22.28 -  <li>Limited support for dependencies between multiple theory buffers.<br/>
   22.29 -  <em>Workaround:</em> Load required files manually.</li>
   22.30 -
   22.31 -  <li>No reclaiming of old/unused document versions in prover or
   22.32 -  editor.<br/>
   22.33 -  <em>Workaround:</em> Avoid large files; restart after a few hours of use.</li>
   22.34 -
   22.35    <li>Incremental reparsing sometimes produces unexpected command
   22.36    spans.<br/>
   22.37    <em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
   22.38  
   22.39 -  <li>Command execution sometimes gets stuck (purple background).<br/>
   22.40 -  <em>Workaround:</em> Force reparsing as above.</li>
   22.41 +  <li>Odd behavior of some diagnostic commands, notably those starting
   22.42 +  external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/>
   22.43 +  <em>Workaround:</em> Avoid such commands.</li>
   22.44  
   22.45 -  <li>Odd behavior of some diagnostic commands, notably those
   22.46 -  starting external processes asynchronously
   22.47 -  (e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/>
   22.48 -  <em>Workaround:</em> Avoid such commands.</li>
   22.49 +  <li>Lack of dependency managed for auxiliary files that contribute
   22.50 +  to a theory ("<b>uses</b>").<br/>
   22.51 +  <em>Workaround:</em> Re-use files manually within the prover.</li>
   22.52  
   22.53    <li>No support for non-local markup, e.g. commands reporting on
   22.54    previous commands (proof end on proof head), or markup produced by
   22.55 @@ -149,6 +147,59 @@
   22.56    General.</li>
   22.57  </ul>
   22.58  
   22.59 +
   22.60 +<h2>Known problems with Mac OS</h2>
   22.61 +
   22.62 +<ul>
   22.63 +
   22.64 +<li>The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
   22.65 +  e.g. between the editor and the Console plugin, which is a standard
   22.66 +  swing text box.  Similar for search boxes etc.</li>
   22.67 +
   22.68 +<li>ToggleButton selected state is not rendered if window focus is
   22.69 +  lost, which is probably a genuine feature of the Apple
   22.70 +  look-and-feel.</li>
   22.71 +
   22.72 +<li>Font.createFont mangles the font family of non-regular fonts,
   22.73 +  e.g. bold.  IsabelleText font files need to be installed/updated
   22.74 +  manually.</li>
   22.75 +
   22.76 +<li>Missing glyphs are collected from other fonts (like Emacs,
   22.77 +  Firefox).  This is actually an advantage over the Oracle/Sun JVM on
   22.78 +  Windows or Linux, but probably also the deeper reason for the other
   22.79 +  oddities of Apple font management.</li>
   22.80 +
   22.81 +<li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true
   22.82 +  (not enabled by default) fails to handle the infinitesimal font size
   22.83 +  of "hidden" text (e.g.  used in Isabelle sub/superscripts).</li>
   22.84 +
   22.85 +</ul>
   22.86 +
   22.87 +
   22.88 +<h2>Known problems with OpenJDK 1.6.x</h2>
   22.89 +
   22.90 +<ul>
   22.91 +
   22.92 +<li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
   22.93 +  of the jEdit text area.  Always use official JRE 1.6.x from
   22.94 +  Sun/Oracle/Apple.</li>
   22.95 +
   22.96 +<li>jEdit on OpenJDK is generally not supported.</li>
   22.97 +
   22.98 +</ul>
   22.99 +
  22.100 +
  22.101 +<h2>Licenses and home sites of contributing systems</h2>
  22.102 +
  22.103 +<ul>
  22.104 +
  22.105 +<li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
  22.106 +
  22.107 +<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
  22.108 +
  22.109 +<li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org/</li>
  22.110 +
  22.111 +</ul>
  22.112 +
  22.113  </body>
  22.114  </html>
  22.115 -
    23.1 --- a/src/Tools/jEdit/README_BUILD	Sun Sep 04 10:29:38 2011 -0700
    23.2 +++ b/src/Tools/jEdit/README_BUILD	Sun Sep 04 20:37:20 2011 +0200
    23.3 @@ -1,14 +1,14 @@
    23.4  Requirements for instantaneous build from sources
    23.5  =================================================
    23.6  
    23.7 -* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_26
    23.8 -  http://java.sun.com/javase/downloads/index.jsp
    23.9 +* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_27
   23.10 +  http://www.oracle.com/technetwork/java/javase/downloads/index.html
   23.11  
   23.12  * Scala Compiler 2.8.1.final
   23.13    http://www.scala-lang.org
   23.14  
   23.15  * Auxiliary jedit_build component
   23.16 -  http://www4.in.tum.de/~wenzelm/test/jedit_build-20110521.tar.gz
   23.17 +  http://www4.in.tum.de/~wenzelm/test/jedit_build-20110622.tar.gz
   23.18  
   23.19  
   23.20  Important settings within Isabelle environment
    24.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Sun Sep 04 10:29:38 2011 -0700
    24.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sun Sep 04 20:37:20 2011 +0200
    24.3 @@ -128,10 +128,7 @@
    24.4    }
    24.5  
    24.6    private val text_entity_colors: Map[String, Color] =
    24.7 -    Map(
    24.8 -      Markup.CLASS -> get_color("red"),
    24.9 -      Markup.TYPE -> get_color("black"),
   24.10 -      Markup.CONSTANT -> get_color("black"))
   24.11 +    Map(Markup.CLASS -> get_color("red"))
   24.12  
   24.13    private val text_colors: Map[String, Color] =
   24.14      Map(
   24.15 @@ -140,7 +137,6 @@
   24.16        Markup.VERBATIM -> get_color("black"),
   24.17        Markup.LITERAL -> keyword1_color,
   24.18        Markup.DELIMITER -> get_color("black"),
   24.19 -      Markup.IDENT -> get_color("black"),
   24.20        Markup.TFREE -> get_color("#A020F0"),
   24.21        Markup.TVAR -> get_color("#A020F0"),
   24.22        Markup.FREE -> get_color("blue"),
    25.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Sun Sep 04 10:29:38 2011 -0700
    25.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Sun Sep 04 20:37:20 2011 +0200
    25.3 @@ -63,6 +63,6 @@
    25.4        tooltip_margin.getValue().asInstanceOf[Int]
    25.5  
    25.6      Isabelle.Time_Property("tooltip-dismiss-delay") =
    25.7 -      Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
    25.8 +      Time.ms(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
    25.9    }
   25.10  }
    26.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Sep 04 10:29:38 2011 -0700
    26.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Sep 04 20:37:20 2011 +0200
    26.3 @@ -123,8 +123,10 @@
    26.4          Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
    26.5        HTML.encode(text) + "</pre></html>"
    26.6  
    26.7 +  private val tooltip_lb = Time.seconds(0.5)
    26.8 +  private val tooltip_ub = Time.seconds(60.0)
    26.9    def tooltip_dismiss_delay(): Time =
   26.10 -    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
   26.11 +    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub
   26.12  
   26.13    def setup_tooltips()
   26.14    {
    27.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Sep 04 10:29:38 2011 -0700
    27.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Sep 04 20:37:20 2011 +0200
    27.3 @@ -173,41 +173,42 @@
    27.4            case _ => Some(Scan.Finished)
    27.5          }
    27.6        val context1 =
    27.7 -        if (line_ctxt.isDefined && Isabelle.session.is_ready) {
    27.8 -          val syntax = Isabelle.session.current_syntax()
    27.9 -    
   27.10 -          val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
   27.11 -          val context1 = new Line_Context(Some(ctxt1))
   27.12 -    
   27.13 -          val extended = extended_styles(line)
   27.14 -    
   27.15 -          var offset = 0
   27.16 -          for (token <- tokens) {
   27.17 -            val style = Isabelle_Markup.token_markup(syntax, token)
   27.18 -            val length = token.source.length
   27.19 -            val end_offset = offset + length
   27.20 -            if ((offset until end_offset) exists extended.isDefinedAt) {
   27.21 -              for (i <- offset until end_offset) {
   27.22 -                val style1 =
   27.23 -                  extended.get(i) match {
   27.24 -                    case None => style
   27.25 -                    case Some(ext) => ext(style)
   27.26 -                  }
   27.27 -                handler.handleToken(line, style1, i, 1, context1)
   27.28 -              }
   27.29 +      {
   27.30 +        val (styled_tokens, context1) =
   27.31 +          if (line_ctxt.isDefined && Isabelle.session.is_ready) {
   27.32 +            val syntax = Isabelle.session.current_syntax()
   27.33 +            val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
   27.34 +            val styled_tokens = tokens.map(tok => (Isabelle_Markup.token_markup(syntax, tok), tok))
   27.35 +            (styled_tokens, new Line_Context(Some(ctxt1)))
   27.36 +          }
   27.37 +          else {
   27.38 +            val token = Token(Token.Kind.UNPARSED, line.subSequence(0, line.count).toString)
   27.39 +            (List((JEditToken.NULL, token)), new Line_Context(None))
   27.40 +          }
   27.41 +
   27.42 +        val extended = extended_styles(line)
   27.43 +
   27.44 +        var offset = 0
   27.45 +        for ((style, token) <- styled_tokens) {
   27.46 +          val length = token.source.length
   27.47 +          val end_offset = offset + length
   27.48 +          if ((offset until end_offset) exists
   27.49 +              (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
   27.50 +            for (i <- offset until end_offset) {
   27.51 +              val style1 =
   27.52 +                extended.get(i) match {
   27.53 +                  case None => style
   27.54 +                  case Some(ext) => ext(style)
   27.55 +                }
   27.56 +              handler.handleToken(line, style1, i, 1, context1)
   27.57              }
   27.58 -            else handler.handleToken(line, style, offset, length, context1)
   27.59 -            offset += length
   27.60            }
   27.61 -          handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   27.62 -          context1
   27.63 +          else handler.handleToken(line, style, offset, length, context1)
   27.64 +          offset += length
   27.65          }
   27.66 -        else {
   27.67 -          val context1 = new Line_Context(None)
   27.68 -          handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
   27.69 -          handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   27.70 -          context1
   27.71 -        }
   27.72 +        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   27.73 +        context1
   27.74 +      }
   27.75        val context2 = context1.intern
   27.76        handler.setLineContext(context2)
   27.77        context2