More improvements/fixes for closing unfinished proofs.

Added proof-unnamed-theorem-name.

6 files changed, 41 insertions, 10 deletions

diff --git a/CHANGES b/CHANGES
index d5e9787d..8f1c4475 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,10 @@ Generic Changes
 * New function C-c C-f (proof-find) to invoke some prover-specific
   mechanism to search for theories.  
 
+* Whenever scripting is triggered in a new file, a cd command
+  is sent to the proof assistant to switch to the right directory
+  (in case other files are included).
+
 * [XEmacs only] Toolbar has six new buttons (State, Context, Info, 
   Command, Help, Stop) which invoke commands previously available on 
   keys/menus.   Also a new "Find" button for proof-find.
@@ -73,6 +77,13 @@ Coq Changes
   specific command C-c C-s (coq-Search).
 
 
+LEGO Changes
+------------
+
+* Proofs which have no save command are now closed off automatically
+  when a new goal is begun, mirroring the behaviour of LEGO.
+
+
 Isabelle and Isar Changes
 -------------------------
 
@@ -117,10 +128,16 @@ Internal changes for developers to note
   using special character codes is fragile and needs replacing
   in future versions of Proof General!
 
+* Proofs which are "unfinished", i.e. have no qed or result,
+  are now closed off automatically when a new goal is begun.
+  The new code only applies if proof-nested-goals-allowed is
+  nil (the default).  Setting this variable to t forces 
+  identical behaviour to before.  The default for Coq is t.
+
 * Renamed some configuration variables for uniformity:
     proof-ctxt-string -> proof-context-command
     proof-help-string -> proof-info-command
     proof-prf-string  -> proof-showproof-command
 
-* Code cleanups and improvements.
+* Many code cleanups and improvements.
 
diff --git a/coq/coq.el b/coq/coq.el
index 4b0f6070..daa71eb6 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -190,8 +190,12 @@
        ((eq (span-property span 'type) 'comment))       
 
        ((eq (span-property span 'type) 'goalsave)
-	(setq ans (concat coq-forget-id-command
-			  (span-property span 'name) proof-terminal-string)))
+	;; FIXME da 5.10.99: I added in this test for an unnamed
+	;; theorem.  Probably it is harmless (it's a new case for LEGO
+	;; and Isabelle).
+	(unless (eq (span-property span 'name) proof-unnamed-theorem-name)
+	  (setq ans (concat lego-forget-id-command
+			    (span-property span 'name) proof-terminal-string))))
 
        ((proof-string-match (concat "\\`\\(" coq-keywords-decl-defn-regexp
                               "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str)
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 54c6e6fb..a2191dce 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1298,6 +1298,12 @@ These are evaluated and appended to `proof-splash-contents'."
   :type 'string
   :group 'proof-general-internals)
 
+(defcustom proof-unnamed-theorem-name
+  "Unnamed_thm"
+  "A name for theorems which are unnamed.  Used internally by Proof General."
+  :type 'string
+  :group 'proof-general-internals)
+
 ;; FIXME: da: could we put these into another keymap shared across the
 ;; various PG modes?
 (defcustom proof-universal-keys
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 175906d7..6f8a7396 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -852,7 +852,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	;; FIXME da: maybe this should be prover specific: is
 	;; "Unnamed_thm" actually a Coq identifier?
 	(unless nam
-	  (setq nam "Unnamed_thm"))
+	  (setq nam proof-unnamed-theorem-name))
 
 	;; Now make the new goal-save span
 	(set-span-end gspan end)
@@ -910,7 +910,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	       (setq nam (match-string 2 (span-property gspan 'cmd))))
 	  ;; As a final desparate attempt, set the name to "Unnamed_thm".
 	  (unless nam
-	    (setq nam "Unnamed_thm"))
+	    (setq nam proof-unnamed-theorem-name))
 	  
 	  ;; Now make the new goal-save span
 	  (set-span-end gspan (span-start span))
@@ -1695,6 +1695,8 @@ Typically, a list of syntax of commands available."
 (defun proof-cd-sync ()
   "If proof-shell-cd is set, do proof-cd and wait for prover ready.
 This is intended as a value for proof-activate-scripting-hook"
+  ;; The hook is set in proof-mode before proof-shell-cd may be set,
+  ;; so we explicitly test it here.  
   (if proof-shell-cd 
       (progn
 	(proof-cd)
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index 9feb283a..454eeb42 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -82,7 +82,7 @@
 ;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore,
 ;; it might be safer to append "\\s-*:".
 (defconst lego-goal-with-hole-regexp
-  (concat "\\(" (proof-ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^:]+\\)")
+  (concat "\\(" (proof-ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^(){},:]+\\)")
   "Regular expression which matches an entry in `lego-keywords-goal'
   and the name of the goal.") 
 
diff --git a/lego/lego.el b/lego/lego.el
index bf906c9f..603b19d5 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -109,7 +109,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 "KillRef: ok, not in proof state"
@@ -216,8 +216,9 @@ Given is the first SPAN which needs to be undone."
        ((eq (span-property span 'type) 'comment))
 
        ((eq (span-property span 'type) 'goalsave)
-	(setq ans (concat lego-forget-id-command
-			  (span-property span 'name) proof-terminal-string)))
+	(unless (eq (span-property span 'name) proof-unnamed-theorem-name)
+	  (setq ans (concat lego-forget-id-command
+			    (span-property span 'name) proof-terminal-string))))
 
        ;; alternative definitions
        ((proof-string-match lego-definiendum-alternative-regexp str)
@@ -243,7 +244,8 @@ Given is the first SPAN which needs to be undone."
        ((proof-string-match "\\`\\s-*Module\\s-+\\(\\S-+\\)\\W" str)
 	(setq ans (concat "ForgetMark " (match-string 1 str) 
 			  proof-terminal-string))))
-      
+      ;; Carry on searching forward for something to forget
+      ;; (The first thing to be forget will forget everything following)
       (setq span (next-span span 'type)))
   (or ans proof-no-command)))