src/HOL/Import/xml.ML
author obua
Thu, 16 Feb 2006 23:40:32 +0100
changeset 19091 a6a15d3446ad
parent 19089 2e487fe9593a
child 19093 6d584f9d2021
permissions -rw-r--r--
use VectorScannerSeq instead of ListScannerSeq in xml.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19064
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
     1
(*  Title:      Pure/General/xml.ML
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
     2
    ID:         $Id$
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
     3
    Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
     4
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
     5
Basic support for XML.
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
     6
*)
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
     7
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
     8
signature XML =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
     9
sig
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    10
  val header: string
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    11
  val text: string -> string
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    12
  val text_charref: string -> string
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    13
  val cdata: string -> string
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    14
  val element: string -> (string * string) list -> string list -> string
19089
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
    15
  
19064
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    16
  datatype tree =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    17
      Elem of string * (string * string) list * tree list
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    18
    | Text of string
19089
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
    19
  
19064
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    20
  val string_of_tree: tree -> string
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    21
  val tree_of_string: string -> tree
19089
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
    22
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
    23
  val encoded_string_of_tree : tree -> string
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
    24
  val tree_of_encoded_string : string -> tree
19064
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    25
end;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    26
19089
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
    27
structure XML :> XML =
19064
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    28
struct
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    29
19091
a6a15d3446ad use VectorScannerSeq instead of ListScannerSeq in xml.ML
obua
parents: 19089
diff changeset
    30
structure Seq = VectorScannerSeq
19089
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
    31
structure Scan = Scanner (structure Seq = Seq)
19064
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    32
open Scan
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    33
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    34
(** string based representation (small scale) **)
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    35
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    36
val header = "<?xml version=\"1.0\"?>\n";
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    37
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    38
(* text and character data *)
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    39
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    40
fun decode "&lt;" = "<"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    41
  | decode "&gt;" = ">"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    42
  | decode "&amp;" = "&"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    43
  | decode "&apos;" = "'"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    44
  | decode "&quot;" = "\""
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    45
  | decode c = c;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    46
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    47
fun encode "<" = "&lt;"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    48
  | encode ">" = "&gt;"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    49
  | encode "&" = "&amp;"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    50
  | encode "'" = "&apos;"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    51
  | encode "\"" = "&quot;"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    52
  | encode c = c;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    53
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    54
fun encode_charref c = "&#" ^ Int.toString (ord c) ^ ";"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    55
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    56
val text = Library.translate_string encode
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    57
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    58
val text_charref = translate_string encode_charref;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    59
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    60
val cdata = enclose "<![CDATA[" "]]>\n"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    61
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    62
(* elements *)
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    63
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    64
fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    65
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    66
fun element name atts cs =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    67
  let val elem = space_implode " " (name :: map attribute atts) in
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    68
    if null cs then enclose "<" "/>" elem
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    69
    else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    70
  end;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    71
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    72
(** explicit XML trees **)
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    73
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    74
datatype tree =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    75
    Elem of string * (string * string) list * tree list
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    76
  | Text of string;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    77
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    78
fun string_of_tree tree =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    79
  let
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    80
    fun string_of (Elem (name, atts, ts)) buf =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    81
        let val buf' =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    82
          buf |> Buffer.add "<"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    83
          |> fold Buffer.add (separate " " (name :: map attribute atts))
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    84
        in
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    85
          if null ts then
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    86
            buf' |> Buffer.add "/>"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    87
          else
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    88
            buf' |> Buffer.add ">"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    89
            |> fold string_of ts
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    90
            |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    91
        end
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    92
      | string_of (Text s) buf = Buffer.add (text s) buf;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    93
  in Buffer.content (string_of tree Buffer.empty) end;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    94
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    95
(** XML parsing **)
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    96
19089
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
    97
fun beginning n xs = Symbol.beginning n (Seq.take_at_most xs n)
19064
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    98
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
    99
