read_asts: Lexicon.report_token, filter Lexicon.is_proper;
authorwenzelm
Fri Aug 15 15:51:04 2008 +0200 (2008-08-15)
changeset 27889c9e8a5bda32b
parent 27888 7ed38f1d11de
child 27890 62ac62e30ab1
read_asts: Lexicon.report_token, filter Lexicon.is_proper;
report tokens;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri Aug 15 15:51:02 2008 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Aug 15 15:51:04 2008 +0200
     1.3 @@ -481,11 +481,11 @@
     1.4  fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root (syms, pos) =
     1.5    let
     1.6      val {lexicon, gram, parse_ast_trtab, ...} = tabs;
     1.7 +    val toks = Lexicon.tokenize lexicon xids syms;
     1.8 +    val _ = List.app Lexicon.report_token toks;
     1.9 +
    1.10      val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
    1.11 -    val toks = Lexicon.tokenize lexicon xids syms;
    1.12 -    val _ = toks |> List.app (fn Lexicon.Token (Lexicon.Literal, _, (pos, _)) =>
    1.13 -      Position.report Markup.literal pos | _ => ());
    1.14 -    val pts = Parser.parse gram root' toks;
    1.15 +    val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
    1.16      val len = length pts;
    1.17  
    1.18      val limit = ! ambiguity_limit;