aboutsummaryrefslogtreecommitdiffhomepage
path: root/isa/ProofGeneral.ML
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-11-12 14:36:22 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-11-12 14:36:22 +0000
commit75441a61e232861c4536b94ca462d3783d6c27e8 (patch)
treef10ab2f9a94080b7d09672f839ad938da0859b58 /isa/ProofGeneral.ML
parentec827d606b8b1bff89d4fc894371e7911b1f2ff8 (diff)
Fixed error regexp
Diffstat (limited to 'isa/ProofGeneral.ML')
-rw-r--r--isa/ProofGeneral.ML4
1 files changed, 2 insertions, 2 deletions
diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 4036061c..1986422d 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -156,9 +156,9 @@ in
(prs_fn :=
(fn s => out ("\240" ^ s ^ "\241"));
warning_fn :=
- (fn s => out ("\242" ^ (prefix_lines "###" s) ^ "\243"));
+ (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 *)