# HG changeset patch
# User wenzelm
# Date 1218277691 -7200
# Node ID ece79c0597fe1f83fd643d40b62f524bd369fc0d
# Parent  2e533bcd13439aa8e37edfb6330475613fa89543
pos_of_token: Position.T;
removed unused display_token;
tuned;

diff -r 2e533bcd1343 -r ece79c0597fe src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat Aug 09 12:28:10 2008 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Aug 09 12:28:11 2008 +0200
@@ -41,6 +41,8 @@
   datatype token_kind =
     Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | XNumSy | StrSy | EOF
   datatype token = Token of token_kind * string * Position.range
+  val str_of_token: token -> string
+  val pos_of_token: token -> Position.T
   val mk_eof: Position.T -> token
   val eof: token
   val is_eof: token -> bool
@@ -52,9 +54,6 @@
   val tvarT: typ
   val terminals: string list
   val is_terminal: string -> bool
-  val str_of_token: token -> string
-  val pos_of_token: token -> string
-  val display_token: token -> string
   val matching_tokens: token * token -> bool
   val valued_token: token -> bool
   val predef_term: string -> token option
@@ -112,6 +111,9 @@
 
 datatype token = Token of token_kind * string * Position.range;
 
+fun str_of_token (Token (_, s, _)) = s;
+fun pos_of_token (Token (_, _, (pos, _))) = pos;
+
 
 (* stopper *)
 
@@ -137,27 +139,6 @@
 val is_terminal = member (op =) terminals;
 
 
-(* str_of_token *)
-
-fun str_of_token (Token (_, s, _)) = s;
-
-fun pos_of_token (Token (_, _, (pos, _))) = Position.str_of pos;
-
-
-(* display_token *)
-
-fun display_token (Token (Literal, s, _)) = quote s
-  | display_token (Token (IdentSy, s, _)) = "id(" ^ s ^ ")"
-  | display_token (Token (LongIdentSy, s, _)) = "longid(" ^ s ^ ")"
-  | display_token (Token (VarSy, s, _)) = "var(" ^ s ^ ")"
-  | display_token (Token (TFreeSy, s, _)) = "tid(" ^ s ^ ")"
-  | display_token (Token (TVarSy, s, _)) = "tvar(" ^ s ^ ")"
-  | display_token (Token (NumSy, s, _)) = "num(" ^ s ^ ")"
-  | display_token (Token (XNumSy, s, _)) = "xnum(" ^ s ^ ")"
-  | display_token (Token (StrSy, s, _)) = "xstr(" ^ s ^ ")"
-  | display_token (Token (EOF, _, _)) = "";
-
-
 (* matching_tokens *)
 
 fun matching_tokens (Token (Literal, x, _), Token (Literal, y, _)) = x = y
@@ -208,6 +189,7 @@
   | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
 
 
+
 (** tokenize **)
 
 fun token_leq (Token (_, s1, _), Token (_, s2, _)) = s1 <= s2;