aboutsummaryrefslogtreecommitdiffhomepage
path: root/demoisa
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-03-30 12:10:20 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-03-30 12:10:20 +0000
commitc193b1d3e1bbb52ebc8f6551c921ceb007019dea (patch)
treef5526b553aec685e8719ae64b456662f35594973 /demoisa
parent33028a27c20d47a6de7c5d53c0ba033b18833260 (diff)
Adjust proof-shell-annotated-prompt-regexp to match latest Isabelle versions
Diffstat (limited to 'demoisa')
-rw-r--r--demoisa/demoisa-easy.el8
-rw-r--r--demoisa/demoisa.el4
2 files changed, 8 insertions, 4 deletions
diff --git a/demoisa/demoisa-easy.el b/demoisa/demoisa-easy.el
index e0c91674..c9d1869f 100644
--- a/demoisa/demoisa-easy.el
+++ b/demoisa/demoisa-easy.el
@@ -15,8 +15,12 @@
;; using alternative architectures. It is still easy to augment
;; with additional elisp functions and other settings.
;;
+;; The most important setting is `proof-shell-annotated-prompt-regexp'
+;; used to recognize prompt texts from the prover.
+;;
;; See demoisa.el and the Adapting Proof General manual for more
-;; documentation.
+;; documentation. Please do read the documentation of the variables
+;; to understand how things work.
;;
;; To test this file you must rename it demoisa.el.
;;
@@ -47,7 +51,7 @@
proof-shell-end-goals-regexp "val it"
proof-shell-quit-cmd "quit();"
proof-assistant-home-page "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/"
- proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?ML>? "
+ proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?\\(ML\\)?> "
proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
proof-shell-init-cmd "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));"
proof-shell-proof-completed-regexp "^No subgoals!"
diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index 46c2f7b5..f9b75845 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -90,9 +90,9 @@
(defun demoisa-shell-config ()
"Configure Proof General shell for Isabelle."
(setq
- proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?ML>? "
+ proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?\\(ML\\)?> "
proof-shell-cd-cmd "cd \"%s\""
- proof-shell-prompt-pattern "[ML-=#>]+>? "
+ proof-shell-prompt-pattern "([ML-=#>]+>? "
proof-shell-interrupt-regexp "Interrupt"
proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
proof-shell-start-goals-regexp "Level [0-9]"