diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2000-03-19 06:44:31 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-19 06:44:31 +0000 |
commit | 515f9da2eace774e55f76789ff7a2697358ab336 (patch) | |
tree | d9875f9d19eed1e316fff77e356a4f47cf3e73cb /hol98 | |
parent | 47316e151054edd69f98382a6a4b21345d3f78ef (diff) |
More reliable prompt regexp
Diffstat (limited to 'hol98')
-rw-r--r-- | hol98/hol98.el | 8 |
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 |