src/Pure/PIDE/xml.ML
changeset 48769 e3b7087bb923
parent 47199 15ede9f1da3f
child 49599 e716209814b3
equal deleted inserted replaced
48768:abc45de5bb22 48769:e3b7087bb923
   222 
   222 
   223 fun parse s =
   223 fun parse s =
   224   (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
   224   (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
   225       (blanks |-- parse_document --| blanks))) (raw_explode s) of
   225       (blanks |-- parse_document --| blanks))) (raw_explode s) of
   226     (x, []) => x
   226     (x, []) => x
   227   | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
   227   | (_, ys) => error ("XML parsing error: unprocessed input\n" ^ Symbol.beginning 100 ys));
   228 
   228 
   229 end;
   229 end;
   230 
   230 
   231 
   231 
   232 (** cache for substructural sharing **)
   232 (** cache for substructural sharing **)