98 |
98 |
99 |
99 |
100 (* common markup *) |
100 (* common markup *) |
101 |
101 |
102 fun proof_general_markup (name, props) = |
102 fun proof_general_markup (name, props) = |
103 (if name = Markup.promptN then ("", special "372") |
103 let |
104 else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367") |
104 val (bg1, en1) = |
105 else if name = Markup.sendbackN then (special "376", special "377") |
105 if name = Markup.promptN then ("", special "372") |
106 else if name = Markup.hiliteN then (special "327", special "330") |
106 else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367") |
107 else ("", "")) |
107 else if name = Markup.sendbackN then (special "376", special "377") |
108 |> (name <> Markup.promptN andalso print_mode_active IsabelleProcess.test_markupN) ? |
108 else if name = Markup.hiliteN then (special "327", special "330") |
109 (fn (bg1, en1) => |
109 else ("", ""); |
110 let val (bg2, en2) = IsabelleProcess.test_markup (name, props) |
110 val (bg2, en2) = |
111 in (bg1 ^ bg2, en2 ^ en1) end); |
111 if name <> Markup.promptN andalso print_mode_active IsabelleProcess.test_markupN |
|
112 then IsabelleProcess.test_markup (name, props) |
|
113 else ("", ""); |
|
114 in (bg1 ^ bg2, en2 ^ en1) end; |
112 |
115 |
113 val _ = Markup.add_mode proof_generalN proof_general_markup; |
116 val _ = Markup.add_mode proof_generalN proof_general_markup; |
114 |
117 |
115 |
118 |
116 (* messages and notification *) |
119 (* messages and notification *) |