eliminate use of Thy_Info 12: prep.arg. ctxt in TermC, UnparseC
1 (* Title: BaseDefinitions/unparseC.sml
2 Author: Walther Neuper 2018
3 (c) copyright due to lincense terms
6 signature UNPARSE_ISAC =
13 (*val term: Proof.context -> term -> term_as_string *)
14 val term_in_ctxt: Proof.context -> term -> term_as_string
15 val term: term -> term_as_string
17 val term_in_thy: theory -> term -> term_as_string
19 (*val term_opt: Proof.context -> term option -> term_as_string *)
20 val term_opt: term option -> term_as_string
22 val terms: term list -> term_as_string
24 val terms_in_ctxt: Proof.context -> term list -> term_as_string
26 val terms_in_thy: theory -> term list -> term_as_string
28 (*val terms_short: Proof.context -> term list -> term_as_string*)
29 val terms_short: term list -> term_as_string
30 (*val typ: Proof.context -> typ -> term_as_string*)
31 val typ_in_ctxt: Proof.context -> typ -> term_as_string
34 val term_by_thyID: ThyC.id -> term -> term_as_string
35 val terms_to_strings: term list -> term_as_string list
40 structure UnparseC(**): UNPARSE_ISAC(**) =
44 type term_as_string = string;
46 fun term_in_ctxt ctxt t =
48 val ctxt' = Config.put show_markup false ctxt;
50 Print_Mode.setmp [] (Syntax.string_of_term ctxt') t
52 fun terms_in_ctxt ctxt ts = ts |> map (term_in_ctxt ctxt) |> strs2str';
56 fun term_by_thyID thyID t =
58 val ctxt' = Config.put show_markup false (Proof_Context.init_global
59 (ThyC.get_theory thyID));
61 Print_Mode.setmp [] (Syntax.string_of_term ctxt') t
65 fun term t = term_in_ctxt (ThyC.id_to_ctxt "Isac_Knowledge") t;
66 fun term_in_thy thy t = term_in_ctxt (Proof_Context.init_global thy) t;
67 fun terms_in_thy thy ts = ts |> map (term_in_thy thy) |> strs2str';
68 fun terms_to_strings ts = map term ts; (* terms_to_strings [t1,t2] = ["1 + 2", "abc"]; *)
69 val terms = strs2str o terms_to_strings; (* terms [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
71 val terms_short = strs2str' o terms_to_strings; (* terms_short [t1,t2] = "[1 + 2,abc]"; *)
72 fun term_opt (SOME t) = "(SOME " ^ term t ^ ")"
73 | term_opt NONE = "NONE";
75 fun type_to_string' ctxt typ =
76 Print_Mode.setmp [] (Syntax.string_of_typ ctxt) typ
77 fun typ_in_ctxt ctxt typ = type_to_string' ctxt typ
79 val typ_empty = Type ("empty", []);
80 val term_empty = Const ("empty", Type("'a", []));