Replace proof-terminal-char with proof-terminal-string.

4 files changed, 63 insertions, 60 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")
 
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