# HG changeset patch
# User wenzelm
# Date 1218277693 -7200
# Node ID 4dd3d5efcc7f73f0e815bf4e4fe302e754226921
# Parent  851a1dfb7828e59728d7329e2f094cecca1540ce
read_asts: report literal tokens;

diff -r 851a1dfb7828 -r 4dd3d5efcc7f src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Aug 09 12:28:12 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Aug 09 12:28:13 2008 +0200
@@ -481,7 +481,10 @@
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
     val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
-    val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids syms);
+    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 len = length pts;
 
     val limit = ! ambiguity_limit;