Removed use of proof-terminal-string, added explicit terminators everywhere.

2 files changed, 25 insertions, 34 deletions

diff --git a/coq/coq.el b/coq/coq.el
index c28216d9..5dbc9704 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -77,7 +77,7 @@
   "*The prompt pattern for the inferior shell running coq.")
 
 ;; FIXME da: this was disabled (set to nil) -- why?
-(defvar coq-shell-cd "Cd \"%s\""
+(defvar coq-shell-cd "Cd \"%s\"."
   "*Command of the inferior process to change the directory.") 
 
 (defvar coq-shell-abort-goal-regexp "Current goal aborted"
@@ -102,7 +102,7 @@
 (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp)
 
 (defconst coq-kill-goal-command "Abort.")
-(defconst coq-forget-id-command "Reset ")
+(defconst coq-forget-id-command "Reset %s.")
 
 (defconst coq-undoable-commands-regexp (proof-ids-to-regexp coq-tactics))
 
@@ -148,7 +148,7 @@
 	     (not (eq (span-property (prev-span span 'type) 'type) 'comment))
 	     (coq-goal-command-p
 	      (span-property (prev-span span 'type) 'cmd)))
-	(concat "Restart" proof-terminal-string)
+	"Restart."
       (while span
 	(setq str (span-property span 'cmd))
 	(cond ((eq (span-property span 'type) 'vanilla)
@@ -163,7 +163,7 @@
 			(setq i (+ 1 i))))
 		     (t nil))))
 	(setq span (next-span span 'type)))
-      (concat "Undo " (int-to-string ct) proof-terminal-string))))
+      (concat "Undo " (int-to-string ct) "."))))
 
 (defconst coq-keywords-decl-defn-regexp
   (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-defn))
@@ -197,8 +197,7 @@
 	;; identifier "Unnamed_thm", though!  So we don't need
 	;; this test:
 	;; (unless (eq (span-property span 'name) proof-unnamed-theorem-name)
-	(setq ans (concat coq-forget-id-command
-			  (span-property span 'name) proof-terminal-string)))
+	(setq ans (format coq-forget-id-command (span-property span 'name))))
 
        ((proof-string-match (concat "\\`\\(" coq-keywords-decl-defn-regexp
 				    "\\)\\s-*\\(" proof-id 
@@ -213,16 +212,14 @@
 				    ;; Section .. End Section should be
 				    ;; atomic!
 				    "\\)\\s-*[\\[,:.]") str)
-	(setq ans (concat coq-forget-id-command
-			  (match-string 2 str) proof-terminal-string)))
+	(setq ans (format coq-forget-id-command (match-string 2 str))))
 
        ;; If it's not a goal but it contains "Definition" then it's a
        ;; declaration
        ((and (not (coq-goal-command-p str))
 	     (proof-string-match
 	      (concat "Definition\\s-+\\(" proof-id "\\)\\s-*:") str))
-	(setq ans (concat coq-forget-id-command
-			  (match-string 2 str) proof-terminal-string))))
+	(setq ans (format coq-forget-id-command (match-string 2 str)))))
 
       (setq span (next-span span 'type)))
 
@@ -290,7 +287,7 @@ This is specific to coq-mode."
     (proof-shell-ready-prover) 
     (setq cmd (read-string "SearchIsos: " nil 'proof-minibuffer-history))
     (proof-shell-invisible-command
-     (concat "SearchIsos " cmd proof-terminal-string))))
+     (format "SearchIsos %s." cmd))))
 
 (defun coq-end-Section ()
   "Ends a Coq section."
@@ -423,8 +420,8 @@ This is specific to coq-mode."
   (setq proof-guess-command-line 'coq-guess-command-line)
 
   ;; Commands sent to proof engine
-  (setq proof-showproof-command "Show"
-	proof-context-command "Print All"
+  (setq proof-showproof-command "Show."
+	proof-context-command "Print All."
 	proof-goal-command "Goal %s."
 	proof-save-command "Save %s."
 	proof-find-theorems-command "Search %s."
diff --git a/lego/lego.el b/lego/lego.el
index 1f700f5d..23dd5984 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -114,7 +114,7 @@ Activates extended printing routines required for Proof General.")
 (defvar lego-shell-prompt-pattern "^\\(Lego>[ \201]*\\)+"
   "*The prompt pattern for the inferior shell running lego.")
 
-(defvar lego-shell-cd "Cd \"%s\""
+(defvar lego-shell-cd "Cd \"%s\";"
   "*Command of the inferior process to change the directory.") 
 
 (defvar lego-shell-abort-goal-regexp 
@@ -131,7 +131,7 @@ Activates extended printing routines required for Proof General.")
   (concat "^" (proof-ids-to-regexp lego-keywords-goal)))
 
 (defvar lego-kill-goal-command "KillRef;")
-(defvar lego-forget-id-command "Forget ")
+(defvar lego-forget-id-command "Forget %s;")
 
 (defvar lego-undoable-commands-regexp
   (proof-ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal"
@@ -204,7 +204,8 @@ Given is the first SPAN which needs to be undone."
 	       (if (= (aref str i) proof-terminal-char) (setq ct (+ 1 ct)))
 	       (setq i (+ 1 i)))))
       (setq span (next-span span 'type)))
-    (concat "Undo " (int-to-string ct) proof-terminal-string)))
+    ;; FIXME: make this stuff generic.  This should be undo-n-times-cmd
+    (concat "Undo " (int-to-string ct) ";")))
 
 (defun lego-goal-command-p (str)
   "Decide whether argument is a goal or not"
@@ -221,33 +222,26 @@ Given is the first SPAN which needs to be undone."
 
        ((eq (span-property span 'type) 'goalsave)
 	(unless (eq (span-property span 'name) proof-unnamed-theorem-name)
-	  (setq ans (concat lego-forget-id-command
-			    (span-property span 'name) proof-terminal-string))))
-
+	  (setq ans (format lego-forget-id-command (span-property span 'name)))))
        ;; alternative definitions
        ((proof-string-match lego-definiendum-alternative-regexp str)
-	(setq ans (concat lego-forget-id-command (match-string 1 str)
-			  proof-terminal-string)))
+	(setq ans (format lego-forget-id-command (match-string 1 str))))
        ;; declarations
        ((proof-string-match (concat "\\`\\$?" (lego-decl-defn-regexp "[:|=]")) str)
 	(let ((ids (match-string 1 str))) ; returns "a,b"
 	  (proof-string-match proof-id ids)	; matches "a"
-	  (setq ans (concat lego-forget-id-command(match-string 1 ids)
-			    proof-terminal-string))))
+	  (setq ans (format lego-forget-id-command (match-string 1 ids)))))
 	   
        ((proof-string-match "\\`\\(Inductive\\|\\Record\\)\\s-*\\[\\s-*\\w+\\s-*:[^;]+\\`Parameters\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str)
-	(setq ans (concat lego-forget-id-command
-			  (match-string 2 str) proof-terminal-string)))
+	(setq ans (format lego-forget-id-command (match-string 2 str))))
 
        ((proof-string-match 
 	 "\\`\\(Inductive\\|Record\\)\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str)
 	(setq ans 
-	      (concat lego-forget-id-command (match-string 2 str)
-		      proof-terminal-string)))
+	      (format lego-forget-id-command (match-string 2 str))))
        
        ((proof-string-match "\\`\\s-*Module\\s-+\\(\\S-+\\)\\W" str)
-	(setq ans (concat "ForgetMark " (match-string 1 str) 
-			  proof-terminal-string))))
+	(setq ans (format "ForgetMark %s;" (match-string 1 str)))))
       ;; Carry on searching forward for something to forget
       ;; (The first thing to be forget will forget everything following)
       (setq span (next-span span 'type)))
@@ -344,11 +338,11 @@ Checks the width in the `proof-goals-buffer'"
   
   (setq proof-mode-for-script 'lego-mode)
 
-  (setq proof-showproof-command "Prf"
+  (setq proof-showproof-command "Prf;"
 	proof-goal-command "Goal %s;"
 	proof-save-command "Save %s;"
-	proof-context-command "Ctxt"
-	proof-info-command "Help")
+	proof-context-command "Ctxt;"
+	proof-info-command "Help;")
 
   (setq proof-goal-command-p 'lego-goal-command-p
 	proof-completed-proof-behaviour 'closeany ; new in 3.0
@@ -369,8 +363,8 @@ Checks the width in the `proof-goals-buffer'"
   (lego-init-syntax-table)
 
   ;; da: I've moved these out of proof-config-done in proof-script.el 
-  (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string))
-  (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string))
+  (setq pbp-goal-command "Pbp %s;")
+  (setq pbp-hyp-command "PbpHyp %s;")
 
 ;; font-lock