fun err s xs =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   100
  "XML parsing error: " ^ s ^ "\nfound: " ^ quote (beginning 100 xs) ;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   101
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   102
val scan_whspc = Scan.any Symbol.is_blank;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   103
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   104
val scan_special = $$ "&" ^^ scan_id ^^ $$ ";" >> decode;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   105
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   106
val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   107
  (scan_special || Scan.one Symbol.not_eof)) >> implode;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   108
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   109
val parse_cdata = Scan.this_string "<![CDATA[" |--
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   110
  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.not_eof)) >>
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   111
    implode) --| Scan.this_string "]]>";
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   112
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   113
val parse_att =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   114
    scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   115
    (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   116
    (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ s) >> snd);
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   117
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   118
val parse_comment = Scan.this_string "<!--" --
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   119
  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.not_eof)) --
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   120
  Scan.this_string "-->";
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   121
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   122
val scan_comment_whspc = 
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   123
    (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   124
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   125
val parse_pi = Scan.this_string "<?" |--
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   126
  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.not_eof)) --|
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   127
  Scan.this_string "?>";
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   128
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   129
fun parse_content xs =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   130
  ((Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) [] --
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   131
    (Scan.repeat ((* scan_whspc |-- *)
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   132
       (   parse_elem >> single
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   133
        || parse_cdata >> (single o Text)
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   134
        || parse_pi >> K []
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   135
        || parse_comment >> K []) --
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   136
       Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   137
         >> op @) >> List.concat) >> op @)(* --| scan_whspc*)) xs
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   138
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   139
and parse_elem xs =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   140
  ($$ "<" |-- scan_id --
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   141
    Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   142
      !! (err "Expected > or />")
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   143
        (Scan.this_string "/>" >> K []
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   144
         || $$ ">" |-- parse_content --|
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   145
            !! (err ("Expected </" ^ s ^ ">"))
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   146
              (Scan.this_string ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   147
    (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   148
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   149
val parse_document =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   150
  Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   151
    (Scan.repeat (Scan.unless ($$ ">")
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   152
      (Scan.one Symbol.not_eof)) >> implode) --| $$ ">" --| scan_whspc) --
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   153
  parse_elem;
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   154
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   155
fun tree_of_string s =
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   156
    let
19089
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   157
	val seq = Seq.fromString s
19064
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   158
	val scanner = !! (err "Malformed element") (scan_whspc |-- parse_elem --| scan_whspc)
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   159
	val (x, toks) = scanner seq
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   160
    in
19089
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   161
	if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
19064
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   162
    end
19089
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   163
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   164
(* More efficient saving and loading of xml trees employing a proprietary external format *)
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   165
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   166
fun write_lstring s buf = buf |> Buffer.add (string_of_int (size s)) |> Buffer.add " " |> Buffer.add s
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   167
fun parse_lstring toks = (scan_nat --| one Symbol.is_blank :-- (fn i => repeat_fixed i (one (K true))) >> snd >> implode) toks
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   168
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   169
fun write_list w l buf = buf |> Buffer.add (string_of_int (length l)) |> Buffer.add " " |> fold w l     
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   170
fun parse_list sc = scan_nat --| one Symbol.is_blank :-- (fn i => repeat_fixed i sc) >> snd
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   171
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   172
fun write_tree (Text s) buf = buf |> Buffer.add "T" |> write_lstring s
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   173
  | write_tree (Elem (name, attrs, children)) buf = 
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   174
    buf |> Buffer.add "E" 
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   175
	|> write_lstring name 
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   176
	|> write_list (fn (a,b) => fn buf => buf |> write_lstring a |> write_lstring b) attrs 
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   177
	|> write_list write_tree children
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   178
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   179
fun parse_tree toks = (one (K true) :-- (fn "T" => parse_lstring >> Text | "E" => parse_elem | _ => raise SyntaxError) >> snd) toks
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   180
and parse_elem toks = (parse_lstring -- parse_list (parse_lstring -- parse_lstring) -- parse_list parse_tree >> (fn ((n, a), c) => Elem (n,a,c))) toks
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   181
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   182
fun encoded_string_of_tree tree = Buffer.content (write_tree tree Buffer.empty)
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   183
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   184
fun tree_of_encoded_string s = 
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   185
    let
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   186
	fun print (a,b) = writeln (a^" "^(string_of_int b))
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   187
	val _ = print ("length of encoded string: ", size s)
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   188
	val _ = writeln "Seq.fromString..."
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   189
	val seq = timeit (fn () => Seq.fromString s)
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   190
	val  _ = print ("length of sequence", timeit (fn () => Seq.length seq))
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   191
	val scanner = !! (err "Malformed encoded xml") parse_tree
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   192
	val (x, toks) = scanner seq
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   193
    in
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   194
	if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   195
    end	       
2e487fe9593a improved scanning
obua
parents: 19064
diff changeset
   196
19064
bf19cc5a7899 fixed bugs, added caching
obua
parents:
diff changeset
   197
end;