# HG changeset patch
# User wenzelm
# Date 1218808264 -7200
# Node ID c9e8a5bda32bd7e0a71874e2e678735f3f285f8b
# Parent  7ed38f1d11de57dcc2fa2f5116adc91ef962d87c
read_asts: Lexicon.report_token, filter Lexicon.is_proper;
report tokens;

diff -r 7ed38f1d11de -r c9e8a5bda32b src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Aug 15 15:51:02 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Aug 15 15:51:04 2008 +0200
@@ -481,11 +481,11 @@
 fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root (syms, pos) =
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
+    val toks = Lexicon.tokenize lexicon xids syms;
+    val _ = List.app Lexicon.report_token toks;
+
     val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
-    val toks = Lexicon.tokenize lexicon xids syms;
-    val _ = toks |> List.app (fn Lexicon.Token (Lexicon.Literal, _, (pos, _)) =>
-      Position.report Markup.literal pos | _ => ());
-    val pts = Parser.parse gram root' toks;
+    val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
     val len = length pts;
 
     val limit = ! ambiguity_limit;