From e1a327e5621d191fe408d12b331d05dda17b395c Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 27 Aug 2010 16:32:16 +0000 Subject: Replace proof-terminal-char with proof-terminal-string. --- obsolete/demoisa/demoisa-easy.el | 48 ++++++++++++++++++++-------------------- obsolete/demoisa/demoisa.el | 32 +++++++++++++-------------- obsolete/lclam/lclam.el | 33 +++++++++++++-------------- obsolete/plastic/plastic.el | 10 +++++---- 4 files changed, 63 insertions(+), 60 deletions(-) (limited to 'obsolete') 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") diff --git a/obsolete/demoisa/demoisa.el b/obsolete/demoisa/demoisa.el index ffaa21b1..5254e97e 100644 --- a/obsolete/demoisa/demoisa.el +++ b/obsolete/demoisa/demoisa.el @@ -27,7 +27,7 @@ ;; ;; To make the line above take precedence over the real Isabelle mode ;; later in the table, set PROOFGENERAL_ASSISTANTS=demoisa in the -;; shell before starting Emacs (or customize proof-assistants). +;; shell before starting Emacs (or customize proof-assistants). ;; (require 'proof) ; load generic parts @@ -43,7 +43,7 @@ ;; proof-site provides us with two customization groups ;; automatically: (based on the name of the assistant) ;; -;; 'isabelledemo - User options for Isabelle Demo Proof General +;; 'isabelledemo - User options for Isabelle Demo Proof General ;; 'isabelledemo-config - Configuration of Isabelle Proof General ;; (constants, but may be nice to tweak) ;; @@ -72,14 +72,14 @@ (defun demoisa-config () "Configure Proof General scripting for Isabelle." (setq - proof-terminal-char ?\; ; ends every command - 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-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-undo-n-times-cmd "pg_repeat undo %s;" proof-showproof-command "pr()" proof-goal-command "Goal \"%s\";" @@ -87,21 +87,21 @@ proof-kill-goal-command "Goal \"PROP no_goal_set\";" proof-assistant-home-page isabelledemo-web-page proof-prog-name isabelledemo-prog-name - proof-auto-multiple-files t)) + proof-auto-multiple-files t)) (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-interrupt-regexp "Interrupt" + proof-shell-interrupt-regexp "Interrupt" proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " proof-shell-start-goals-regexp "Level [0-9]" proof-shell-end-goals-regexp "val it" - proof-shell-proof-completed-regexp "^No subgoals!" - proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" - proof-shell-init-cmd ; define a utility function, in a lib somewhere? + proof-shell-proof-completed-regexp "^No subgoals!" + proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" + proof-shell-init-cmd ; define a utility function, in a lib somewhere? "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));" proof-shell-quit-cmd "quit();")) diff --git a/obsolete/lclam/lclam.el b/obsolete/lclam/lclam.el index ae171aa0..0472b6a0 100644 --- a/obsolete/lclam/lclam.el +++ b/obsolete/lclam/lclam.el @@ -32,9 +32,9 @@ (defun lclam-config () "Configure Proof General scripting for Lambda-CLAM." (setq - proof-terminal-char ?\. - proof-comment-start "/*" - proof-comment-end "*/" + proof-terminal-string "." + proof-script-comment-start "/*" + proof-script-comment-end "*/" proof-goal-command-regexp "^pds_plan" proof-save-command-regexp nil proof-goal-with-hole-regexp nil @@ -45,7 +45,7 @@ proof-goal-command "^pds_plan %s." proof-save-command nil proof-kill-goal-command nil - proof-assistant-homepage lclam-web-page + proof-assistant-home-page lclam-web-page proof-auto-multiple-files nil )) @@ -54,7 +54,6 @@ (setq proof-shell-annotated-prompt-regexp "^lclam:" proof-shell-cd-cmd nil - proof-shell-prompt-pattern nil proof-shell-interrupt-regexp nil proof-shell-error-regexp nil proof-shell-start-goals-regexp nil @@ -123,16 +122,18 @@ ;; Remove redundant toolbar buttons -(setq lclam-toolbar-entries - (remassoc 'state lclam-toolbar-entries)) -(setq lclam-toolbar-entries - (remassoc 'context lclam-toolbar-entries)) -(setq lclam-toolbar-entries - (remassoc 'undo lclam-toolbar-entries)) -(setq lclam-toolbar-entries - (remassoc 'retract lclam-toolbar-entries)) -(setq lclam-toolbar-entries - (remassoc 'qed lclam-toolbar-entries)) +(eval-after-load "pg-custom" +'(progn + (setq lclam-toolbar-entries + (remassoc 'state lclam-toolbar-entries)) + (setq lclam-toolbar-entries + (remassoc 'context lclam-toolbar-entries)) + (setq lclam-toolbar-entries + (remassoc 'undo lclam-toolbar-entries)) + (setq lclam-toolbar-entries + (remassoc 'retract lclam-toolbar-entries)) + (setq lclam-toolbar-entries + (remassoc 'qed lclam-toolbar-entries)))) ;; ;; ============ Theory file mode ============== @@ -197,7 +198,7 @@ (proof-shell-invisible-command (proof-format-filename ;; %r parameter means relative (don't expand) path - (format "use_thy \"%%r\"." (if try "try_" "")) + (format "use_thy \"%s%%r\"." (if try "try_" "")) (file-name-nondirectory file)) wait)) diff --git a/obsolete/plastic/plastic.el b/obsolete/plastic/plastic.el index 3461dbb8..f19b7006 100644 --- a/obsolete/plastic/plastic.el +++ b/obsolete/plastic/plastic.el @@ -213,7 +213,8 @@ (defun plastic-count-undos (span) "This is how to work out what the undo commands are. Given is the first SPAN which needs to be undone." - (let ((ct 0) string i) + (let ((ct 0) string i + (tl (length proof-terminal-string))) (while span (setq string (span-property span 'cmd)) (plastic-preprocessing) ;; dynamic scope, on string @@ -225,7 +226,8 @@ Given is the first SPAN which needs to be undone." ((eq (span-property span 'type) 'pbp) (setq i 0) (while (< i (length string)) - (if (= (aref string i) proof-terminal-char) (setq ct (+ 1 ct))) + (if (string-equal (substring string i (+ i tl)) proof-terminal-string) + (incf ct)) (setq i (+ 1 i))))) (setq span (next-span span 'type))) (list (concat plastic-lit-string @@ -344,7 +346,7 @@ Given is the first SPAN which needs to be undone." (defun plastic-mode-config () - (setq proof-terminal-char ?\;) + (setq proof-terminal-string ";") (setq proof-script-comment-start "(*") ;; these still active (setq proof-script-comment-end "*)") @@ -421,7 +423,7 @@ Given is the first SPAN which needs to be undone." (add-hook 'proof-shell-insert-hook 'plastic-preprocessing) ;; (add-hook 'proof-shell-handle-error-or-interrupt-hook -;; (lambda()(goto-char (search-forward (char-to-string proof-terminal-char))))) +;; (lambda()(goto-char (search-forward (regexp-quote proof-terminal-char))))) ;; (add-hook 'proof-shell-handle-delayed-output-hook `plastic-show-shell-buffer t) ;; this forces display of shell-buffer after each cmd, rather than goals-buffer -- cgit v1.2.3