diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-03-30 12:10:20 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-03-30 12:10:20 +0000 |
| commit | c193b1d3e1bbb52ebc8f6551c921ceb007019dea (patch) | |
| tree | f5526b553aec685e8719ae64b456662f35594973 /demoisa | |
| parent | 33028a27c20d47a6de7c5d53c0ba033b18833260 (diff) | |
Adjust proof-shell-annotated-prompt-regexp to match latest Isabelle versions
Diffstat (limited to 'demoisa')
| -rw-r--r-- | demoisa/demoisa-easy.el | 8 | ||||
| -rw-r--r-- | demoisa/demoisa.el | 4 |
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]" |