diff options
Diffstat (limited to 'obsolete/demoisa/demoisa-easy.el')
| -rw-r--r-- | obsolete/demoisa/demoisa-easy.el | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/obsolete/demoisa/demoisa-easy.el b/obsolete/demoisa/demoisa-easy.el index 6631cebd..f2e84837 100644 --- a/obsolete/demoisa/demoisa-easy.el +++ b/obsolete/demoisa/demoisa-easy.el @@ -30,34 +30,34 @@ (proof-ready-for-assistant 'demoisa)) (require 'proof) -(require 'proof-easy-config) ; easy configure mechanism +(require 'proof-easy-config) ; easy configure mechanism (proof-easy-config 'demoisa "Isabelle Demo" - proof-prog-name "isabelle" - proof-terminal-char ?\; - proof-script-comment-start "(*" - proof-script-comment-end "*)" - proof-goal-command-regexp "^Goal" - proof-save-command-regexp "^qed" - proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" - proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" - proof-non-undoables-regexp "undo\\|back" - proof-goal-command "Goal \"%s\";" - proof-save-command "qed \"%s\";" - proof-kill-goal-command "Goal \"PROP no_goal_set\";" - proof-showproof-command "pr()" - proof-undo-n-times-cmd "pg_repeat undo %s;" - proof-auto-multiple-files t - proof-shell-cd-cmd "cd \"%s\"" - proof-shell-interrupt-regexp "Interrupt" - proof-shell-start-goals-regexp "Level [0-9]" - 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-prog-name "isabelle" + proof-terminal-string ";" + proof-script-comment-start "(*" + proof-script-comment-end "*)" + proof-goal-command-regexp "^Goal" + proof-save-command-regexp "^qed" + proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" + proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" + proof-non-undoables-regexp "undo\\|back" + proof-goal-command "Goal \"%s\";" + proof-save-command "qed \"%s\";" + proof-kill-goal-command "Goal \"PROP no_goal_set\";" + proof-showproof-command "pr()" + proof-undo-n-times-cmd "pg_repeat undo %s;" + proof-auto-multiple-files t + proof-shell-cd-cmd "cd \"%s\"" + proof-shell-interrupt-regexp "Interrupt" + proof-shell-start-goals-regexp "Level [0-9]" + 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-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-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!" proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading") |