aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol98
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-19 06:44:31 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-19 06:44:31 +0000
commit515f9da2eace774e55f76789ff7a2697358ab336 (patch)
treed9875f9d19eed1e316fff77e356a4f47cf3e73cb /hol98
parent47316e151054edd69f98382a6a4b21345d3f78ef (diff)
More reliable prompt regexp
Diffstat (limited to 'hol98')
-rw-r--r--hol98/hol98.el8
1 files changed, 5 insertions, 3 deletions
diff --git a/hol98/hol98.el b/hol98/hol98.el
index 68c7e09b..41f2f484 100644
--- a/hol98/hol98.el
+++ b/hol98/hol98.el
@@ -45,8 +45,10 @@
proof-assistant-home-page
"http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html"
proof-shell-annotated-prompt-regexp
- "^\\(> val it = () : unit\n\\)?- "
- proof-shell-error-regexp "^! "
+ "^- "
+ ;; This one is nice but less reliable, I think.
+ ;; "\\(> val it = () : unit\n\\)?- "
+ proof-shell-error-regexp "^! "
proof-shell-init-cmd
"Help.displayLines:=3000;
fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));"
@@ -63,7 +65,7 @@
;; proof-shell-eager-annotation-start
proof-find-theorems-command "DB.match [] (%s);"
- ;; We must set this to use ptys since mosml doesn't flush its output
+ ;; We must force this to use ptys since mosml doesn't flush its output
;; (on Linux, presumably on Solaris too).
proof-shell-process-connection-type t