equal
deleted
inserted
replaced
98 |
98 |
99 (* common markup *) |
99 (* common markup *) |
100 |
100 |
101 fun proof_general_markup (name, props) = |
101 fun proof_general_markup (name, props) = |
102 (if name = Markup.promptN then ("", special "372") |
102 (if name = Markup.promptN then ("", special "372") |
103 else if name = Markup.no_stateN orelse name = Markup.stateN |
103 else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367") |
104 then (special "366" ^ "\n", "\n" ^ special "367") |
|
105 else ("", "")) |
104 else ("", "")) |
106 |> (name <> Markup.promptN andalso print_mode_active "test_markup") ? |
105 |> (name <> Markup.promptN andalso print_mode_active "test_markup") ? |
107 (fn (bg, en) => |
106 (fn (bg, en) => |
108 (bg ^ enclose "<" ">" (space_implode " " (name :: map XML.attribute props)), |
107 (bg ^ enclose "<" ">" (space_implode " " (name :: map XML.attribute props)), |
109 enclose "</" ">" name ^ en)); |
108 enclose "</" ">" name ^ en)); |
110 |
109 |
111 val _ = Pretty.add_mode proof_generalN Pretty.default_indent proof_general_markup; |
110 val _ = Markup.add_mode proof_generalN proof_general_markup; |
112 |
111 |
113 |
112 |
114 (* messages and notification *) |
113 (* messages and notification *) |
115 |
114 |
116 fun decorate bg en prfx = |
115 fun decorate bg en prfx = |