51 Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw; |
51 Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw; |
52 |
52 |
53 end; |
53 end; |
54 |
54 |
55 |
55 |
56 (* token translations *) |
|
57 |
|
58 local |
|
59 |
|
60 fun end_tag () = special "350"; |
|
61 val class_tag = ("class", fn () => special "351"); |
|
62 val tfree_tag = ("tfree", fn () => special "352"); |
|
63 val tvar_tag = ("tvar", fn () => special "353"); |
|
64 val free_tag = ("free", fn () => special "354"); |
|
65 val bound_tag = ("bound", fn () => special "355"); |
|
66 val var_tag = ("var", fn () => special "356"); |
|
67 val skolem_tag = ("skolem", fn () => special "357"); |
|
68 |
|
69 fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x]; |
|
70 |
|
71 fun tagit (kind, bg_tag) x = |
|
72 (bg_tag () ^ x ^ end_tag (), Symbol.length (Symbol.explode x)); |
|
73 |
|
74 fun free_or_skolem x = |
|
75 (case try Name.dest_skolem x of |
|
76 NONE => tagit free_tag x |
|
77 | SOME x' => tagit skolem_tag x'); |
|
78 |
|
79 fun var_or_skolem s = |
|
80 (case Lexicon.read_variable s of |
|
81 SOME (x, i) => |
|
82 (case try Name.dest_skolem x of |
|
83 NONE => tagit var_tag s |
|
84 | SOME x' => tagit skolem_tag |
|
85 (setmp show_question_marks true Term.string_of_vname (x', i))) |
|
86 | NONE => tagit var_tag s); |
|
87 |
|
88 val proof_general_trans = |
|
89 Syntax.tokentrans_mode proof_generalN |
|
90 [("class", tagit class_tag), |
|
91 ("tfree", tagit tfree_tag), |
|
92 ("tvar", tagit tvar_tag), |
|
93 ("free", free_or_skolem), |
|
94 ("bound", tagit bound_tag), |
|
95 ("var", var_or_skolem)]; |
|
96 |
|
97 in |
|
98 |
|
99 val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans)); |
|
100 |
|
101 end; |
|
102 |
|
103 |
|
104 (* common markup *) |
56 (* common markup *) |
105 |
57 |
106 fun proof_general_markup (name, props) = |
58 val _ = Markup.add_mode proof_generalN (fn (name, props) => |
107 let |
59 let |
108 val (bg1, en1) = |
60 val (bg1, en1) = |
109 if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367") |
61 if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367") |
110 else if name = Markup.sendbackN then (special "376", special "377") |
62 else if name = Markup.sendbackN then (special "376", special "377") |
111 else if name = Markup.hiliteN then (special "327", special "330") |
63 else if name = Markup.hiliteN then (special "327", special "330") |
|
64 else if name = Markup.classN then (special "351", special "350") |
|
65 else if name = Markup.tfreeN then (special "352", special "350") |
|
66 else if name = Markup.tvarN then (special "353", special "350") |
|
67 else if name = Markup.freeN then (special "354", special "350") |
|
68 else if name = Markup.boundN then (special "355", special "350") |
|
69 else if name = Markup.varN then (special "356", special "350") |
|
70 else if name = Markup.skolemN then (special "357", special "350") |
112 else ("", ""); |
71 else ("", ""); |
113 val (bg2, en2) = |
72 val (bg2, en2) = |
114 if print_mode_active test_markupN |
73 if print_mode_active test_markupN |
115 then XML.output_markup (name, props) |
74 then XML.output_markup (name, props) |
116 else ("", ""); |
75 else ("", ""); |
117 in (bg1 ^ bg2, en2 ^ en1) end; |
76 in (bg1 ^ bg2, en2 ^ en1) end); |
118 |
|
119 val _ = Markup.add_mode proof_generalN proof_general_markup; |
|
120 |
77 |
121 |
78 |
122 (* messages and notification *) |
79 (* messages and notification *) |
123 |
80 |
124 fun decorate bg en prfx = |
81 fun decorate bg en prfx = |