equal
deleted
inserted
replaced
256 end; |
256 end; |
257 |
257 |
258 |
258 |
259 (* hooks *) |
259 (* hooks *) |
260 |
260 |
261 fun message bg en prfx text = |
261 fun message bg en prfx body = |
262 (case render text of |
262 (case render (implode body) of |
263 "" => () |
263 "" => () |
264 | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s))); |
264 | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s))); |
265 |
265 |
266 fun setup_messages () = |
266 fun setup_messages () = |
267 (Output.writeln_fn := message "" "" ""; |
267 (Output.writeln_fn := message "" "" ""; |
274 Output.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S"))); |
274 Output.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S"))); |
275 |
275 |
276 |
276 |
277 (* notification *) |
277 (* notification *) |
278 |
278 |
279 val emacs_notify = message (special "I") (special "J") ""; |
279 fun emacs_notify s = message (special "I") (special "J") "" [s]; |
280 |
280 |
281 fun tell_clear_goals () = |
281 fun tell_clear_goals () = |
282 emacs_notify "Proof General, please clear the goals buffer."; |
282 emacs_notify "Proof General, please clear the goals buffer."; |
283 |
283 |
284 fun tell_clear_response () = |
284 fun tell_clear_response () = |