equal
deleted
inserted
replaced
25 (*replace by ^^^*) |
25 (*replace by ^^^*) |
26 val terms_in_thy: theory -> term list -> term_as_string |
26 val terms_in_thy: theory -> term list -> term_as_string |
27 |
27 |
28 (*val terms_short: Proof.context -> 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 |
29 val terms_short: term list -> term_as_string |
30 |
|
31 (*val typ: Proof.context -> typ -> term_as_string*) |
30 (*val typ: Proof.context -> typ -> term_as_string*) |
32 val typ_in_ctxt: Proof.context -> typ -> term_as_string |
31 val typ_in_ctxt: Proof.context -> typ -> term_as_string |
33 val typ: typ -> term_as_string |
|
34 (*replace by ^^^*) |
|
35 val typ_by_thyID: ThyC.id -> typ -> term_as_string |
|
36 |
32 |
37 \<^isac_test>\<open> |
33 \<^isac_test>\<open> |
38 val term_by_thyID: ThyC.id -> term -> term_as_string |
34 val term_by_thyID: ThyC.id -> term -> term_as_string |
39 val terms_to_strings: term list -> term_as_string list |
35 val terms_to_strings: term list -> term_as_string list |
40 \<close> |
36 \<close> |
74 |
70 |
75 val terms_short = strs2str' o terms_to_strings; (* terms_short [t1,t2] = "[1 + 2,abc]"; *) |
71 val terms_short = strs2str' o terms_to_strings; (* terms_short [t1,t2] = "[1 + 2,abc]"; *) |
76 fun term_opt (SOME t) = "(SOME " ^ term t ^ ")" |
72 fun term_opt (SOME t) = "(SOME " ^ term t ^ ")" |
77 | term_opt NONE = "NONE"; |
73 | term_opt NONE = "NONE"; |
78 |
74 |
79 fun type_to_string'' (thyID : ThyC.id) t = |
|
80 let |
|
81 val ctxt' = Config.put show_markup false (Proof_Context.init_global |
|
82 (ThyC.get_theory thyID)) |
|
83 in |
|
84 Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t |
|
85 end; |
|
86 fun typ typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*) |
|
87 fun typ_by_thyID thy typ = type_to_string'' thy typ; (*legacy*) |
|
88 |
|
89 fun type_to_string' ctxt typ = |
75 fun type_to_string' ctxt typ = |
90 Print_Mode.setmp [] (Syntax.string_of_typ ctxt) typ |
76 Print_Mode.setmp [] (Syntax.string_of_typ ctxt) typ |
91 fun typ_in_ctxt ctxt typ = type_to_string' ctxt typ |
77 fun typ_in_ctxt ctxt typ = type_to_string' ctxt typ |
92 |
78 |
93 val typ_empty = Type ("empty", []); |
79 val typ_empty = Type ("empty", []); |