# HG changeset patch
# User wenzelm
# Date 1114278705 -7200
# Node ID fdf678bec5678449609d6c36eb7009031c0d209e
# Parent  a5166d054683d34ac975b4dc84cc3500af09dec8
added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);

diff -r a5166d054683 -r fdf678bec567 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Sat Apr 23 19:51:35 2005 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Sat Apr 23 19:51:45 2005 +0200
@@ -14,6 +14,9 @@
   val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
   val mk_trfun: string * 'a -> string * ('a * stamp)
   val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
+  val tokentrans_mode: string -> (string * (string -> string * real)) list ->
+    (string * string * (string -> string * real)) list
+  val standard_token_classes: string list
 end;
 
 signature SYN_EXT =
@@ -70,6 +73,7 @@
     (string * ((bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
+  val standard_token_markers: string list
   val pure_ext: syn_ext
 end;
 
@@ -365,6 +369,16 @@
 fun eq_trfun ((_, s1:stamp), (_, s2)) = s1 = s2;
 
 
+(* token translations *)
+
+fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
+
+val standard_token_classes =
+  ["class", "tfree", "tvar", "free", "bound", "var", "num", "xnum", "xstr"];
+
+val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
+
+
 (* pure_ext *)
 
 val pure_ext = syn_ext' false (K false)