# HG changeset patch
# User wenzelm
# Date 1208442650 -7200
# Node ID 51ee753cc2e3cf17d44481dd99d1269c41adb57c
# Parent  c07b1a90600cb99999c9ce491754f9dca142a92f
token translations: context dependent, result Pretty.T;
string_of_term/prop: Variable.auto_fixes;

diff -r c07b1a90600c -r 51ee753cc2e3 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 17 16:30:48 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 17 16:30:50 2008 +0200
@@ -186,7 +186,7 @@
 
 fun token_translation (txt, pos) =
   txt |> ML_Context.expression pos
-    "val token_translation: (string * string * (string -> output * int)) list"
+    "val token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list"
       "Context.map_theory (Sign.add_tokentrfuns token_translation)"
   |> Context.theory_map;
 
@@ -602,17 +602,19 @@
   let
     val ctxt = Proof.context_of state;
     val prop = Syntax.read_prop ctxt s;
-  in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt prop)) end;
+    val ctxt' = Variable.auto_fixes prop ctxt;
+  in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
 
 fun string_of_term state s =
   let
     val ctxt = Proof.context_of state;
     val t = Syntax.read_term ctxt s;
     val T = Term.type_of t;
+    val ctxt' = Variable.auto_fixes t ctxt;
   in
     Pretty.string_of
-      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
+      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
   end;
 
 fun string_of_type state s =
diff -r c07b1a90600c -r 51ee753cc2e3 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Thu Apr 17 16:30:48 2008 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Thu Apr 17 16:30:50 2008 +0200
@@ -14,8 +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 -> output * int)) list ->
-    (string * string * (string -> output * int)) list
+  val tokentrans_mode:
+    string -> (string * (Proof.context -> string -> Pretty.T)) list ->
+    (string * string * (Proof.context -> string -> Pretty.T)) list
   val standard_token_classes: string list
 end;
 
@@ -49,7 +50,7 @@
         (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
       print_rules: (Ast.ast * Ast.ast) list,
       print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
-      token_translation: (string * string * (string -> output * int)) list}
+      token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list}
   val mfix_delims: string -> string list
   val mfix_args: string -> int
   val escape_mfix: string -> string
@@ -58,14 +59,14 @@
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
-    -> (string * string * (string -> output * int)) list
+    -> (string * string * (Proof.context -> string -> Pretty.T)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext: mfix list -> string list ->
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
-    -> (string * string * (string -> output * int)) list
+    -> (string * string * (Proof.context -> string -> Pretty.T)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext_const_names: string list -> syn_ext
   val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
@@ -79,7 +80,7 @@
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
-  val syn_ext_tokentrfuns: (string * string * (string -> output * int)) list -> syn_ext
+  val syn_ext_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> syn_ext
   val standard_token_markers: string list
   val pure_ext: syn_ext
 end;
@@ -334,7 +335,7 @@
       (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
     print_rules: (Ast.ast * Ast.ast) list,
     print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
-    token_translation: (string * string * (string -> output * int)) list};
+    token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list};
 
 
 (* syn_ext *)
diff -r c07b1a90600c -r 51ee753cc2e3 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Apr 17 16:30:48 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu Apr 17 16:30:50 2008 +0200
@@ -45,7 +45,8 @@
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
-  val extend_tokentrfuns: (string * string * (string -> output * int)) list -> syntax -> syntax
+  val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
+    syntax -> syntax
   val update_const_gram: (string -> bool) ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
   val remove_const_gram: (string -> bool) ->
@@ -239,7 +240,7 @@
     print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
     print_ruletab: ruletab,
     print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
-    tokentrtab: (string * (string * ((string -> output * int) * stamp)) list) list,
+    tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
     prtabs: Printer.prtabs} * stamp;
 
 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;