src/Pure/Syntax/syntax.ML
changeset 39449 e3ac771235f7
parent 39409 4d701c0388c3
child 39541 f1ae2493d93f
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Sep 07 13:16:45 2010 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Sep 07 14:08:21 2010 +0200
     1.3 @@ -709,7 +709,8 @@
     1.4      val _ = List.app (Lexicon.report_token ctxt) toks;
     1.5  
     1.6      val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
     1.7 -    val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
     1.8 +    val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks)
     1.9 +      handle ERROR msg => (List.app (Lexicon.report_token_range ctxt) toks; error msg);
    1.10      val len = length pts;
    1.11  
    1.12      val limit = Config.get ctxt ambiguity_limit;