read_asts: report literal tokens;
authorwenzelm
Sat, 09 Aug 2008 12:28:13 +0200
changeset 278084dd3d5efcc7f
parent 27807 851a1dfb7828
child 27809 a1e409db516b
read_asts: report literal tokens;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Aug 09 12:28:12 2008 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Aug 09 12:28:13 2008 +0200
     1.3 @@ -481,7 +481,10 @@
     1.4    let
     1.5      val {lexicon, gram, parse_ast_trtab, ...} = tabs;
     1.6      val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
     1.7 -    val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids syms);
     1.8 +    val toks = Lexicon.tokenize lexicon xids syms;
     1.9 +    val _ = toks |> List.app (fn Lexicon.Token (Lexicon.Literal, _, (pos, _)) =>
    1.10 +      Position.report Markup.literal pos | _ => ());
    1.11 +    val pts = Parser.parse gram root' toks;
    1.12      val len = length pts;
    1.13  
    1.14      val limit = ! ambiguity_limit;