184 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)") |
184 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)") |
185 |> Context.theory_map; |
185 |> Context.theory_map; |
186 |
186 |
187 fun token_translation (txt, pos) = |
187 fun token_translation (txt, pos) = |
188 txt |> ML_Context.expression pos |
188 txt |> ML_Context.expression pos |
189 "val token_translation: (string * string * (string -> output * int)) list" |
189 "val token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list" |
190 "Context.map_theory (Sign.add_tokentrfuns token_translation)" |
190 "Context.map_theory (Sign.add_tokentrfuns token_translation)" |
191 |> Context.theory_map; |
191 |> Context.theory_map; |
192 |
192 |
193 end; |
193 end; |
194 |
194 |
600 |
600 |
601 fun string_of_prop state s = |
601 fun string_of_prop state s = |
602 let |
602 let |
603 val ctxt = Proof.context_of state; |
603 val ctxt = Proof.context_of state; |
604 val prop = Syntax.read_prop ctxt s; |
604 val prop = Syntax.read_prop ctxt s; |
605 in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt prop)) end; |
605 val ctxt' = Variable.auto_fixes prop ctxt; |
|
606 in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end; |
606 |
607 |
607 fun string_of_term state s = |
608 fun string_of_term state s = |
608 let |
609 let |
609 val ctxt = Proof.context_of state; |
610 val ctxt = Proof.context_of state; |
610 val t = Syntax.read_term ctxt s; |
611 val t = Syntax.read_term ctxt s; |
611 val T = Term.type_of t; |
612 val T = Term.type_of t; |
|
613 val ctxt' = Variable.auto_fixes t ctxt; |
612 in |
614 in |
613 Pretty.string_of |
615 Pretty.string_of |
614 (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk, |
616 (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk, |
615 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)]) |
617 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) |
616 end; |
618 end; |
617 |
619 |
618 fun string_of_type state s = |
620 fun string_of_type state s = |
619 let |
621 let |
620 val ctxt = Proof.context_of state; |
622 val ctxt = Proof.context_of state; |