diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-11-02 17:53:58 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-11-02 17:53:58 +0000 |
| commit | 8b1d33b2412c7bdd3a95c547661e844eea0cd4a4 (patch) | |
| tree | cc7e99d5cc2234c202fb504ba3a601fa11de281f /isa/ProofGeneral.ML | |
| parent | 69e63449c447a246a0e26486c2b6344972d187c4 (diff) | |
Changes suggested by Markus Wenzel
Diffstat (limited to 'isa/ProofGeneral.ML')
| -rw-r--r-- | isa/ProofGeneral.ML | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML index 9327496b..0cd50bf1 100644 --- a/isa/ProofGeneral.ML +++ b/isa/ProofGeneral.ML @@ -23,7 +23,7 @@ sig val retract_ML_file : string -> unit val retract_thy_file : string -> unit val repeat_undo : int -> unit -end +end; structure ProofGeneral = struct @@ -155,7 +155,7 @@ in warning_fn := (fn s => out ("\242" ^ (prefix_lines "###" s) ^ "\243")); error_fn := - (fn s => out ("\244" ^ (prefix_lines "###" s) ^ "\245"))) + (fn s => out ("\244" ^ (prefix_lines "***" s) ^ "\245"))) end; (* add specials to ml prompts *) @@ -176,15 +176,8 @@ local fun out s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); in - fun print_current_goals_with_plain_output i j t = - let - val curr_prs = !prs_fn - val _ = prs_fn := (fn s => out s) - val _ = (print_current_goals_default i j t) - handle e => (prs_fn := curr_prs; raise e) - in - prs_fn := curr_prs - end + fun print_current_goals_with_plain_output i j t = + Library.setmp prs_fn out (print_current_goals_default i j) t; end; print_current_goals_fn := print_current_goals_with_plain_output; |