# HG changeset patch
# User wenzelm
# Date 1517395226 -3600
# Node ID 679253fef27751efa334571f1b25a80079094aff
# Parent  4a087b9a29c556c1fe6d6d08fbc09f3738676d31
clarified signature;

diff -r 4a087b9a29c5 -r 679253fef277 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Jan 31 11:26:50 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Wed Jan 31 11:40:26 2018 +0100
@@ -30,6 +30,8 @@
   val pos_of_token: token -> Position.T
   val end_pos_of_token: token -> Position.T
   val tokens_match_ord: token * token -> order
+  val literal: string -> token
+  val is_literal: token -> bool
   val is_proper: token -> bool
   val dummy: token
   val mk_eof: Position.T -> token
@@ -154,6 +156,9 @@
     (Literal, Literal) => fast_string_ord (apply2 str_of_token toks)
   | kinds => token_kind_ord kinds);
 
+fun literal s = Token (Literal, s, Position.no_range);
+fun is_literal tok = kind_of_token tok = Literal;
+
 val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true);
 
 val dummy = Token (Dummy, "", Position.no_range);
diff -r 4a087b9a29c5 -r 679253fef277 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Jan 31 11:26:50 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Wed Jan 31 11:40:26 2018 +0100
@@ -401,8 +401,10 @@
     val print_nt = tags_name tags;
     fun print_pri p = if p < 0 then "" else Symbol.make_sup ("(" ^ string_of_int p ^ ")");
 
-    fun pretty_symb (Terminal (Lexicon.Token (kind, s, _))) =
-          if kind = Lexicon.Literal then Pretty.quote (Pretty.keyword1 s) else Pretty.str s
+    fun pretty_symb (Terminal tok) =
+          if Lexicon.is_literal tok
+          then Pretty.quote (Pretty.keyword1 (Lexicon.str_of_token tok))
+          else Pretty.str (Lexicon.str_of_token tok)
       | pretty_symb (Nonterminal (tag, p)) = Pretty.str (print_nt tag ^ print_pri p);
 
     fun pretty_const "" = []
@@ -446,8 +448,7 @@
           nonterminals are converted to integer tags*)
         fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
           | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result =
-              symb_of ss nt_count tags
-                (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
+              symb_of ss nt_count tags (Terminal (Lexicon.literal s) :: result)
           | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result =
               let
                 val (nt_count', tags', new_symb) =
@@ -722,11 +723,12 @@
   let
     fun freeze a = map_range (curry Vector.sub a) (Vector.length a);
     val prods = maps (prods_content o #2) (freeze (#prods gram));
-    fun guess (SOME ([Nonterminal (_, k),
-            Terminal (Lexicon.Token (Lexicon.Literal, s, _)), Nonterminal (_, l)], _, j)) =
-          if k = j andalso l = j + 1 then SOME (s, true, false, j)
-          else if k = j + 1 then if l = j then SOME (s, false, true, j)
-            else if l = j + 1 then SOME (s, false, false, j)
+    fun guess (SOME ([Nonterminal (_, k), Terminal tok, Nonterminal (_, l)], _, j)) =
+          if Lexicon.is_literal tok then
+            if k = j andalso l = j + 1 then SOME (Lexicon.str_of_token tok, true, false, j)
+            else if k = j + 1 then if l = j then SOME (Lexicon.str_of_token tok, false, true, j)
+              else if l = j + 1 then SOME (Lexicon.str_of_token tok, false, false, j)
+              else NONE
             else NONE
           else NONE
       | guess _ = NONE;
diff -r 4a087b9a29c5 -r 679253fef277 src/Pure/Syntax/simple_syntax.ML
--- a/src/Pure/Syntax/simple_syntax.ML	Wed Jan 31 11:26:50 2018 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML	Wed Jan 31 11:40:26 2018 +0100
@@ -31,8 +31,9 @@
 
 (* basic scanners *)
 
-fun $$ s = Scan.some (fn Lexicon.Token (Lexicon.Literal, s', _) =>
-  if s = s' then SOME s else NONE | _ => NONE);
+fun $$ s =
+  Scan.some (fn tok =>
+    if Lexicon.is_literal tok andalso s = Lexicon.str_of_token tok then SOME s else NONE);
 
 fun enum1 s scan = scan ::: Scan.repeat ($$ s |-- scan);
 fun enum2 s scan = scan ::: Scan.repeat1 ($$ s |-- scan);