src/Pure/Syntax/syntax.ML
changeset 27803 c08f4ea29b83
parent 27786 4525c6f5d753
child 27808 4dd3d5efcc7f
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Aug 09 00:09:38 2008 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Aug 09 00:09:39 2008 +0200
     1.3 @@ -461,13 +461,11 @@
     1.4  
     1.5  fun read_token str =
     1.6    let val (text, pos) =
     1.7 -    if YXML.detect str then
     1.8 -      (case YXML.parse str of
     1.9 -        XML.Elem ("token", props, [XML.Text text]) =>
    1.10 -          let val pos = Position.of_properties props;
    1.11 -          in (text, pos) end
    1.12 -      | _ => (str, Position.none))
    1.13 -    else (str, Position.none)
    1.14 +    (case YXML.parse str handle Fail msg => error msg of
    1.15 +      XML.Elem ("token", props, [XML.Text text]) => (text, Position.of_properties props)
    1.16 +    | XML.Elem ("token", props, []) => ("", Position.of_properties props)
    1.17 +    | XML.Text text => (text, Position.none)
    1.18 +    | _ => (str, Position.none))
    1.19    in (SymbolPos.explode (text, pos), pos) end;
    1.20  
    1.21