# HG changeset patch
# User wenzelm
# Date 1218233379 -7200
# Node ID c08f4ea29b833655c0be16766dbbdc413d785d3b
# Parent  1eddcd7dda2d04bf8603960f5ddbb2a273e841b7
read_token: more robust handling of empty text;

diff -r 1eddcd7dda2d -r c08f4ea29b83 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Aug 09 00:09:38 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Aug 09 00:09:39 2008 +0200
@@ -461,13 +461,11 @@
 
 fun read_token str =
   let val (text, pos) =
-    if YXML.detect str then
-      (case YXML.parse str of
-        XML.Elem ("token", props, [XML.Text text]) =>
-          let val pos = Position.of_properties props;
-          in (text, pos) end
-      | _ => (str, Position.none))
-    else (str, Position.none)
+    (case YXML.parse str handle Fail msg => error msg of
+      XML.Elem ("token", props, [XML.Text text]) => (text, Position.of_properties props)
+    | XML.Elem ("token", props, []) => ("", Position.of_properties props)
+    | XML.Text text => (text, Position.none)
+    | _ => (str, Position.none))
   in (SymbolPos.explode (text, pos), pos) end;