Moved code into proof-system and proof-utils.

1 files changed, 14 insertions, 393 deletions

diff --git a/generic/proof.el b/generic/proof.el
index 102a8727..d2eb93a1 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -19,6 +19,7 @@
 (require 'proof-site)			; site config
 
 ;; cl is dumped with my XEmacs 20.4, but not FSF Emacs 20.2.
+;; would rather it was autoloaded but autoloads broken in FSF.
 (require 'cl)				
 
 (require 'proof-config)			; configuration variables
@@ -40,6 +41,9 @@
 (autoload 'font-lock-fontify-region "font-lock")
 (autoload 'font-lock-append-text-property "font-lock")
 
+
+;;; FIXME: autoloads should be automatic!!
+
 ;;;
 ;;; Autoloads for main code
 ;;;
@@ -84,10 +88,15 @@
 (autoload 'proof-x-symbol-configure "proof-x-symbol"
   "Configure the current buffer for X-Symbol.")
 
+
 ;;;
 ;;; Global variables
 ;;;
 
+; rough test for XEmacs on win32
+(defconst proof-running-on-win32 (fboundp 'win32-long-file-name)
+  "Non-nil if we're running on a win32 system.")
+
 (deflocal proof-buffer-type nil 
   "Symbol indicating the type of this buffer: 'script, 'shell, 'pbp, or 'response.")
 
@@ -162,402 +171,14 @@ of the proof (starting from 1).")
       (apply 'message str args)
       (sit-for 2)))
 
-;;;
-;;; Utilities/macros used in several files  (-> proof-utils)
-;;;
-
-
-;; -----------------------------------------------------------------
-;; Handy macros
-
-(defmacro proof-with-current-buffer-if-exists (buf &rest body)
-  "As with-current-buffer if BUF exists and is live, otherwise nothing."
-  `(if (buffer-live-p ,buf)
-       (with-current-buffer ,buf
-	 ,@body)))
-
-(defmacro proof-map-buffers (buflist &rest body)
-  "Do BODY on each buffer in BUFLIST, if it exists."
-  `(dolist (buf ,buflist)
-     (proof-with-current-buffer-if-exists buf ,@body)))
-
-(defmacro proof-customize-toggle (var)
-  "Make a function for toggling a boolean customize setting VAR.
-The toggle function uses customize-set-variable to change the variable."
-  `(lambda (arg)
-     ,(concat "Toggle " (symbol-name var) ". With ARG, turn on iff ARG>0.
-This function simply uses customize-set-variable to set the variable.
-It was constructed with the macro proof-customize-toggle.")
-     (interactive "P")
-     (customize-set-variable 
-      (quote ,var)
-      (if (null arg) (not ,var)
-	(> (prefix-numeric-value arg) 0)))))
-
-;; FIXME: combine this with above, and remove messing calls in
-;; proof-script.
-(defmacro proof-deftoggle (var)
-  "Define a function VAR-toggle for toggling a boolean customize setting VAR.
-The toggle function uses customize-set-variable to change the variable."
-  `(defun ,(intern (concat (symbol-name var) "-toggle")) (arg)
-     ,(concat "Toggle " (symbol-name var) ". With ARG, turn on iff ARG>0.
-This function simply uses customize-set-variable to set the variable.
-It was constructed with the macro proof-deftoggle.")
-     (interactive "P")
-     (customize-set-variable 
-      (quote ,var)
-      (if (null arg) (not ,var)
-	(> (prefix-numeric-value arg) 0)))))
-
-(defmacro proof-defshortcut (fn string &optional key)
-  "Define shortcut function FN to insert STRING, optional keydef KEY.
-This is intended for defining proof assistant specific functions.
-STRING is inserted using `proof-insert', which see.
-KEY is added onto proof-assistant map."
-  (if key
-      (eval
-       `(define-key proof-assistant-keymap ,key (quote ,fn))))
-  `(defun ,fn ()
-     "Shortcut command to insert a string."
-     (interactive)
-     (proof-insert ,string)))
-
-  
-(defun proof-try-require (symbol)
-  "Try requiring SYMBOL.  No error if the file for SYMBOL isn't found."
-  (condition-case ()
-      (require symbol)
-    (file-error nil))
-  (featurep symbol))
-
-
-;; -----------------------------------------------------------------
-;; Buffers and filenames
-
-(defun proof-file-truename (filename)
-  "Returns the true name of the file FILENAME or nil if file non-existent."
-  (and filename (file-exists-p filename) (file-truename filename)))
-
-(defun proof-file-to-buffer (filename)
-  "Find a buffer visiting file FILENAME, or nil if there isn't one."
-  (let* ((buffers (buffer-list))
-	 (pos
-	  (position (file-truename filename)
-		    (mapcar 'proof-file-truename
-			    (mapcar 'buffer-file-name
-				    buffers))
-		    :test 'equal)))
-    (and pos (nth pos buffers))))
-
-(defun proof-files-to-buffers (filenames)
-  "Converts a list of FILENAMES into a list of BUFFERS."
-  (if (null filenames) nil
-    (let* ((buffer (proof-file-to-buffer (car filenames)))
-	  (rest (proof-files-to-buffers (cdr filenames))))
-      (if buffer (cons buffer rest) rest))))
-
-(defun proof-buffers-in-mode (mode &optional buflist)
-  "Return a list of the buffers in the buffer list in major-mode MODE.
-Restrict to BUFLIST if it's set."
-  (let ((bufs-left (or buflist (buffer-list))) 
-	bufs-got)
-    (dolist (buf bufs-left bufs-got)
-      (if (with-current-buffer buf (eq mode major-mode))
-	  (setq bufs-got (cons buf bufs-got))))))
-
-;; -----------------------------------------------------------------
-;; Key functions
-
-(defun proof-define-keys (map kbl)
-  "Adds keybindings KBL in MAP.
-The argument KBL is a list of tuples (k . f) where `k' is a keybinding
-(vector) and `f' the designated function."
-  (mapcar
-   (lambda (kbl)
-     (let ((k (car kbl)) (f (cdr kbl)))
-         (define-key map k f)))
-   kbl))
-
-;; -----------------------------------------------------------------
-;; Managing font-lock
-;;
-
-;; Notes:
-;;
-;; * Various mechanisms for setting defaults, different between 
-;;   Emacsen.  Old method(?) was to set "blah-mode-font-lock-keywords"
-;;   and copy it into "font-lock-keywords" to engage font-lock.
-;;   Present method for XEmacs is to put a 'font-lock-defaults 
-;;   property on the major-mode symbol, or use font-lock-defaults
-;;   buffer local variable.  We use the later.
-;;
-;; * Buffers which are output-only are *not* kept in special minor
-;;   modes font-lock-mode (or x-symbol-mode).  In case the user
-;;   doesn't want fontification we have a user option,
-;;   proof-output-fontify-enable.
-
-(deflocal proof-font-lock-keywords nil
-  "Value of font-lock-keywords in this buffer.
-We set font-lock-defaults to '(proof-font-lock-keywords t) for
-compatibility with X-Symbol, which may hack proof-font-lock-keywords
-with extra patterns (in non-mule mode).")
-
-; (deflocal proof-font-lock-defaults nil
-;  "Value of font-lock-defaults in this buffer.
-
-(defun proof-font-lock-configure-defaults (&optional case-fold)
-  "Set defaults for font-lock based on current font-lock-keywords."
-  ;;
-  ;; At the moment, the specific assistant code hacks
-  ;; font-lock-keywords.  Here we use that value to hack
-  ;; font-lock-defaults, which is used by font-lock to set
-  ;; font-lock-keywords from again!!  Yuk.
-  ;;
-  ;; Previously, 'font-lock-keywords was used directly as a setting
-  ;; for the defaults.  This has a bad interaction with x-symbol which
-  ;; edits font-lock-keywords and loses the setting.  So we make a
-  ;; copy of it in a new local variable, proof-font-lock-keywords.
-  ;;
-  ;; FIXME: specific code could set this variable directly, really.
-  (setq proof-font-lock-keywords font-lock-keywords)
-  (setq font-lock-keywords-case-fold-search case-fold)
-  ;; Setting font-lock-defaults explicitly is required by FSF Emacs
-  ;; 20.4's version of font-lock in any case.
-  (make-local-variable 'font-lock-defaults) ; not needed in XEmacs, FSF?
-  (setq font-lock-defaults `(proof-font-lock-keywords nil ,case-fold))
-  ;; 12.1.99: testing: For XEmacs, we must also set the property.
-  ;; This is needed for buffers which are put into font-lock-mode
-  ;; (rather than fontified by hand).
-  (put major-mode 'font-lock-defaults font-lock-defaults)
-  (setq font-lock-keywords nil))
-
-(defun proof-fontify-region (start end)
-  "Fontify and decode X-Symbols in region START...END.
-Fontifies according to the buffer's font lock defaults.
-Uses proof-x-symbol-decode to decode tokens if x-symbol is present.
-
-If proof-shell-leave-annotations-in-output is set, remove characters
-with top bit set after fontifying so they can be used for
-fontification.
-
-Returns new END value."
-  ;; We fontify first because decoding changes char positions.
-  ;; It's okay because x-symbol-decode works even without font lock.
-  ;; Possible disadvantage is that font lock patterns can't refer
-  ;; to X-Symbol characters.  Probably they shouldn't!
-  (narrow-to-region start end)
-
-  (if proof-output-fontify-enable
-      (progn
-	;; FSF hack, yuk.
-	(unless (string-match "XEmacs" emacs-version)
-	  (font-lock-set-defaults))
-	(let ((font-lock-keywords proof-font-lock-keywords))
-	  ;; FIXME: should set other bits of font lock defaults,
-	  ;; perhaps, such as case fold etc.  What happened to
-	  ;; the careful buffer local font-lock-defaults??
-	  (font-lock-fontify-region start end)
-	  (proof-zap-commas-region start end))))
-  (if proof-shell-leave-annotations-in-output
-      ;; Remove special characters that were used for font lock,
-      ;; so cut and paste works from here.
-      (let ((p (point)))
-	(goto-char start)
-	(while (< (point) (point-max))
-	  (forward-char)
-	  (unless (< (char-before (point)) 128) ; char-to-int in XEmacs
-	    (delete-char -1)))
-	(goto-char p)))
-  (proof-x-symbol-decode-region start (point-max))
-  (prog1 (point-max)
-    (widen)))
-
-;; FIXME todo: add toggle for fontify region which turns it on/off
-;; (maybe).
-
-(defun proof-fontify-buffer ()
-  "Call proof-fontify-region on whole buffer."
-  (proof-fontify-region (point-min) (point-max)))
-
-
-
-;; -----------------------------------------------------------------
-;; Messaging and display functions
-;;
-
-
-(defun proof-warn-if-unset (tag sym)
-  "Give a warning (with TAG) if symbol SYM is unbound or nil."
-  (unless (and (boundp sym) (symbol-value sym))
-    (warn "Proof General %s: %s is unset."  tag (symbol-name sym))))
-
-;; FIXME: this function should be combined with
-;; proof-shell-maybe-erase-response-buffer. 
-(defun proof-response-buffer-display (str &optional face)
-  "Display STR with FACE in response buffer and return fontified STR."
-  (if (string-equal str "\n")	
-      str				; quick exit, no display.
-  (let (start end)
-    (with-current-buffer proof-response-buffer
-      ;; da: I've moved newline before the string itself, to match
-      ;; the other cases when messages are inserted and to cope
-      ;; with warnings after delayed output (non newline terminated).
-      ; (ugit (format "End is %i" (point-max)))
-      (goto-char (point-max))
-      (newline)				
-      (setq start (point))
-      (insert str)
-      (unless (bolp) (newline))
-      (setq end (proof-fontify-region start (point)))
-      ;; This is one reason why we don't keep the buffer in font-lock
-      ;; minor mode: it destroys this hacky property as soon as it's
-      ;; made!  (Using the minor mode is much more convenient, tho')
-      (if (and face proof-output-fontify-enable)
-	  (font-lock-append-text-property start end 'face face))
-      ;; This returns the decorated string, but it doesn't appear 
-      ;; decorated in the minibuffer, unfortunately.
-      (buffer-substring start (point-max))))))
-
-(defun proof-display-and-keep-buffer (buffer &optional pos)
-  "Display BUFFER and mark window according to `proof-dont-switch-windows'.
-If optional POS is present, will set point to POS.  
-Otherwise move point to the end of the buffer.
-Ensure that point is visible in window."
-  (let (window)
-    (save-excursion
-      (set-buffer buffer)
-      (display-buffer buffer)
-      (setq window (get-buffer-window buffer 'visible))
-      (set-window-dedicated-p window proof-dont-switch-windows)
-      (and window
-	   (save-selected-window
-	     (select-window window)
-	     
-	     ;; tms: I don't understand why the point in
-	     ;; proof-response-buffer is not at the end anyway.
-	     ;; Is there a superfluous save-excursion somewhere?
-	     ;; da replies: I think it's because of a *missing*
-	     ;; save-excursion above around the font-lock stuff.
-	     ;; Adding one has maybe fixed this problem.
-	     ;; 10.12.98 Experiment removing this so that point
-	     ;; doesn't always go to end of goals buffer
-	     ;; RESULT: point doesn't go to end of response
-	     ;; buffer.  Hypothesis above was wrong, so this
-	     ;; is re-added and optional POS argument added
-	     ;; for this function.
-	     (goto-char (or pos (point-max)))
-	     (if pos (beginning-of-line)) ;  Normalization
-
-	     ;; Ensure point visible
-	     (or (pos-visible-in-window-p (point) window)
-		 (recenter -1)))))))
-
-(defun proof-clean-buffer (buffer)
-  "Erase buffer and hide from display if proof-delete-empty-windows set.
-Auto deletion only affects selected frame.  (We assume that the selected
-frame is the one showing the script buffer.)"
-  (with-current-buffer buffer
-    ;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(.
-    (erase-buffer)
-    (if proof-delete-empty-windows
-	(delete-windows-on buffer t))))
-
-(defun proof-message (&rest args)
-  "Issue the message ARGS in the response buffer and display it."
-    (proof-response-buffer-display (apply 'concat args))
-    (proof-display-and-keep-buffer proof-response-buffer))
-
-(defun proof-warning (&rest args)
-  "Issue the warning ARGS in the response buffer and display it.
-The warning is coloured with proof-warning-face."
-    (proof-response-buffer-display (apply 'concat args) 'proof-warning-face)
-    (proof-display-and-keep-buffer proof-response-buffer))
-
-;; could be a macro for efficiency in compiled code
-(defun proof-debug (&rest args)
-  "Issue the debugging messages ARGS in the response buffer, display it.
-If proof-show-debug-messages is nil, do nothing."
-  (if proof-show-debug-messages
-      (progn
-	(proof-response-buffer-display (apply 'concat 
-					      "PG debug: " 
-					      args)
-				       'proof-debug-message-face)
-	(proof-display-and-keep-buffer proof-response-buffer))))
-
-
-;;; A handy utility function used in the "Buffers" menu.
-(defun proof-switch-to-buffer (buf &optional noselect)
-  "Switch to or display buffer BUF in other window unless already displayed.
-If optional arg NOSELECT is true, don't switch, only display it.
-No action if BUF is nil or killed."
-  ;; Maybe this needs to be more sophisticated, using 
-  ;; proof-display-and-keep-buffer ?
-  (and (buffer-live-p buf)
-       (unless (eq buf (window-buffer (selected-window)))
-	 (if noselect
-	     (display-buffer buf t)
-	   (switch-to-buffer-other-window buf)))))
 
-;;
-;; Flag and function to keep response buffer tidy.
-;;
-;; FIXME: rename this now it's moved out of proof-shell.
-;;
-(defvar proof-shell-erase-response-flag nil
-  "Indicates that the response buffer should be cleared before next message.")
-
-(defun proof-shell-maybe-erase-response
-  (&optional erase-next-time clean-windows force)
-  "Erase the response buffer according to proof-shell-erase-response-flag.
-ERASE-NEXT-TIME is the new value for the flag.
-If CLEAN-WINDOWS is set, use proof-clean-buffer to do the erasing.
-If FORCE, override proof-shell-erase-response-flag.
-
-If the user option proof-tidy-response is nil, then
-the buffer is only cleared when FORCE is set.
-
-No effect if there is no response buffer currently.
-Returns non-nil if response buffer was cleared."
-  (when (buffer-live-p proof-response-buffer)
-    (let ((doit (or (and
-		     proof-tidy-response
-		     (not (eq proof-shell-erase-response-flag 'invisible))
-		     proof-shell-erase-response-flag) 
-		    force)))
-      (if doit
-	  (if clean-windows
-	      (proof-clean-buffer proof-response-buffer)
-	  ;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(.
-	  ;; (erase-buffer proof-response-buffer)
-	    (with-current-buffer proof-response-buffer
-	      (erase-buffer))))
-      (setq proof-shell-erase-response-flag erase-next-time)
-      doit)))
-
-
-
-;; -----------------------------------------------------------------
-;; Function for submitting bug reports.
-
-(defun proof-submit-bug-report ()
-  "Submit an bug report or other report for Proof General."
-  (interactive)
-  (require 'reporter)
-  (let
-      ((reporter-prompt-for-summary-p 
-	"(Very) brief summary of problem or suggestion: "))
-    (reporter-submit-bug-report
-     "proofgen@dcs.ed.ac.uk"
-     "Proof General" 
-     (list 'proof-general-version 'proof-assistant)
-     nil nil
-     "[ When reporting a bug, please include a small test case for us to repeat it.
- Please also check that it is not already covered in the BUGS files that came with
- the distribution, or the latest versions at 
- http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral/BUGS ]")))
 
+;;;
+;;; Load other Proof General libraries
+;;;
 
+(require 'proof-utils)
+(require 'proof-system)
 
 
 (provide 'proof)