default token translations with proper markup;
authorwenzelm
Thu Apr 17 16:30:51 2008 +0200 (2008-04-17 ago)
changeset 26705334d3fa649ea
parent 26704 51ee753cc2e3
child 26706 4ea64590d28b
default token translations with proper markup;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 17 16:30:50 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 17 16:30:51 2008 +0200
     1.3 @@ -370,6 +370,45 @@
     1.4    in reverts end;
     1.5  
     1.6  
     1.7 +(* default token translations *)
     1.8 +
     1.9 +local
    1.10 +
    1.11 +fun free_or_skolem ctxt x =   (* FIXME revert skolem *)
    1.12 +  (case try Name.dest_skolem x of
    1.13 +    NONE => Pretty.mark Markup.free (Pretty.str x)
    1.14 +  | SOME x' => Pretty.mark Markup.skolem (Pretty.str x'))
    1.15 +  |> Pretty.mark (if Variable.is_fixed ctxt x then Markup.fixed x else Markup.hilite);
    1.16 +
    1.17 +fun var_or_skolem _ s =
    1.18 +  (case Lexicon.read_variable s of
    1.19 +    SOME (x, i) =>
    1.20 +      (case try Name.dest_skolem x of
    1.21 +        NONE => Pretty.mark Markup.var (Pretty.str s)
    1.22 +      | SOME x' => Pretty.mark Markup.skolem
    1.23 +          (Pretty.str (setmp show_question_marks true Term.string_of_vname (x', i))))
    1.24 +  | NONE => Pretty.mark Markup.var (Pretty.str s));
    1.25 +
    1.26 +fun class_markup _ c =    (* FIXME authentic name *)
    1.27 +  Pretty.mark (Markup.classN, []) (Pretty.str c);
    1.28 +
    1.29 +fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
    1.30 +
    1.31 +val token_trans =
    1.32 + Syntax.tokentrans_mode ""
    1.33 +  [("class", class_markup),
    1.34 +   ("tfree", plain_markup Markup.tfree),
    1.35 +   ("tvar", plain_markup Markup.tvar),
    1.36 +   ("free", free_or_skolem),
    1.37 +   ("bound", plain_markup Markup.bound),
    1.38 +   ("var", var_or_skolem),
    1.39 +   ("num", plain_markup Markup.num),
    1.40 +   ("xnum", plain_markup Markup.xnum),
    1.41 +   ("xstr", plain_markup Markup.xstr)];
    1.42 +
    1.43 +in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end;
    1.44 +
    1.45 +
    1.46  
    1.47  (** prepare terms and propositions **)
    1.48