More improvements/fixes for closing unfinished proofs.

Added proof-unnamed-theorem-name.

2 files changed, 10 insertions, 2 deletions

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)