diff options
| author | David Aspinall | 1998-10-12 12:54:46 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-10-12 12:54:46 +0000 |
| commit | eb55ebfc43b36a0af59625e68de644ade2717abc (patch) | |
| tree | 25e650a857bc11216f34d102e242f07b5600ebfe /isa/ProofGeneral.ML | |
| parent | f1221f3e544691d7b0971f007ce993c3fa3ae6a2 (diff) | |
Important regular expression fixes:
-error-regexp doesn't match warnings now.
-annotated-prompt-regexp doesn't match warnings now,
and is different from -prompt-regexp.
Diffstat (limited to 'isa/ProofGeneral.ML')
| -rw-r--r-- | isa/ProofGeneral.ML | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML index 100aa4ad..c47d11c4 100644 --- a/isa/ProofGeneral.ML +++ b/isa/ProofGeneral.ML @@ -30,11 +30,14 @@ in (*hooks for output channels: normal, warning, error*) -(* da: NO CHANGES NEEDED YET *) +(* Proof General: no change to these yet from defaults, but be + careful that proof-shell-prompt-pattern doesn't match any + of these! (maybe the default needs adjustment) +*) val () = (prs_fn := (fn s => out s); warning_fn := (fn s => out (prefix_lines "### " s)); - error_fn := (fn s => out (prefix_lines "*** " s))) + error_fn := (fn s => out (prefix_lines "*** " s))) end; |