equal
deleted
inserted
replaced
65 val promptN: string val prompt: T |
65 val promptN: string val prompt: T |
66 val stateN: string val state: T |
66 val stateN: string val state: T |
67 val subgoalN: string val subgoal: T |
67 val subgoalN: string val subgoal: T |
68 val sendbackN: string val sendback: T |
68 val sendbackN: string val sendback: T |
69 val hiliteN: string val hilite: T |
69 val hiliteN: string val hilite: T |
|
70 val unprocessedN: string val unprocessed: T |
|
71 val runningN: string val running: T |
|
72 val finishedN: string val finished: T |
|
73 val failedN: string val failed: T |
|
74 val disposedN: string val disposed: T |
70 val default_output: T -> output * output |
75 val default_output: T -> output * output |
71 val add_mode: string -> (T -> output * output) -> unit |
76 val add_mode: string -> (T -> output * output) -> unit |
72 val output: T -> output * output |
77 val output: T -> output * output |
73 val enclose: T -> output -> output |
78 val enclose: T -> output -> output |
74 val markup: T -> string -> string |
79 val markup: T -> string -> string |
192 val (subgoalN, subgoal) = markup_elem "subgoal"; |
197 val (subgoalN, subgoal) = markup_elem "subgoal"; |
193 val (sendbackN, sendback) = markup_elem "sendback"; |
198 val (sendbackN, sendback) = markup_elem "sendback"; |
194 val (hiliteN, hilite) = markup_elem "hilite"; |
199 val (hiliteN, hilite) = markup_elem "hilite"; |
195 |
200 |
196 |
201 |
|
202 (* command status *) |
|
203 |
|
204 val (unprocessedN, unprocessed) = markup_elem "unprocessed"; |
|
205 val (runningN, running) = markup_elem "running"; |
|
206 val (finishedN, finished) = markup_elem "finished"; |
|
207 val (failedN, failed) = markup_elem "failed"; |
|
208 val (disposedN, disposed) = markup_elem "disposed"; |
|
209 |
|
210 |
197 (* print mode operations *) |
211 (* print mode operations *) |
198 |
212 |
199 fun default_output (_: T) = ("", ""); |
213 fun default_output (_: T) = ("", ""); |
200 |
214 |
201 local |
215 local |