Renamed proof-invisible-command proof-shell-invisible-command.

Removed superfluous optional 'relaxed' argument from:
  proof-shell-invisibile-command,
  proof-grab-lock,
  proof-start-queue.

5 files changed, 37 insertions, 30 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 106aa94d..73f58af9 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -107,7 +107,7 @@
   (remove-hook 'proof-shell-insert-hook 'coq-shell-init-hook))
 
 (defun coq-set-undo-limit (undos)
-  (proof-invisible-command (format "Set Undo %s." undos)))
+  (proof-shell-invisible-command (format "Set Undo %s." undos)))
 
 (defun coq-count-undos (span)
   (let ((ct 0) str i)
@@ -237,7 +237,8 @@
   (let (cmd)
     (proof-shell-ready-prover) ;; was (proof-check-process-available)
     (setq cmd (read-string "Search Type: " nil 'proof-minibuffer-history))
-    (proof-invisible-command (concat "Search " cmd proof-terminal-string))))
+    (proof-shell-invisible-command
+     (concat "Search " cmd proof-terminal-string))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Indentation                                                    ;;
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 51dd695e..06aa9b6b 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1088,11 +1088,15 @@ Only for use by consenting adults."
   "History of proof commands read from the minibuffer")
 
 (defun proof-execute-minibuffer-cmd ()
+  "Prompt for a command in the minibuffer and send it to proof assistant."
   (interactive)
   (let (cmd)
-    (proof-shell-ready-prover) ;; was (proof-check-process-available 'relaxed) 
+    ;; FIXME note: removed ready-prover call since it's done by
+    ;; proof-shell-invisible-command anyway.
+    ;; (proof-shell-ready-prover)
+    ;; was (proof-check-process-available 'relaxed) 
     (setq cmd (read-string "Command: " nil 'proof-minibuffer-history))
-    (proof-invisible-command cmd 'relaxed)))
+    (proof-shell-invisible-command cmd)))
 
 
 
@@ -1145,17 +1149,17 @@ Based on position of point."
 (defun proof-ctxt ()
   "List context."
   (interactive) 
-  (proof-invisible-command (concat proof-ctxt-string proof-terminal-string)))
+  (proof-shell-invisible-command (concat proof-ctxt-string proof-terminal-string)))
 
 (defun proof-help ()
   "Print help message giving syntax."
   (interactive)
-  (proof-invisible-command (concat proof-help-string proof-terminal-string)))
+  (proof-shell-invisible-command (concat proof-help-string proof-terminal-string)))
 
 (defun proof-prf ()
   "List proof state."
   (interactive)
-  (proof-invisible-command (concat proof-prf-string proof-terminal-string)))
+  (proof-shell-invisible-command (concat proof-prf-string proof-terminal-string)))
 
 
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f029c36a..d5d0cb57 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -79,17 +79,17 @@ an error.")
 ;;
 ;;   was passed into proof-grab by proof-start-queue
 ;;    only call to proof-start-queue with this arg is in
-;;    proof-invisible-command.
-;;   only call of proof-invisible-command with relaxed arg
+;;    proof-shell-invisible-command.
+;;   only call of proof-shell-invisible-command with relaxed arg
 ;;   is in proof-execute-minibuffer-cmd.
 ;;  --- presumably so that command could be executed from any
 ;;  buffer, not just a scripting one?
 ;;
-;;  I think it's wrong for proof-invisible-command to enforce
+;;  I think it's wrong for proof-shell-invisible-command to enforce
 ;;  scripting buffer!
 ;; 
 ;;  This is reflected now by just calling (proof-shell-ready-prover)
-;;  in proof-invisible-command, not proof-check-process-available.
+;;  in proof-shell-invisible-command, not proof-check-process-available.
 ;;
 ;; Hopefully we can get rid of these messy 'relaxed' flags now.
 ;;
@@ -112,10 +112,10 @@ No error messages.  Useful as menu or toolbar enabler."
   (and (proof-shell-live-buffer)
        (not proof-shell-busy)))
 
-(defun proof-grab-lock (&optional relaxed)
+;; FIXME: note: removed optional 'relaxed' arg
+(defun proof-grab-lock ()
   "Grab the proof shell lock."
-  ;; FIXME: this used to observe 'relaxed' flag, now it ignores it!
-  (proof-shell-ready-prover)			;
+  (proof-shell-ready-prover)
   (setq proof-shell-busy t))
 
 (defun proof-release-lock ()
@@ -271,13 +271,13 @@ Does nothing if proof assistant is already running."
       (pop-to-buffer (car proof-script-buffer-list))
       (cond
        (span
-	(proof-invisible-command 
+	(proof-shell-invisible-command 
 	 (format (if (eq 'hyp (car top-info)) pbp-hyp-command 
 		                              pbp-goal-command)
 		 (concat (cdr top-info) (proof-expand-path 
 					 (span-property span 'proof))))))
        ((eq (car top-info) 'hyp)
-	(proof-invisible-command (format pbp-hyp-command (cdr top-info))))
+	(proof-shell-invisible-command (format pbp-hyp-command (cdr top-info))))
        (t
 	 (proof-insert-pbp-command (format pbp-change-goal (cdr top-info))))))
     ))
@@ -652,7 +652,8 @@ assistant."
 
 ; Pass start and end as nil if the cmd isn't in the buffer.
 
-(defun proof-start-queue (start end alist &optional relaxed)
+;; FIXME: note: removed optional 'relaxed' arg
+(defun proof-start-queue (start end alist)
   (if start
       (proof-set-queue-endpoints start end))
   (let (item)
@@ -663,7 +664,7 @@ assistant."
     (setq alist (cdr alist)))
   (if alist
       (progn
-	(proof-grab-lock relaxed) 
+	(proof-grab-lock) 
 	(setq proof-shell-delayed-output (cons 'insert "Done."))
 	(setq proof-action-list alist)
 	(proof-send (nth 1 item))))))
@@ -738,6 +739,7 @@ at the end of locked region (after inserting a newline and indenting)."
 		  (cons (list span cmd 'proof-done-advancing)
 			(cdr proof-action-list)))))))
 
+;; da: this note seems to be false!
 ;; ******** NB **********
 ;;  While we're using pty communication, this code is OK, since all
 ;; eager annotations are one line long, and we get input a line at a
@@ -903,19 +905,19 @@ how far we've got."
       (setq span (prev-span span 'type)))
     span)))
     
-(defun proof-done-invisible (span) ())
-
+(defun proof-shell-done-invisible (span) ())
 
 ;; da: What is the rationale here for making the *command* sent
 ;; invisible, rather than the stuff returned????
 ;; doc string makes no sense of this.
-(defun proof-invisible-command (cmd &optional relaxed)
+;; FIXME: note: removed optional 'relaxed' arg
+(defun proof-shell-invisible-command (cmd)
   "Send cmd to the proof process without responding to the user."
   (proof-shell-ready-prover)
   (if (not (string-match proof-re-end-of-cmd cmd))
       (setq cmd (concat cmd proof-terminal-string)))
   (proof-start-queue nil nil (list (list nil cmd
-  'proof-done-invisible)) relaxed))
+  'proof-shell-done-invisible))))
 
 
 
diff --git a/isa/isa.el b/isa/isa.el
index 887166f8..00cf9edb 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -155,14 +155,11 @@ no regular or easily discernable structure."
 ;; We use the top level theory and then force an update, both to fix
 ;; up Isabelle's messy dependency handling and to recache the
 ;; list of loaded files inside emacs.
-(defconst isa-usethy-notopml-command "use_thy_and_update \"%s\";"
+(defconst isa-usethy-notopml-command "use_thy_and_update \"%s\"; list_loaded_files();"
   "Command to send to Isabelle to process theory for this ML file.")
 
 ;; Unfortunately, use_thy_no_topml followed by update(); doesn't work
 ;; for *theory* files, because update() will report that the ML file
-
-;; Unfortunately, use_thy_no_topml followed by update(); doesn't work
-;; for *theory* files, because update() will report that the ML file
 ;; 
 (defconst isa-usethy-command "use_thy \"%s\"; update();"
   "Command to send to Isabelle to process a theory file.")
@@ -274,16 +271,16 @@ isa-proofscript-mode."
 (defun isa-process-thy-file (file)
   "Process the theory file FILE.  If interactive, use buffer-file-name."
   (interactive (list buffer-file-name))
-  (proof-invisible-command 
+  (proof-shell-invisible-command 
    (format isa-usethy-notopml-command
-	   (file-name-sans-extension file)) t))
+	   (file-name-sans-extension file))))
 
 (defun isa-retract-thy-file (file)
   "Retract the theory file FILE. If interactive, use buffer-file-name."
   (interactive (list buffer-file-name))
-  (proof-invisible-command
+  (proof-shell-invisible-command
    (format isa-retract-file-command
-	   (file-name-sans-extension file)) t))
+	   (file-name-sans-extension file))))
 
 
 ;; Next portion taken from isa-load.el
diff --git a/todo b/todo
index 72ffe5f4..9a1c5b96 100644
--- a/todo
+++ b/todo
@@ -14,6 +14,9 @@ X (Low)    probably not worth wasting time on
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
+C  Remove "FIXME notes" which are just notes I've put in about old
+   code in case something breaks   (da, 30mins). 
+
 
 A* Fix bugs in proof-shell-filter. Don't assume that full match is
    contained in filter chunk.(Should match strings in buffer instead)