# HG changeset patch
# User wenzelm
# Date 1208442651 -7200
# Node ID 334d3fa649eab8d20c649962a1a44366440c6ad4
# Parent  51ee753cc2e3cf17d44481dd99d1269c41adb57c
default token translations with proper markup;

diff -r 51ee753cc2e3 -r 334d3fa649ea src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Apr 17 16:30:50 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 17 16:30:51 2008 +0200
@@ -370,6 +370,45 @@
   in reverts end;
 
 
+(* default token translations *)
+
+local
+
+fun free_or_skolem ctxt x =   (* FIXME revert skolem *)
+  (case try Name.dest_skolem x of
+    NONE => Pretty.mark Markup.free (Pretty.str x)
+  | SOME x' => Pretty.mark Markup.skolem (Pretty.str x'))
+  |> Pretty.mark (if Variable.is_fixed ctxt x then Markup.fixed x else Markup.hilite);
+
+fun var_or_skolem _ s =
+  (case Lexicon.read_variable s of
+    SOME (x, i) =>
+      (case try Name.dest_skolem x of
+        NONE => Pretty.mark Markup.var (Pretty.str s)
+      | SOME x' => Pretty.mark Markup.skolem
+          (Pretty.str (setmp show_question_marks true Term.string_of_vname (x', i))))
+  | NONE => Pretty.mark Markup.var (Pretty.str s));
+
+fun class_markup _ c =    (* FIXME authentic name *)
+  Pretty.mark (Markup.classN, []) (Pretty.str c);
+
+fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
+
+val token_trans =
+ Syntax.tokentrans_mode ""
+  [("class", class_markup),
+   ("tfree", plain_markup Markup.tfree),
+   ("tvar", plain_markup Markup.tvar),
+   ("free", free_or_skolem),
+   ("bound", plain_markup Markup.bound),
+   ("var", var_or_skolem),
+   ("num", plain_markup Markup.num),
+   ("xnum", plain_markup Markup.xnum),
+   ("xstr", plain_markup Markup.xstr)];
+
+in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end;
+
+
 
 (** prepare terms and propositions **)