New files

4 files changed, 599 insertions, 0 deletions

diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
new file mode 100644
index 00000000..2363e248
--- /dev/null
+++ b/generic/proof-autoloads.el
@@ -0,0 +1,120 @@
+;;; DO NOT MODIFY THIS FILE
+(if (featurep 'proof-autoloads) (error "Already loaded"))
+
+;;;### (autoloads (proof-easy-config) "proof-easy-config" "generic/proof-easy-config.el")
+
+(autoload 'proof-easy-config "proof-easy-config" "\
+Configure Proof General for proof-assistant using BODY as a setq body." nil 'macro)
+
+;;;***
+
+;;;### (autoloads (proof-indent-line) "proof-indent" "generic/proof-indent.el")
+
+(autoload 'proof-indent-line "proof-indent" "\
+Indent current line of proof script" t nil)
+
+;;;***
+
+;;;### (autoloads (proof-menu-define-specific proof-menu-define-main proof-menu-define-keys) "proof-menu" "generic/proof-menu.el")
+
+(autoload 'proof-menu-define-keys "proof-menu" nil nil nil)
+
+(autoload 'proof-menu-define-main "proof-menu" nil nil nil)
+
+(autoload 'proof-menu-define-specific "proof-menu" nil nil nil)
+
+;;;***
+
+;;;### (autoloads nil "proof-script" "generic/proof-script.el")
+
+;;;***
+
+;;;### (autoloads (proof-shell-invisible-command proof-shell-wait proof-extend-queue proof-start-queue proof-shell-available-p proof-shell-live-buffer proof-shell-ready-prover) "proof-shell" "generic/proof-shell.el")
+
+(autoload 'proof-shell-ready-prover "proof-shell" "\
+Make sure the proof assistant is ready for a command.
+If QUEUEMODE is set, succeed if the proof shell is busy but
+has mode QUEUEMODE.
+Otherwise, if the shell is busy, give an error.
+No change to current buffer or point." nil nil)
+
+(autoload 'proof-shell-live-buffer "proof-shell" "\
+Return buffer of active proof assistant, or nil if none running." nil nil)
+
+(autoload 'proof-shell-available-p "proof-shell" "\
+Returns non-nil if there is a proof shell active and available.
+No error messages.  Useful as menu or toolbar enabler." nil nil)
+
+(autoload 'proof-start-queue "proof-shell" "\
+Begin processing a queue of commands in ALIST.
+If START is non-nil, START and END are buffer positions in the
+active scripting buffer for the queue region.
+
+This function calls `proof-append-alist'." nil nil)
+
+(autoload 'proof-extend-queue "proof-shell" "\
+Extend the current queue with commands in ALIST, queue end END.
+To make sense, the commands should correspond to processing actions
+for processing a region from (buffer-queue-or-locked-end) to END.
+The queue mode is set to 'advancing" nil nil)
+
+(autoload 'proof-shell-wait "proof-shell" "\
+Busy wait for proof-shell-busy to become nil, or for TIMEOUT seconds.
+Needed between sequences of commands to maintain synchronization,
+because Proof General does not allow for the action list to be extended
+in some cases.   May be called by proof-shell-invisible-command." nil nil)
+
+(autoload 'proof-shell-invisible-command "proof-shell" "\
+Send CMD to the proof process.  Add terminal string if necessary.
+By default, let the command be processed asynchronously.
+But if optional WAIT command is non-nil, wait for processing to finish
+before and after sending the command.
+If WAIT is an integer, wait for that many seconds afterwards." nil nil)
+
+;;;***
+
+;;;### (autoloads (proof-splash-display-screen) "proof-splash" "generic/proof-splash.el")
+
+(autoload 'proof-splash-display-screen "proof-splash" "\
+Save window config and display Proof General splash screen.
+Only do it if proof-splash-enable is non-nil." nil nil)
+
+;;;***
+
+;;;### (autoloads (proof-toolbar-setup) "proof-toolbar" "generic/proof-toolbar.el")
+
+(autoload 'proof-toolbar-setup "proof-toolbar" "\
+Initialize Proof General toolbar and enable it for the current buffer.
+If proof-mode-use-toolbar is nil, change the current buffer toolbar
+to the default toolbar." t nil)
+
+;;;***
+
+;;;### (autoloads (proof-x-symbol-configure proof-x-symbol-mode proof-x-symbol-decode-region proof-x-symbol-enable) "proof-x-symbol" "generic/proof-x-symbol.el")
+
+(autoload 'proof-x-symbol-enable "proof-x-symbol" "\
+Turn on or off support for x-symbol, initializing if necessary.
+Calls proof-x-symbol-toggle-clean-buffers afterwards." nil nil)
+
+(autoload 'proof-x-symbol-decode-region "proof-x-symbol" "\
+Call (x-symbol-decode-region A Z), if x-symbol support is enabled.
+This converts tokens in the region into X-Symbol characters." nil nil)
+
+(autoload 'proof-x-symbol-mode "proof-x-symbol" "\
+Turn on/off x-symbol mode in current buffer, from proof-x-symbol-enable.
+The X-Symbol minor mode is only useful in buffers where symbol input
+takes place (it isn't used for output-only buffers)." t nil)
+
+(autoload 'proof-x-symbol-configure "proof-x-symbol" "\
+Configure the current buffer (goals or response) for X-Symbol." nil nil)
+
+;;;***
+
+;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "generic/texi-docstring-magic.el")
+
+(autoload 'texi-docstring-magic "texi-docstring-magic" "\
+Update all texi docstring magic annotations in buffer." t nil)
+
+;;;***
+
+(provide 'proof-autoloads)
diff --git a/generic/proof-compat.el b/generic/proof-compat.el
new file mode 100644
index 00000000..defb1b51
--- /dev/null
+++ b/generic/proof-compat.el
@@ -0,0 +1,119 @@
+;; proof-comapt.el   Operating system and Emacs version compatibility
+;;
+;; Copyright (C) 2000 LFCS Edinburgh. 
+;;
+;; Author:      David Aspinall <da@dcs.ed.ac.uk> and others
+;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;;
+;; $Id$
+;;
+;; This file collects together compatibility hacks for different
+;; operating systems and Emacs versions.  This is to help keep
+;; track of them.
+;;
+;; The development policy for Proof General is for the main codebase
+;; to be written for the latest stable version of XEmacs.  We follow
+;; XEmacs advice on removing obsolete function calls.
+;;
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Architecture flags
+;;;
+
+(eval-and-compile
+(defvar proof-running-on-XEmacs (string-match "XEmacs" emacs-version)
+  "Non-nil if Proof General is running on XEmacs.")
+;; rough test for XEmacs on win32, anyone't know about FSF there?
+(defvar proof-running-on-win32 (fboundp 'win32-long-file-name)
+  "Non-nil if Proof General is running on a win32 system."))
+
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; XEmacs compatibility
+;;;
+
+;; browse-url function isn't autoloaded in XEmacs 20.4
+(or (fboundp 'browse-url)
+    (autoload 'browse-url "browse-url"
+      "Ask a WWW browser to load URL." t))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; FSF compatibility
+;;;
+
+;; These days cl is dumped with XEmacs (20.4,21.1) but not FSF Emacs
+;; 20.2.  Would rather it was autoloaded but the autoloads are broken
+;; in FSF so we load it now.
+(require 'cl)				
+
+;; Give a warning,
+
+(or (fboundp 'warn)
+(defun warn (str &rest args)
+      "Issue a warning STR.  Defined by PG for FSF compatibility."
+      (apply 'message str args)
+      (sit-for 2)))
+
+;; Modeline redrawing (actually force-mode-line-update is alias on XEmacs)
+
+(or (fboundp 'redraw-modeline)
+(defun redraw-modeline (&rest args)
+  "Dummy function for Proof General on FSF Emacs."
+  (force-mode-line-update)))
+
+;; Interactive flag
+(or (fboundp 'noninteractive)
+    (defun noninteractive ()
+      "Dummy function for Proof General on FSF Emacs."
+      nil)) ;; pretend always interactive.
+
+      
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Old Emacs version compatibility
+;;;
+
+;; Create a menu from a customize group, for older/non-existent customize
+
+(or (fboundp 'customize-menu-create)
+(defun customize-menu-create (&rest args)
+  "Dummy function for PG; please upgrade your Emacs."
+  nil))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; General Emacs version compatibility
+;;;
+
+
+;; These are internal functions of font-lock, autoload policy
+;; differs between Emacs versions
+
+(or (fboundp 'font-lock-set-defaults)
+    (autoload 'font-lock-set-defaults "font-lock"))
+(or (fboundp 'font-lock-fontify-region)
+    (autoload 'font-lock-fontify-region "font-lock"))
+(or (fboundp 'font-lock-append-text-property)
+    (autoload 'font-lock-append-text-property "font-lock"))
+
+
+;; FIXME: todo: keybinding compat here, esp for mouse.
+;; See Isamode and emu.el for ideas.
+
+	    
+
+
+
+;; End of proof-compat.el
+(provide 'proof-compat)
\ No newline at end of file
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
new file mode 100644
index 00000000..6c392faa
--- /dev/null
+++ b/generic/proof-menu.el
@@ -0,0 +1,340 @@
+;; proof-menu.el  Menu and keymaps for Proof General
+;;
+;; Copyright (C) 2000 LFCS Edinburgh. 
+;; Authors:  David Aspinall
+;;
+;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;;
+;; $Id$
+;;
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Key bindings
+;;;
+
+;;;###autoload
+(defun proof-menu-define-keys (map)
+(define-key map [(control c) a] proof-assistant-keymap)
+(define-key map [(control c) (control a)] 'proof-goto-command-start)
+(define-key map [(control c) (control b)] 'proof-process-buffer)
+; C-c C-c is proof-interrupt-process in universal-keys
+(define-key map [(control c) (control e)] 'proof-goto-command-end)
+(define-key map [(control c) (control n)] 'proof-assert-next-command-interactive)
+(define-key map [(control c) (control p)] 'proof-prf)
+(define-key map [(control c) (control r)] 'proof-retract-buffer)
+(define-key map [(control c) (control s)] 'proof-toggle-active-scripting)
+(define-key map [(control c) (control t)] 'proof-ctxt)
+(define-key map [(control c) (control u)] 'proof-undo-last-successful-command)
+(define-key map [(control c) (control backspace)] 'proof-undo-and-delete-last-successful-command)
+; C-c C-v is proof-minibuffer-cmd in universal-keys
+(define-key map [(control c) (control z)] 'proof-frob-locked-end)
+(define-key map [(control c) (control ?.)] 'proof-goto-end-of-locked)
+(define-key map [(control c) (control return)] 'proof-goto-point)
+(cond ((string-match "XEmacs" emacs-version)
+(define-key map [(control button3)]	  'proof-mouse-goto-point)
+(define-key map [(control button1)]	  'proof-mouse-track-insert)) ; no FSF
+      (t 
+(define-key map [mouse-3]		  'proof-mouse-goto-point))) ; FSF
+;; NB: next binding overwrites comint-find-source-code.  
+(define-key map [(control c) (control f)] 'proof-find-theorems)
+(define-key map [(control c) (control h)] 'proof-help)
+;; FIXME: not implemented yet 
+;; (define-key map [(meta p)]		  'proof-previous-matching-command)
+;; (define-key map [(meta n)]		  'proof-next-matching-command)
+;; Deprecated bindings
+;(define-key map [(control c) return] 'proof-assert-next-command)
+;(define-key map [(control c) ?u] 'proof-retract-until-point-interactive)
+;; Add the universal keys bound in all PG buffers.
+(proof-define-keys map proof-universal-keys))
+
+
+
+
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Functions to define the menus
+;;;
+
+;; The main Proof-General generic menu
+
+;;;###autoload
+(defun proof-menu-define-main ()
+  (easy-menu-define 
+   proof-mode-menu  
+   proof-mode-map
+   "The main Proof General menu"
+   (cons proof-general-name
+	 (append
+	  proof-toolbar-scripting-menu
+	  proof-menu
+	  (list "----")
+	  (append
+	   (customize-menu-create 'proof-general)
+	   (customize-menu-create 'proof-general-internals "Internals"))
+	  proof-bug-report-menu))))
+
+
+;; The proof assistant specific menu
+
+;;;###autoload
+(defun proof-menu-define-specific ()
+  (easy-menu-define 
+   proof-assistant-menu 
+   proof-mode-map
+   (concat "The menu for " proof-assistant)
+   (cons proof-assistant
+	 (append
+	  proof-assistant-menu-entries
+	  proof-assistant-favourites
+	  '("----")
+	  '(["Add favourite" 
+	     (call-interactively 'proof-add-favourite) t])))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Contents of the generic menus
+;;;
+
+
+(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)))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Contents of the generic menus
+;;;
+
+(defvar proof-help-menu
+  `("Help"
+    [,(concat proof-assistant " information")
+     (proof-help) t]
+    [,(concat proof-assistant " web page")
+     (browse-url proof-assistant-home-page) t]
+    ["Proof General home page"
+     (browse-url proof-general-home-page) t]
+    ["Proof General Info"
+     (info "ProofGeneral") t]
+    )
+  "Proof General help menu.")
+
+(defvar proof-buffer-menu
+  '("Buffers"
+    ["Active scripting"
+     (proof-switch-to-buffer proof-script-buffer)
+     :active (buffer-live-p proof-script-buffer)]
+    ["Goals"
+     (proof-switch-to-buffer proof-goals-buffer t)
+     :active (buffer-live-p proof-goals-buffer)]
+    ["Response"
+     (proof-switch-to-buffer proof-response-buffer t)
+     :active (buffer-live-p proof-response-buffer)]
+    ["Shell"
+     (proof-switch-to-buffer proof-shell-buffer)
+     :active (buffer-live-p proof-shell-buffer)])
+  "Proof General buffer menu.")
+
+;; Make the togglers used in options menu below
+
+(proof-deftoggle proof-dont-switch-windows)
+(proof-deftoggle proof-delete-empty-windows)
+(fset 'proof-multiple-frames-toggle
+      (proof-customize-toggle proof-multiple-frames-enable))
+(fset 'proof-output-fontify-toggle
+      (proof-customize-toggle proof-output-fontify-enable))
+(fset 'proof-x-symbol-toggle
+      (proof-customize-toggle proof-x-symbol-enable))
+
+(defvar proof-quick-opts-menu
+  `("Options"
+    ["Don't switch windows" proof-dont-switch-windows-toggle
+     :style toggle
+     :selected proof-dont-switch-windows]
+    ["Delete empty windows" proof-delete-empty-windows-toggle
+     :style toggle
+     :selected proof-delete-empty-windows]
+    ["Multiple frames" proof-multiple-frames-toggle
+     :style toggle
+     :selected proof-multiple-frames-enable]
+    ["Output highlighting" proof-output-fontify-toggle
+     :active t
+     :style toggle
+     :selected proof-output-fontify-enable]
+    ["Toolbar" proof-toolbar-toggle
+     :active (and (featurep 'toolbar) 
+		  (boundp 'proof-buffer-type)
+		  (eq proof-buffer-type 'script))
+     :style toggle
+     :selected proof-toolbar-enable]
+    ["X-Symbol" proof-x-symbol-toggle
+     :active (proof-x-symbol-support-maybe-available)
+     :style toggle
+     :selected proof-x-symbol-enable]
+    ("Follow mode" 
+     ["Follow locked region" 
+      (customize-set-variable 'proof-follow-mode 'locked)
+     :style radio
+     :selected (eq proof-follow-mode 'locked)]
+     ["Keep locked region displayed" 
+      (customize-set-variable 'proof-follow-mode 'follow)
+     :style radio
+     :selected (eq proof-follow-mode 'follow)]
+     ["Never move" 
+      (customize-set-variable 'proof-follow-mode 'ignore)
+     :style radio
+     :selected (eq proof-follow-mode 'ignore)]))
+  "Proof General quick options.")
+
+(defvar proof-shared-menu
+  (append
+    (list
+     (vector
+      (concat "Start " proof-assistant)
+      'proof-shell-start
+      ':active '(not (proof-shell-live-buffer)))
+     (vector
+      (concat "Exit " proof-assistant)
+      'proof-shell-exit
+      ':active '(proof-shell-live-buffer)))
+    (list proof-buffer-menu)
+    (list proof-quick-opts-menu)
+    (list proof-help-menu))
+  "Proof General menu for various modes.")
+
+(defvar proof-bug-report-menu
+  (list
+   "----"
+   ["Submit bug report"
+    proof-submit-bug-report
+    :active t])
+  "Proof General menu for submitting bug report (one item plus separator).")
+
+(defvar proof-menu  
+  (append '("----"
+	    ["Scripting active" proof-toggle-active-scripting
+	     :style toggle
+	     :selected (eq proof-script-buffer (current-buffer))]
+	    ["Electric terminator" proof-electric-terminator-toggle
+	     :style toggle
+             :selected proof-electric-terminator-enable]
+	    ["Function menu" function-menu
+	     :active (fboundp 'function-menu)]
+	    "----")
+          proof-shared-menu)
+  "The Proof General generic menu.")
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Favourites mechanism for specific menu
+;;;
+
+
+(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 ()
+     (concat "Shortcut command to insert " ,string " into the current buffer.")
+     (interactive)
+     (proof-insert ,string)))
+
+(defmacro proof-definvisible (fn string &optional key)
+  "Define function FN to send STRING to proof assistant, optional keydef KEY.
+This is intended for defining proof assistant specific functions.
+STRING is sent using proof-shell-invisible-command, which see.
+KEY is added onto proof-assistant map."
+  (if key
+      (eval
+       `(define-key proof-assistant-keymap ,key (quote ,fn))))
+  `(defun ,fn ()
+     (concat "Command to send " ,string " to the proof assistant.")
+     (interactive)
+     (proof-shell-invisible-command ,string)))
+
+
+;;; Code for adding "favourites" to the proof-assistant specific menu
+
+(defvar proof-make-favourite-cmd-history nil
+  "History for proof-make-favourite.")
+
+(defun proof-add-favourite (command inscript menuname &optional key)
+  "Define and add a \"favourite\" proof-assisant function to the menu bar.
+The favourite function will issue COMMAND to the proof assistant.  
+COMMAND is inserted into script (not sent immediately) if INSCRIPT non-nil.
+MENUNAME is the name of the function for the menu.
+KEY is the optional key binding
+This function defines a function and returns a menu entry 
+suitable for adding to the proof assistant menu."
+  (interactive 
+   (list
+    (read-string (concat "Command to send to " proof-assistant ": ") nil 
+		 proof-make-favourite-cmd-history)
+    (y-or-n-p "Should command be recorded in script? ")
+    (read-string "Name of command on menu: ")
+    (if (y-or-n-p "Set a keybinding for this command? : ")
+	(read-key-sequence "Type the key to use (I recommend C-c a <key>): " nil t))))
+  (let* ((menunames	(split-string (downcase menuname)))
+	 (menuname-sym  (proof-sym (proof-splice-separator "-" menunames)))
+	 (menu-fn	menuname-sym) (i 1))
+    (while (fboundp menu-fn)
+      (setq menu-fn (intern (concat (symbol-name menuname-sym)
+				    "-" (int-to-string i))))
+      (incf i))
+    (if inscript
+	`(proof-defshortcut ,menu-fn ,command ,key)
+      `(proof-definvisible ,menu-fn ,command ,key))
+    (let ((menu-entry (vector menuname menu-fn t)))
+      (customize-save-variable 'proof-assistant-menu-entries
+			       (append proof-assistant-menu-entries 
+				       (list menu-entry)))
+      ;; Unfortunately, (easy-menu-add-item proof-assistant-menu nil ..)
+      ;; seems buggy, it adds to main menu. But with "Coq" argument 
+      ;; for path it adds a submenu!   The item argument seems to be
+      ;; something special, but no way to make an item for adding
+      ;; an ordinary item?!
+      (easy-menu-add-item proof-assistant-menu 
+			  '("Favourites")
+			  menu-entry 
+			  "Add favourite"))))
+
+
+
+(provide 'proof-menu)
+;; proof-menu.el ends here.
diff --git a/generic/span.el b/generic/span.el
new file mode 100644
index 00000000..59710e1f
--- /dev/null
+++ b/generic/span.el
@@ -0,0 +1,20 @@
+;; span.el	Datatype of "spans" for Proof General.
+;; Copyright (C) 1998 LFCS Edinburgh
+;; Author:	Healfdene Goguen
+;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;;
+;; $Id$
+
+
+;; Spans are our abstraction of extents/overlays.
+;; 
+(eval-and-compile
+  (cond
+   ((fboundp 'make-extent)    (require 'span-extent))
+   ((fboundp 'make-overlay)   (require 'span-overlay))
+   (t			       
+    (error 
+     "Your Emacs version is not compatible with Proof General, sorry."))))
+
+(provide 'span)
+;; span.el ends here.