Compilation tweaks

9 files changed, 59 insertions, 67 deletions

diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index b9f6e72b..9372d3d1 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -14,11 +14,13 @@
 ;;; Code:
 
 (eval-when-compile 
-  (require 'proof)				; globals
   (require 'proof-syntax)			; proof-replace-{string,regexp}
   (require 'span)				; spans
   (require 'cl))				; incf
 
+(require 'proof)				; globals
+
+
 (eval-and-compile ; defines proof-universal-keys-only-mode-map at compile time
   (define-derived-mode proof-universal-keys-only-mode fundamental-mode
     proof-general-name "Universal keymaps only"
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index f1558217..c55c593f 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -12,16 +12,13 @@
 (eval-when-compile
   (require 'easymenu)			; easy-menu-add, etc
   (require 'cl)				; incf
-  (require 'span)			; span-*
-  (require 'proof-utils))
-
+  (require 'span))			; span-*
 
 ;;; Commentary:
-;; 
 
-(require 'proof-site)
+(require 'proof)
+(require 'pg-assoc)
 (require 'bufhist)
-;(require 'pg-assoc)
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -45,7 +42,8 @@ May enable proof-by-pointing or similar features.
   (erase-buffer)
   (buffer-disable-undo)
   (if proof-keep-response-history (bufhist-mode)) ; history for contents
-  (set-buffer-modified-p nil))
+  (set-buffer-modified-p nil)
+  (setq cursor-type nil))
 
 ;;
 ;; Menu for goals buffer
diff --git a/generic/pg-metadata.el b/generic/pg-metadata.el
index 86800e2a..32a61049 100644
--- a/generic/pg-metadata.el
+++ b/generic/pg-metadata.el
@@ -18,10 +18,13 @@
 ;; NB: THIS FILE NOT YET USED: once required by PG,
 ;; must be added to main dist by editing Makefile.devel
 ;;
+;; TODO:
+;;  - look at using cookies for this (Elib)
 
 ;;; Code:
 
 (require 'pg-xml)
+(require 'proof-config)			; proof-face-specs
 
 (defcustom pg-metadata-default-directory "~/.proofgeneral/"
   "*Directory for storing metadata information about proof scripts."
@@ -45,10 +48,7 @@
   ;; Clashes are possible, hopefully unlikely.
   (concat
    (file-name-as-directory pg-metadata-default-directory)
-   (replace-in-string
-    (file-name-sans-extension filename)
-    (regexp-quote (char-to-string directory-sep-char))
-    "__")
+   (replace-in-string (file-name-sans-extension filename) "/" "__")
    ".pgm"))
 
 
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 80713154..ee5bb9ba 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -54,7 +54,8 @@
   (erase-buffer)
   (buffer-disable-undo)
   (if proof-keep-response-history (bufhist-mode)) ; history for contents
-  (set-buffer-modified-p nil))
+  (set-buffer-modified-p nil)
+  (setq cursor-type nil))
 
 (proof-eval-when-ready-for-assistant ; proof-aux-menu depends on <PA>
     (easy-menu-define proof-response-mode-menu
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 620dbacb..e72df3c6 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -139,6 +139,10 @@ assistant during the last group of commands.")
 If non-nil, the value counts the commands from the last command
 of the proof (starting from 1).")
 
+(defvar proof-shell-last-output nil
+  "A record of the last string seen from the proof system.
+This is raw string, for internal use only.")
+
 ;; TODO da: remove proof-terminal-string.  At the moment some
 ;; commands need to have the terminal string, some don't.
 ;; It's used variously in proof-script and proof-shell, which
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index f4301a66..f373b19f 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -53,7 +53,7 @@ This mode is only useful with a font which can display the maths repertoire.
 ;;;***
 
 ;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el"
-;;;;;;  (18316 44932))
+;;;;;;  (18317 59757))
 ;;; Generated autoloads from pg-goals.el
 
 (autoload (quote proof-goals-config-done) "pg-goals" "\
@@ -87,7 +87,7 @@ Send an <askprefs> message to the prover.
 
 ;;;### (autoloads (pg-response-has-error-location proof-next-error
 ;;;;;;  pg-response-maybe-erase proof-response-config-done proof-response-mode)
-;;;;;;  "pg-response" "pg-response.el" (18317 3795))
+;;;;;;  "pg-response" "pg-response.el" (18317 22894))
 ;;; Generated autoloads from pg-response.el
 
 (autoload (quote proof-response-mode) "pg-response" "\
@@ -309,10 +309,15 @@ in future if we have just activated it for this buffer.
 
 ;;;***
 
-;;;### (autoloads (proof-config-done proof-mode) "proof-script" "proof-script.el"
-;;;;;;  (18317 16156))
+;;;### (autoloads (proof-config-done proof-mode proof-insert-pbp-command)
+;;;;;;  "proof-script" "proof-script.el" (18317 59727))
 ;;; Generated autoloads from proof-script.el
 
+(autoload (quote proof-insert-pbp-command) "proof-script" "\
+Insert CMD into the proof queue.
+
+\(fn CMD)" nil nil)
+
 (autoload (quote proof-mode) "proof-script" "\
 Proof General major mode class for proof scripts.
 \\{proof-mode-map}
@@ -328,10 +333,11 @@ finish setup which depends on specific proof assistant configuration.
 
 ;;;***
 
-;;;### (autoloads (proof-shell-config-done proof-shell-mode proof-shell-invisible-command
+;;;### (autoloads (proof-shell-config-done proof-shell-mode proof-shell-invisible-command-invisible-result
+;;;;;;  proof-shell-invisible-cmd-get-result proof-shell-invisible-command
 ;;;;;;  proof-shell-wait proof-extend-queue proof-start-queue proof-shell-insert
 ;;;;;;  proof-shell-available-p proof-shell-live-buffer proof-shell-ready-prover)
-;;;;;;  "proof-shell" "proof-shell.el" (18317 3795))
+;;;;;;  "proof-shell" "proof-shell.el" (18317 59753))
 ;;; Generated autoloads from proof-shell.el
 
 (autoload (quote proof-shell-ready-prover) "proof-shell" "\
@@ -410,6 +416,23 @@ In case CMD is (or yields) nil, do nothing.
 
 \(fn CMD &optional WAIT)" nil nil)
 
+(autoload (quote proof-shell-invisible-cmd-get-result) "proof-shell" "\
+Execute CMD and return result as a string.
+This expects CMD to print something to the response buffer.
+The output in the response buffer is disabled, and the result
+\(contents of `proof-shell-last-output') is returned as a 
+string instead.  
+
+Errors are not supressed and will result in a display as 
+usual, unless NOERROR is non-nil.
+
+\(fn CMD &optional NOERROR)" nil nil)
+
+(autoload (quote proof-shell-invisible-command-invisible-result) "proof-shell" "\
+Execute CMD, wait for but do not display result.
+
+\(fn CMD &optional NOERROR)" nil nil)
+
 (autoload (quote proof-shell-mode) "proof-shell" "\
 Proof General shell mode class for proof assistant processes
 
@@ -477,7 +500,7 @@ Menu made from the Proof General toolbar commands.
 
 ;;;### (autoloads (proof-x-symbol-config-output-buffer proof-x-symbol-shell-config
 ;;;;;;  proof-x-symbol-decode-region proof-x-symbol-enable proof-x-symbol-support-maybe-available)
-;;;;;;  "proof-x-symbol" "proof-x-symbol.el" (18317 16630))
+;;;;;;  "proof-x-symbol" "proof-x-symbol.el" (18317 59366))
 ;;; Generated autoloads from proof-x-symbol.el
 
 (autoload (quote proof-x-symbol-support-maybe-available) "proof-x-symbol" "\
@@ -520,7 +543,7 @@ Configure the current output buffer (goals/response/trace) for X-Symbol.
 ;;;;;;  "pg-pgip-old.el" "pg-vars.el" "pg-xhtml.el" "proof-config.el"
 ;;;;;;  "proof-site.el" "proof-utils.el" "proof.el" "test-compile.el"
 ;;;;;;  "test-mac.el" "test-mac2.el" "test-req.el" "test-req2.el")
-;;;;;;  (18317 18440 719057))
+;;;;;;  (18317 59766 407486))
 
 ;;;***
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 0b75ade4..7b70a64f 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -57,6 +57,9 @@ The `find-alternative-file' function has a nasty habit of setting the
 buffer file name to nil before running kill buffer, which breaks PG's
 kill buffer hook.  This variable is used when buffer-file-name is nil.")
 
+(deflocal pg-script-portions nil
+  "Table of lists of symbols naming script portions which have been processed so far.")
+
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -508,9 +511,6 @@ Assumes script buffer is current"
 This is used for cleaning `buffer-invisibility-spec' in
 `pg-clear-script-portions': it doesn't need to be exactly accurate.")
 
-(deflocal pg-script-portions nil
-  "Table of lists of symbols naming script portions which have been processed so far.")
-
 (defun pg-clear-script-portions ()
   "Clear record of script portion names and types from internal list.
 Also clear all visibility specifications."
@@ -2189,6 +2189,7 @@ appropriate."
 ;;      
 ;; PBP call-backs
 ;;
+;;;###autoload
 (defun proof-insert-pbp-command (cmd)
   "Insert CMD into the proof queue."
   (proof-activate-scripting)
@@ -2794,10 +2795,11 @@ finish setup which depends on specific proof assistant configuration."
       (setq buffer-offer-save t))
 
   ;; Localise the invisibility glyph (XEmacs only):
-  (let ((img (proof-get-image "hiddenproof" t "<proof>")))
-    (cond
-     ((and img (featurep 'xemacs))
-      (set-glyph-image invisible-text-glyph img (current-buffer)))))
+  (if (featurep 'xemacs)
+      (let ((img (proof-get-image "hiddenproof" t "<proof>")))
+	(if img
+	    (set-glyph-image invisible-text-glyph 
+			     img (current-buffer)))))
 
   (if (proof-ass x-symbol-enable)
       (proof-x-symbol-enable))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 5443963c..a30711d9 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -20,42 +20,6 @@
 (require 'pg-goals)
 (require 'proof-script)
 
-;;
-;; Internal variables used in sub-modules
-;;
-
-;; A raw record of the last output from the proof system
-(defvar proof-shell-last-output nil
-  "A record of the last string seen from the proof system.")
-
-
-
-
-;; ;; FIXME:
-;; ;; Autoloads for proof-script (added to nuke warnings,
-;; ;; maybe should be 'official' exported functions in proof.el)
-;; ;; This helps see interface between proof-script / proof-shell.
-;; ;; FIXME 2: We can probably assume that proof-script is always
-;; ;; loaded before proof-shell, so just put a require on 
-;; ;; proof-script here.
-;; (eval-and-compile
-;;   (mapcar (lambda (f) 
-;; 	    (autoload f "proof-script"))
-;; 	  '(proof-goto-end-of-locked
-;; 	    proof-insert-pbp-command
-;; 	    proof-detach-queue 
-;; 	    proof-locked-end 
-;; 	    proof-set-queue-endpoints
-;; 	    proof-script-clear-queue-spans
-;; 	    proof-file-to-buffer 
-;; 	    proof-register-possibly-new-processed-file
-;; 	    proof-restart-buffers)))
-
-;; FIXME:
-;; Some variables from proof-shell are also used, in particular,
-;; the menus.  These should probably be moved out to proof-menu.
-
-
 ;; ============================================================
 ;;
 ;; Internal variables used by proof shell
@@ -1886,6 +1850,7 @@ In case CMD is (or yields) nil, do nothing."
 				  cmd 'proof-done-invisible)))
 	(if wait (proof-shell-wait)))))
 
+;;;###autoload
 (defun proof-shell-invisible-cmd-get-result (cmd &optional noerror)
   "Execute CMD and return result as a string.
 This expects CMD to print something to the response buffer.
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index 4cf3c09a..835d4986 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -43,9 +43,6 @@
 ;; =================================================================
 
 (eval-when-compile
-  (add-to-list 'load-path "../x-symbol/lisp")
-  (require 'x-symbol-hooks)		; <reduce compiler warnings>
-  (require 'x-symbol-autoloads)		; <reduce compiler warnings>
   (require 'proof-utils))		; proof-ass
 
 (require 'proof-config)			; variables