aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-24 09:51:53 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-24 09:51:53 +0000
commit76d6b0b2b1f039549d308a0d2c478a6b05869af9 (patch)
tree78cc7e13bf290a17e7006a6d4616a8a08e36ce8f /generic
parent8f8e9388b582ad6d3ee6e1eea842a8d443d4ce89 (diff)
Merge changes from Version4Branch.
Diffstat (limited to 'generic')
-rw-r--r--generic/pg-assoc.el260
-rw-r--r--generic/pg-custom.el75
-rw-r--r--generic/pg-goals.el185
-rw-r--r--generic/pg-pbrpm.el14
-rw-r--r--generic/pg-response.el128
-rw-r--r--generic/pg-thymodes.el2
-rw-r--r--generic/pg-user.el148
-rw-r--r--generic/pg-xml.el10
-rw-r--r--generic/proof-autoloads.el164
-rw-r--r--generic/proof-auxmodes.el13
-rw-r--r--generic/proof-config.el370
-rw-r--r--generic/proof-easy-config.el4
-rw-r--r--generic/proof-maths-menu.el3
-rw-r--r--generic/proof-menu.el115
-rw-r--r--generic/proof-script.el197
-rw-r--r--generic/proof-shell.el166
-rw-r--r--generic/proof-site.el21
-rw-r--r--generic/proof-splash.el180
-rw-r--r--generic/proof-syntax.el8
-rw-r--r--generic/proof-toolbar.el527
-rw-r--r--generic/proof-unicode-tokens.el144
-rw-r--r--generic/proof-utils.el274
-rw-r--r--generic/proof-x-symbol.el337
-rw-r--r--generic/proof.el3
24 files changed, 816 insertions, 2532 deletions
diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index 9f8b46bd..1a1dcd23 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -18,8 +18,6 @@
(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
@@ -57,263 +55,5 @@ Dead or nil buffers are not represented in the list."
(setq bufs (cdr bufs)))
wins))
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Manipulating prover output
-;;
-
-(defun pg-assoc-strip-subterm-markup (string)
- "Return STRING with subterm and pbp annotations removed.
-Special annotations are characters with codes higher than
-'pg-subterm-first-special-char'.
-If pg-subterm-first-special-char is unset, return STRING unchanged."
- (if pg-subterm-first-special-char
- (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x )))
- (while (< ip l)
- (if (>= (aref string ip) pg-subterm-first-special-char)
- (if (and pg-subterm-start-char
- (char-equal (aref string ip) pg-subterm-start-char))
- (progn (incf ip)
- ;; da: this relies on annotations being
- ;; characters between \200 and first special
- ;; char (e.g. \360). Why not just look for
- ;; the sep char??
- (while
- (< (aref string ip)
- pg-subterm-first-special-char)
- (incf ip))))
- (aset out op (aref string ip))
- (incf op))
- (incf ip))
- (substring out 0 op))
- string))
-
-(defvar pg-assoc-ann-regexp nil
- "Cache of regexp for `pg-assoc-strip-subterm-markup-buf'.")
-
-(defun pg-assoc-strip-subterm-markup-buf (start end)
- "Remove subterm and pbp annotations from region."
- (if pg-subterm-start-char
- (progn
- (unless pg-assoc-ann-regexp
- (setq pg-assoc-ann-regexp
- (concat
- (regexp-quote (char-to-string pg-subterm-start-char))
- "[^"
- (regexp-quote (char-to-string pg-subterm-sep-char))
- "]*"
- (regexp-quote (char-to-string pg-subterm-sep-char)))))
- (save-restriction
- (narrow-to-region start end)
- (goto-char start)
- (proof-replace-regexp pg-assoc-ann-regexp "")
- (goto-char start)
- (proof-replace-string (char-to-string pg-subterm-end-char) "")
- (goto-char start)
- (if pg-topterm-regexp
- (proof-replace-regexp pg-topterm-regexp ""))))))
-
-
-(defun pg-assoc-strip-subterm-markup-buf-old (start end)
- "Remove subterm and pbp annotations from region START END."
- (let (c)
- (goto-char start)
- (while (< (point) end)
- ;; FIXME: small OBO here: if char at end is special
- ;; it won't be removed.
- (if (>= (setq c (char-after (point)))
- pg-subterm-first-special-char)
- (progn
- (delete-char 1)
- (decf end)
- (if (char-equal c pg-subterm-start-char)
- (progn
- ;; FIXME: could simply replace this by replace
- ;; match, matching on sep-char??
- (while (and (< (point) end)
- (< (char-after (point))
- pg-subterm-first-special-char))
- (delete-char 1)
- (decf end)))))
- (forward-char)))
- end))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;;
-;;; Subterm and PBP markup (goals and possibly response buffer)
-;;;
-
-(defconst pg-assoc-active-area-keymap
- (let ((map (make-sparse-keymap)))
- (if (featurep 'xemacs)
- (define-key map [(button1)] 'pg-goals-button-action)
- (define-key map [mouse-1] 'pg-goals-button-action))
- map))
-
-(defun pg-assoc-make-top-span (start end)
- "Make a top span (goal/hyp area) for mouse active output in START END."
- (let (span typname)
- (goto-char start)
- ;; skip the pg-topterm-regexp itself
- (if (looking-at pg-topterm-regexp)
- (forward-char (- (match-end 0) (match-beginning 0))))
- ;; typname is expected to be a cons-cell of a type (goal/hyp)
- ;; with a name, retrieved from the text immediately following
- ;; the topterm-regexp annotation.
- (let ((topterm (point)))
- (setq typname (funcall pg-topterm-goalhyplit-fn)) ;; should be non-nil!
- (goto-char topterm))
- (setq start (point))
- (if (eq (car-safe typname) 'lit)
- ;; Use length of literal command for end point
- (forward-char (length (cdr typname)))
- ;; Otherwise, use start/end of line before next annotation/buffer end
- (goto-char start)
- (beginning-of-line)
- (setq start (point))
- (goto-char end) ;; next annotation/end of buffer
- (beginning-of-line)
- (backward-char))
- (setq span (span-make start (point)))
- (span-set-property span 'mouse-face 'highlight)
- (span-set-property span 'face 'proof-active-area-face)
- (span-set-property span 'proof-top-element typname)
- (set-span-keymap span pg-assoc-active-area-keymap)
- (span-set-property span 'help-echo
- (if (eq (current-buffer) proof-goals-buffer)
- "mouse-1: proof-by-pointing action"
- "mouse-1: copy-paste and send back to prover"))))
-
-
-
-
-(defun pg-assoc-analyse-structure (start end)
- "Analyse the region between START and END for subterm and PBP markup.
-
-For subterms, we can make nested regions in the concrete syntax into
-active mouse-highlighting regions, each of which can be used to
-communicate a selected term back to the prover. The output text is
-marked up with the annotation scheme:
-
- [ <annotation> | <subterm/concrete> ]
-
- ^ ^ ^
- | | |
-pg-subterm-start-char pg-subterm-sep-char pg-subterm-end-char
-
-The annotation is intended to indicate a node in the abstract syntax
-tree inside the prover, which can be used to pick out the internal
-representation of the term itself. We assume that the annotation
-takes the form of a sequence of characters:
-
- <length of shared prefix previous> <ann1> <ann2> .. <annN>
-
-Where each element <..> is a character which is *less* than
-pg-subterm-first-special-char, but *greater* than 128. Each
-character code has 128 subtracted to yield a number. The first
-character allows a simple optimisation by sharing a prefix of
-the previous (left-to-right) subterm's annotation. (See the
-variable `pg-subterm-anns-use-stack' for an alternative
-optimisation.)
-
-For subterm markup without communication back to the prover, the
-annotation is not needed, but the first character must still be given.
-
-For proof-by-pointing (PBP) oriented markup, `pg-topterm-regexp' and
-`pg-topterm-goalhyplit-fn' should be set. Together these allow
-further active regions to be defined, corresponding to \"top elements\"
-in the proof-state display. A \"top element\" is currently assumed
-to be either a hypothesis or a subgoal, and is assumed to occupy
-a line (or at least a line). The markup is simply
-
- & <goal or hypthesis line in proof state>
- ^
- |
- pg-topterm-regexp
-
-And the function `pg-topterm-goalhyplit-fn' is called to do the
-further analysis, to return an indication of the goal/hyp and
-record a name value. These values are used to construct PBP
-commands which can be sent to the prover."
- (if (or pg-subterm-start-char pg-topterm-regexp) ;; markup for topterm alone
- (let*
- ((cur start)
- (len (- end start))
- (ann (make-string len ?x)) ; (more than) enough space for longest ann'n
- (ap 0)
- c stack topl span)
-
- (while (< cur end)
- (setq c (char-after cur))
- (cond
- ;; Seen goal regexp: this is the start of a top extent
- ;; (assumption, goal, literal command)
- ((save-excursion
- (goto-char cur)
- (looking-at pg-topterm-regexp))
- (setq topl (cons cur topl))
- (setq ap 0))
-
- ;; Seen subterm start char: it's followed by a char
- ;; indicating the length of the annotation prefix
- ;; which can be shared with the previous subterm.
- ((and pg-subterm-start-char ;; ignore if subterm start not set
- (= c pg-subterm-start-char))
- (incf cur)
- (if pg-subterm-anns-use-stack
- (setq ap (- ap (- (char-after cur) 128)))
- (setq ap (- (char-after cur) 128)))
- (incf cur)
- ;; Now search for a matching end-annotation char, recording the
- ;; annotation found.
- (while (not (= (setq c (char-after cur)) pg-subterm-sep-char))
- (aset ann ap (- c 128))
- (incf ap)
- (incf cur))
- ;; Push the buffer pos and annotation
- (setq stack (cons cur
- (cons (substring ann 0 ap) stack))))
-
- ;; Seen a subterm end char, terminating an annotated region
- ;; in the concrete syntax. We make a highlighting span now.
- ((and (consp stack) (= c pg-subterm-end-char))
- ;; (consp stack) added to make the code more robust.
- ;; [ Condition violated with lego/example.l and GNU Emacs 20.3 ]
- (setq span (span-make (car stack) cur))
- (span-set-property span 'mouse-face 'highlight)
- (span-set-property span 'goalsave (cadr stack));; FIXME: 'goalsave?
- ;; (span-set-property span 'balloon-help helpmsg)
- (span-set-property span 'help-echo 'pg-goals-get-subterm-help)
- (if pg-subterm-anns-use-stack
- ;; Pop annotation off stack
- (progn
- (setq ap 0)
- (while (< ap (length (cadr stack)))
- (aset ann ap (aref (cadr stack) ap))
- (incf ap))))
- ;; Finish popping annotations
- (setq stack (cdr (cdr stack)))))
- ;; On to next char
- (incf cur))
-
- ;; List of topterm beginning positions (goals/hyps) found
- (setq topl (reverse (cons end topl)))
-
- ;; Proof-by-pointing markup assumes "top" elements which define a
- ;; context for a marked-up (sub)term: we assume these contexts to
- ;; be either a subgoal to be solved or a hypothesis.
- ;; Top element spans are only made if pg-topterm-goalhyplit-fn is set.
- ;; NB: If we want Coq pbp: (setq coq-current-goal 1)
- (if pg-topterm-goalhyplit-fn
- (while (setq ap (car topl)
- topl (cdr topl))
- (pg-assoc-make-top-span ap (car topl))))
-
- ;; Finally: strip the specials. This should
- ;; leave the spans in exactly the right place.
- (pg-assoc-strip-subterm-markup-buf start end))))
-
-
-
(provide 'pg-assoc)
;;; pg-assoc.el ends here
diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index ddf0be01..8fc5158b 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -29,21 +29,6 @@
(require 'proof-utils) ; defpgcustom
(require 'proof-config) ; for proof-toolbar-entries-default
-(defpgcustom x-symbol-enable nil
- "*Whether to use x-symbol in Proof General for this assistant.
-If you activate this variable, whether or not you really get x-symbol
-support depends on whether your proof assistant supports it and
-whether X-Symbol is installed in your Emacs."
- :type 'boolean
- :set 'proof-set-value
- :group 'proof-user-options)
-
-;; todo: can remove this one now, rename isabelle-x-symbol -> isar-x-symbol
-(defpgcustom x-symbol-language proof-assistant-symbol
- "Setting for x-symbol-language for the current proof assistant.
-It defaults to proof-assistant-symbol, which makes X Symbol
-look for files named x-symbol-<PA>.el.")
-
(defpgcustom maths-menu-enable nil
"*Non-nil for Unicode maths menu in Proof General for this assistant."
:type 'boolean
@@ -56,12 +41,6 @@ look for files named x-symbol-<PA>.el.")
:set 'proof-set-value
:group 'proof-user-options)
-(defpgcustom unicode-tokens2-enable nil
- "*Non-nil for using Unicode token input mode in Proof General."
- :type 'boolean
- :set 'proof-set-value
- :group 'proof-user-options)
-
(defpgcustom mmm-enable nil
"*Whether to use MMM Mode in Proof General for this assistant.
MMM Mode allows multiple modes to be used in the same buffer.
@@ -77,32 +56,25 @@ support depends on whether your proof assistant supports it."
:group 'proof-user-options)
(defconst proof-toolbar-entries-default
- `((state "Display Proof State" "Display the current proof state" t
- proof-showproof-command)
- (context "Display Context" "Display the current context" t
- proof-context-command)
-;; PG 3.7: disable goal & qed, they're not so useful (& save-command never enabled).
-;; (goal "Start a New Proof" "Start a new proof" t
-;; proof-goal-command)
- (retract "Retract Buffer" "Retract (undo) whole buffer" t)
- (undo "Undo Step" "Undo the previous proof command" t)
- (delete "Delete Step" nil t)
- (next "Next Step" "Process the next proof command" t)
- (use "Use Buffer" "Process whole buffer" t)
- (goto "Goto Point" "Process or undo to the cursor position" t)
-;; (qed "Finish Proof" "Close/save proved theorem" t
-;; proof-save-command)
- (lockedend "Goto Locked End" nil t)
- (find "Find Theorems" "Find theorems" t proof-find-theorems-command)
- (command "Issue Command" "Issue a non-scripting command" t)
- (interrupt "Interrupt Prover" "Interrupt the proof assistant" t)
- (restart "Restart Scripting" "Restart scripting (clear all locked regions)" t)
- (visibility "Toggle Visibility" nil t)
-; PG 3.6: remove Info item from toolbar; it's not very useful and under PA->Help anyway
-; (info nil "Show online proof assistant information" t
-; proof-info-command)
-; PG 3.7: use Info icon for info
- (info nil "Proof General manual" t))
+ `((state "Display Proof State" "Display the current proof state" t
+ proof-showproof-command)
+ (context "Display Context" "Display the current context" t
+ proof-context-command)
+ (goal "Start a New Proof" "Start a new proof" t nil)
+ (retract "Retract Buffer" "Retract (undo) whole buffer" t)
+ (undo "Undo Step" "Undo the previous proof command" t)
+ (delete "Delete Step" "Delete the last proof command" t)
+ (next "Next Step" "Process the next proof command" t)
+ (use "Use Buffer" "Process whole buffer" t)
+ (goto "Goto Point" "Process or undo to the cursor position" t)
+ (qed "Finish Proof" "Close/save proved theorem" t nil)
+ (lockedend "Goto Locked End" "Goto end of the last command proceesed" nil t)
+ (find "Find Theorems" "Find theorems" t proof-find-theorems-command)
+ (command "Issue Command" "Issue a non-scripting command" nil)
+ (interrupt "Interrupt Prover" "Interrupt the proof assistant" t)
+ (restart "Restart Scripting" "Restart scripting (clear all locked regions)" t)
+ (visibility "Toggle Visibility" "Show or hide hidden proofs" nil t)
+ (help nil "Proof General manual" t t))
"Example value for proof-toolbar-entries. Also used to define scripting menu.
This gives a bare toolbar that works for any prover, providing the
appropriate configuration variables are set.
@@ -112,18 +84,19 @@ defining functions, images.")
(defpgcustom toolbar-entries proof-toolbar-entries-default
"List of entries for Proof General toolbar and Scripting menu.
-Format of each entry is (TOKEN MENUNAME TOOLTIP DYNAMIC-ENABLER-P ENABLE).
+Format of each entry is (TOKEN MENUNAME TOOLTIP TOOLBAR-P [VISIBLE-P]).
For each TOKEN, we expect an icon with base filename TOKEN,
a function proof-toolbar-<TOKEN>, and (optionally) a dynamic enabler
proof-toolbar-<TOKEN>-enable-p.
-If ENABLEP is absent, item is enabled; if ENABLEP is present, item
-is only added to menubar and toolbar if ENABLEP is non-null.
+If VISIBLE-P is absent, or evaluates to non-nil, the item will
+appear on the toolbar or menu. If it evaluates to nil, the item
+is not shown.
If MENUNAME is nil, item will not appear on the scripting menu.
-If TOOLTIP is nil, item will not appear on the toolbar.
+If TOOLBAR-P is nil, item will not appear on the toolbar.
The default value is `proof-toolbar-entries-default' which contains
the standard Proof General buttons.")
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index acc68dd5..18f87577 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -8,15 +8,15 @@
;; $Id$
;;
+;;; Commentary:
+
;;; Code:
(eval-when-compile
(require 'easymenu) ; easy-menu-add, etc
(require 'cl) ; incf
(require 'span)) ; span-*
-;;; Commentary:
-
-(require 'proof)
+(require 'proof-utils)
(require 'pg-assoc)
(require 'bufhist)
@@ -33,8 +33,6 @@
May enable proof-by-pointing or similar features.
\\{proof-goals-mode-map}"
(setq proof-buffer-type 'goals)
- ;; font-lock-keywords isn't automatically buffer-local in Emacs 21.2
- (make-local-variable 'font-lock-keywords)
(add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
(easy-menu-add proof-goals-mode-menu proof-goals-mode-map)
(easy-menu-add proof-assistant-menu proof-goals-mode-map)
@@ -60,27 +58,14 @@ May enable proof-by-pointing or similar features.
;;
(define-key proof-goals-mode-map [q] 'bury-buffer)
-(cond
- ((featurep 'xemacs)
- (define-key proof-goals-mode-map [(button2)] 'pg-goals-button-action)
- (define-key proof-goals-mode-map [(control button2)] 'proof-undo-and-delete-last-successful-command)
- ;; button 2 is a nuisance on 2 button mice, so we'll do 1 as well.
- ;; Actually we better hadn't, people like to use it for cut and paste.
- ;; (define-key proof-goals-mode-map [(button1)] 'pg-goals-button-action)
- ;; (define-key proof-goals-mode-map [(control button1)] 'proof-undo-and-delete-last-successful-command)
- ;; C Raffalli: The next key on button3 will be remapped to proof by contextual
- ;; menu by pg-pbrpm.el. In this case, control button3 is mapped to
- ;; 'pg-goals-yank-subterm
- (define-key proof-goals-mode-map [(button3)] 'pg-goals-yank-subterm))
- (t
- (define-key proof-goals-mode-map [mouse-2] 'pg-goals-button-action)
- (define-key proof-goals-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command)
- ;; (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
- ;; (define-key proof-goals-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command)
- ;; C Raffalli: The next key on button3 will be remapped to proof by contextual
- ;; menu by pg-pbrpm.el. In this case, control button3 is mapped to
- ;; 'pg-goals-yank-subterm
- (define-key proof-goals-mode-map [mouse-3] 'pg-goals-yank-subterm)))
+(define-key proof-goals-mode-map [mouse-2] 'pg-goals-button-action)
+(define-key proof-goals-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command)
+;; (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
+;; (define-key proof-goals-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command)
+;; C Raffalli: The next key on button3 will be remapped to proof by contextual
+;; menu by pg-pbrpm.el. In this case, control button3 is mapped to
+;; 'pg-goals-yank-subterm
+(define-key proof-goals-mode-map [mouse-3] 'pg-goals-yank-subterm)
@@ -90,18 +75,15 @@ May enable proof-by-pointing or similar features.
;;;###autoload
(defun proof-goals-config-done ()
"Initialise the goals buffer after the child has been configured."
- (proof-font-lock-configure-defaults nil)
- (proof-x-symbol-config-output-buffer))
-
+ (setq font-lock-defaults '(proof-goals-font-lock-keywords)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Goals buffer processing
;;
(defun pg-goals-display (string)
- "Display STRING in the proof-goals-buffer, properly marked up.
-Converts term substructure markup into mouse-highlighted extents,
-and properly fontifies STRING using proof-fontify-region."
+ "Display STRING in the `proof-goals-buffer', properly marked up.
+Converts term substructure markup into mouse-highlighted extents."
(save-excursion
;; Response buffer may be out of date. It may contain (error)
;; messages relating to earlier proof states
@@ -127,22 +109,6 @@ and properly fontifies STRING using proof-fontify-region."
(unless (string-equal string "")
(insert string)
- (if pg-use-specials-for-fontify
- ;; With special chars for fontification, do that first,
- ;; but keep specials in case also used for subterm markup.
- (proof-fontify-region (point-min) (point-max) 'keepspecials))
-
- ;; Markup for PBP-style interaction. This currently only works
- ;; for special characters 128-255, which is inconsistent with
- ;; UTF-8 interaction.
- (unless proof-shell-unicode
- (pg-assoc-analyse-structure (point-min) (point-max)))
-
- (unless pg-use-specials-for-fontify
- ;; provers which use ordinary keywords to fontify output must
- ;; do fontification second after subterm specials are removed.
- (proof-fontify-region (point-min) (point-max)))
-
;; Record a cleaned up version of output string
(setq proof-shell-last-output
(buffer-substring (point-min) (point-max)))
@@ -153,129 +119,6 @@ and properly fontifies STRING using proof-fontify-region."
(proof-display-and-keep-buffer
proof-goals-buffer (point-min)))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Commands to prover based on subterm markup (inc PBP).
-;;
-;;
-
-;; Fairly specific to the mechanism implemented in LEGO
-;; To make (more) sense of this code, you should read the
-;; relevant LFCS tech report by tms, yb, and djs
-
-(defun pg-goals-yank-subterm (event)
- "Copy the subterm indicated by the mouse-click EVENT.
-This function should be bound to a mouse button in the Proof General
-goals buffer.
-
-The EVENT is used to find the smallest subterm around a point. The
-subterm is copied to the `kill-ring', and immediately yanked (copied)
-into the current buffer at the current cursor position.
-
-In case the current buffer is the goals buffer itself, the yank
-is not performed. Then the subterm can be retrieved later by an
-explicit yank."
- (interactive "e")
- (let (span)
- (save-window-excursion
- (save-excursion
- (mouse-set-point event)
- ;; Get either the proof body or whole goalsave
- (setq span (or
- (span-at (point) 'proof)
- (span-at (point) 'goalsave)))
- (if span (copy-region-as-kill
- (span-start span)
- (span-end span)))))
- (if (and span (not (eq proof-buffer-type 'goals)))
- (yank))))
-
-(defun pg-goals-button-action (event)
- "Construct a proof-by-pointing command based on the mouse-click EVENT.
-This function should be bound to a mouse button in the Proof General
-goals buffer.
-
-The EVENT is used to find the smallest subterm around a point. A
-position code for the subterm is sent to the proof assistant, to ask
-it to construct an appropriate proof command. The command which is
-constructed will be inserted at the end of the locked region in the
-proof script buffer, and immediately sent back to the proof assistant.
-If it succeeds, the locked region will be extended to cover the
-proof-by-pointing command, just as for any proof command the
-user types by hand."
- (interactive "e")
- (mouse-set-point event)
- (pg-goals-construct-command))
-
-;; Using the spans in a mouse behavior is quite simple: from the mouse
-;; position, find the relevant span, then get its annotation and
-;; produce a piece of text that will be inserted in the right buffer.
-
-(defun proof-expand-path (string)
- (let ((a 0) (l (length string)) ls)
- (while (< a l)
- (setq ls (cons (int-to-string
- (char-to-int (aref string a)))
- (cons " " ls)))
- (incf a))
- (apply 'concat (nreverse ls))))
-
-(defun pg-goals-construct-command ()
- "Examine the goals "
- (let* ((span (span-at (point) 'goalsave)) ;; goalsave means subgoal no/name
- (top-span (span-at (point) 'proof-top-element))
- (buf (current-buffer))
- top-info)
- (when top-span
- (setq top-info (span-property top-span 'proof-top-element))
- (pop-to-buffer proof-script-buffer)
- (cond
- (span
- (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 'goalsave))))))
- ((eq (car top-info) 'hyp)
- ;; Switch focus to another subgoal; a non-scripting command
- (proof-shell-invisible-command
- (format pbp-hyp-command (cdr top-info))))
- ((eq (car top-info) 'goal)
- ;; A scripting command to change goal
- (proof-insert-pbp-command
- (format pg-goals-change-goal (cdr top-info))))
- ((and
- ;; Literal command in one step, classic PBP protocol
- (eq (car top-info) 'lit)
- (equal buf proof-goals-buffer))
- (proof-insert-pbp-command (cdr top-info)))
- ((eq (car top-info) 'lit)
- (proof-insert-sendback-command (cdr top-info)))))))
-
-(defun pg-goals-get-subterm-help (spanorwin &optional obj pos)
- "Return a help string for subterm, called via 'help-echo property."
- (let ((span (or obj spanorwin))) ;; GNU Emacs vs XEmacs interface
- (if (and pg-subterm-help-cmd (span-live-p span))
- (or (span-property span 'cachedhelp) ;; already got
- (progn
- (if (proof-shell-available-p)
- (let ((result
- (proof-shell-invisible-cmd-get-result
- (format pg-subterm-help-cmd (span-string span))
- 'ignorerrors)))
- ;; FIXME: generalise, and make output readable
- ;; (fontify? does that work for GNU Emacs?
- ;; how can we do it away from a buffer?)
- (setq result
- (replace-in-string
- result
- (concat "\n\\|" pg-special-char-regexp) ""))
- (span-set-property span 'cachedhelp result)
- result)))))))
-
-
-
(provide 'pg-goals)
;;; pg-goals.el ends here
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index 2d6a757f..2138de08 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -234,18 +234,8 @@ The prover command is processed via pg-pbrpm-run-command."
"Cancel"
(lambda (n) (pg-pbrpm-erase-buffer-menu) (delete-frame)) nil))
;; needs to be fixed for other prover than phox
- ;; da: here's a possible fix, perhaps we can simply use
- ;; `proof-fontify-region' which has been configured
- ;; by phox mode appropriately with hooks (new second case).
- (cond
- ((featurep 'phox)
- (if phox-sym-lock-enabled
- (font-lock-fontify-buffer)
- (if phox-x-symbol-enable
- (x-symbol-decode))))
- (t
- (proof-fontify-region (point-min) (point-max))))
-
+ ;; da: I've removed code here, we should simply keep this
+ ;; buffer with font lock on.
(mapc 'span-read-only pg-pbrpm-spans)
(make-dialog-frame '(width 80 height 30)))
(beep)))))
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 83ed7af2..c3809974 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -41,8 +41,6 @@
(define-derived-mode proof-response-mode proof-universal-keys-only-mode
"PGResp" "Responses from Proof Assistant"
(setq proof-buffer-type 'response)
- ;; font-lock-keywords isn't automatically buffer-local in Emacs 21.2
- (make-local-variable 'font-lock-keywords)
(define-key proof-response-mode-map [(button2)] 'pg-goals-button-action)
(define-key proof-response-mode-map [q] 'bury-buffer)
(define-key proof-response-mode-map [c] 'pg-response-clear-displays)
@@ -66,9 +64,7 @@
;;;###autoload
(defun proof-response-config-done ()
"Complete initialisation of a response-mode derived buffer."
- (proof-font-lock-configure-defaults nil)
- (proof-x-symbol-config-output-buffer))
-
+ (setq font-lock-defaults '(proof-response-font-lock-keywords)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
@@ -77,42 +73,10 @@
;; -- three window mode
;;
-;; FIXME: 3.5: things are better than before but still quite bad.
-;; To really do this well I think we simply have to write specialised
-;; frame handling code --- and do it twice, once for each Emacs.
-;;
-;; Choice comment from XEmacs frame.el before special-display-popup-frame:
-;; "#### Change, not compatible with FSF: This stuff is all so incredibly
-;; junky anyway that I doubt it makes any difference."
-
(defvar pg-response-special-display-regexp nil
"Regexp for `special-display-regexps' for multiple frame use.
Internal variable, setting this will have no effect!")
-;; NB: this list uses XEmacs defaults in the non-multiframe case.
-;; We handle specifiers quit crudely, bute (1) to set for the
-;; frame specifically we'd need to get hold of the frame,
-;; (2) specifiers have been (still are) quite buggy.
-(defconst proof-multiframe-specifiers
- (if (featurep 'xemacs)
- (list
- (list has-modeline-p nil nil) ;; nil even in ordinary case.
- (list menubar-visible-p nil t)
- (list default-gutter-visible-p nil t)
- (list default-toolbar-visible-p nil t)))
- "List of XEmacs specifiers and their values for non-multiframe and multiframe.")
-
-(defun proof-map-multiple-frame-specifiers (multiframep locale)
- "Set XEmacs specifiers according to MULTIFRAMEP in LOCALE."
- (dolist (spec proof-multiframe-specifiers)
- ;; FIXME: Unfortunately these specifiers seem to get lost very
- ;; easily --- the toolbar, gutter, modeline all come back
- ;; for no good reason. Can we construct a simple bug example?
- (if (fboundp 'set-specifier) ; nuke compile warning
- (set-specifier (car spec)
- (if multiframep (cadr spec) (caddr spec))
- locale))))
-
(defconst proof-multiframe-parameters
'((minibuffer . nil)
(modeline . nil) ; ignored?
@@ -123,17 +87,9 @@ Internal variable, setting this will have no effect!")
"List of GNU Emacs frame parameters for secondary frames.")
(defun proof-multiple-frames-enable ()
- (if (featurep 'xemacs)
- (proof-map-buffers
- (proof-associated-buffers)
- (proof-map-multiple-frame-specifiers proof-multiple-frames-enable
- (current-buffer))))
- (let ((spdres
- (if (featurep 'xemacs)
- pg-response-special-display-regexp
- (cons ; GNU Emacs uses this to set frame params too, handily
- pg-response-special-display-regexp
- proof-multiframe-parameters))))
+ (let ((spdres (cons
+ pg-response-special-display-regexp
+ proof-multiframe-parameters)))
(if proof-multiple-frames-enable
(add-to-list 'special-display-regexps spdres)
(setq special-display-regexps
@@ -143,7 +99,6 @@ Internal variable, setting this will have no effect!")
(defun proof-three-window-enable ()
(proof-layout-windows))
-
(defun proof-select-three-b (b1 b2 b3 &optional nohorizontalsplit)
"Select three buffers. Put them into three windows, selecting the last one."
(interactive "bBuffer1:\nbBuffer2:\nbBuffer3:")
@@ -164,8 +119,6 @@ Internal variable, setting this will have no effect!")
(interactive)
(proof-select-three-b
(or proof-script-buffer (first (buffer-list)))
- ;; Pierre had response buffer first, I think goals
- ;; is a bit nicer though?
(if (buffer-live-p proof-goals-buffer)
proof-goals-buffer (first (buffer-list)))
(if (buffer-live-p proof-response-buffer)
@@ -207,7 +160,6 @@ For multiple frame mode, this function obeys the setting of
;; Restore an existing frame configuration (seems buggy, typical)
(if pg-frame-configuration
(set-frame-configuration pg-frame-configuration 'nodelete)))
- ;; Three window mode: use the Pierre-layout by default
(proof-three-window-enable
(proof-delete-other-frames)
(set-window-dedicated-p (selected-window) nil)
@@ -303,6 +255,17 @@ Returns non-nil if response buffer was cleared."
;; see the proof state and there is none
;; (Isabelle/Isar displays nothing: might be better if it did).
(proof-display-and-keep-buffer proof-response-buffer))
+
+
+;;
+;; Images for the response buffer
+;;
+;(defimage pg-response-error-image
+; ((:type xpm :file "/home/da/PG/images/epg-interrupt.xpm")))
+
+;(defimage pg-response-warning-image
+; ((:type xpm :file "/home/da/PG/images/epg-abort.xpm")))
+
;; TODO: this function should be combined with
;; pg-response-maybe-erase-buffer.
@@ -326,23 +289,13 @@ Returns non-nil if response buffer was cleared."
(setq start (point))
(insert str)
(unless (bolp) (newline))
-
- ;; Do pbp markup here, e.g. for "sendback" commands.
- ;; NB: we might loose if markup has been split between chunks, but this
- ;; will could only happen in cases of huge (spilled) output
- (pg-assoc-analyse-structure start (point-max))
-
- (proof-fontify-region start (point))
-
- ;; Fontify message: one reason why we don't keep the buffer in
- ;; font-lock minor mode is these properties would be lost.
- (if (and face proof-output-fontify-enable)
- (font-lock-append-text-property
- start (point-max) 'face face))
+ (when face
+ (overlay-put
+ (make-overlay start (point-max))
+ 'face face))
(set-buffer-modified-p nil))))))
-
(defun pg-response-clear-displays ()
"Clear Proof General response and tracing buffers.
You can use this command to clear the output from these buffers when
@@ -482,31 +435,33 @@ We fontify the output only if we're not too busy to do so."
(with-current-buffer proof-trace-buffer
(goto-char (point-max))
(newline)
- (or proof-trace-last-fontify-pos
- (setq proof-trace-last-fontify-pos (point)))
(insert str)
(unless (bolp)
- (newline))
- ;; If tracing output is prolific, we try to avoid
- ;; fontifying every chunk and batch it up instead.
- (unless pg-tracing-slow-mode
- (let ((fontifystart (proof-trace-fontify-pos)))
- ;; Catch errors here: this is to deal with ugly problem when
- ;; fontification of large output gives error Nesting too deep
- ;; for parser [see etc/isar/nesting-too-deep-for-parser.txt],
- ;; a serious flaw in XEmacs version of parse-partial-sexp
- (unwind-protect
- (proof-fontify-region fontifystart (point))
- (setq proof-trace-last-fontify-pos nil))
- (set-buffer-modified-p nil)))))
+ (newline))))
+;;; FIXME: reinstate this, turning font lock off then on, mebbe
+;;; (or proof-trace-last-fontify-pos
+;;; (setq proof-trace-last-fontify-pos (point)))
+;;; (insert str)
+;;; (unless (bolp)
+;;; (newline))
+;;; ;; If tracing output is prolific, we try to avoid
+;;; ;; fontifying every chunk and batch it up instead.
+;;; (unless pg-tracing-slow-mode
+;;; (let ((fontifystart (proof-trace-fontify-pos)))
+;;; ;; Catch errors, in case fontification buggy
+;;; (unwind-protect
+;;; (proof-fontify-region fontifystart (point))
+;;; (setq proof-trace-last-fontify-pos nil))
+;;; (set-buffer-modified-p nil)))))
(defun proof-trace-buffer-finish ()
"Complete fontification in tracing buffer now that there's time to do so."
- (let ((fontifystart (proof-trace-fontify-pos)))
- (if (and fontifystart (not quit-flag));; may be done already/user desparately trying to avoid
- (save-excursion
- (set-buffer proof-trace-buffer)
- (proof-fontify-region fontifystart (point-max))))))
+ )
+;;; (let ((fontifystart (proof-trace-fontify-pos)))
+;;; (if (and fontifystart (not quit-flag));; may be done already
+;;; (save-excursion
+;;; (set-buffer proof-trace-buffer)
+;;; (proof-fontify-region fontifystart (point-max))))))
@@ -530,7 +485,6 @@ We fontify the output only if we're not too busy to do so."
(setq start (point))
(insert str)
(unless (bolp) (newline))
- (proof-fontify-region start (point))
(set-buffer-modified-p nil))))
diff --git a/generic/pg-thymodes.el b/generic/pg-thymodes.el
index 333e8829..de4c31ca 100644
--- a/generic/pg-thymodes.el
+++ b/generic/pg-thymodes.el
@@ -53,7 +53,7 @@ All of these settings are optional."
(eval
`(define-derived-mode ,mode ,parentmode ,name
(interactive)
- (pg-do-unless-null ,flks (setq font-lock-keywords ,flks))
+ (pg-do-unless-null ,flks (setq font-lock-defaults (',flks)))
(pg-do-unless-null ,syntaxes (mapcar 'modify-syntax-entry ,syntaxes))))
;; Define the menu (final value of macro to be evaluated)
`(pg-do-unless-null ,menu
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 818afb78..2a8590f8 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1,4 +1,4 @@
-;; pg-user.el --- User level commands for Proof General
+;;; pg-user.el --- User level commands for Proof General
;;
;; Copyright (C) 2000-2008 LFCS Edinburgh.
;; Author: David Aspinall and others
@@ -29,7 +29,9 @@
;;
(defmacro proof-maybe-save-point (&rest body)
- "Save point according to proof-follow-mode, execute BODY."
+ "Save point according to `proof-follow-mode', execute BODY."
+ ;; FIXME: This duplicates the code of the body, which isn't wrong but
+ ;; is undesirable.
`(if (eq proof-follow-mode 'locked)
(progn
,@body)
@@ -90,17 +92,9 @@ you can use the usual `yank' and similar commands to retrieve the
deleted text."
(interactive)
(proof-undo-last-successful-command-1 'delete)
- ;; FIXME want to do this here for 3.3, for nicer behaviour
- ;; when deleting.
- ;; Unfortunately nasty problem with read only flag when
- ;; inserting at (proof-locked-end) sometimes behaves as if
- ;; point is inside locked region (prob because span is
- ;; [ ) and not [ ] -- why??).
- ;; (proof-script-new-command-advance)
+ ;; FIXME (proof-script-new-command-advance)
)
-;; No direct key-binding for this one: C-c C-u was too dangerous,
-;; when used quickly it's too easy to accidently delete!
(defun proof-undo-last-successful-command-1 (&optional delete)
"Undo last successful command at end of locked region.
If optional DELETE is non-nil, the text is also deleted from
@@ -200,18 +194,14 @@ handling of interrupt signals."
(interactive)
(let ((cmd (span-at (point) 'type)))
(if cmd (goto-char (span-end cmd))
-; (and (re-search-forward "\\S-" nil t)
-; (proof-assert-until-point nil 'ignore-proof-process))
(proof-assert-next-command nil
'ignore-proof-process
'dontmoveforward))
(skip-chars-backward " \t\n")
(unless (eq (point) (point-min))
- ;; should land on terminal char
(backward-char))))
-
;;
;; Mouse functions
;;
@@ -221,49 +211,13 @@ handling of interrupt signals."
;; be nicer behaviour than actually moving point into locked region
;; which is only useful for cut and paste, really.
(defun proof-mouse-goto-point (event)
- "Call proof-goto-point on the click position EVENT."
+ "Call `proof-goto-point' on the click position EVENT."
(interactive "e")
(proof-maybe-save-point
(mouse-set-point event)
(proof-goto-point)))
-;; FIXME da: this is an oddity. It copies the span, but does not
-;; send it, contrary to it's old name ("proof-send-span").
-;; Now made more general to behave like mouse-track-insert
-;; when not over a span.
-;; FIXME da: improvement would be to allow selection of part
-;; of command by dragging, as in ordinary mouse-track-insert.
-;; Maybe by setting some of the mouse track hooks.
-;; TODO: mouse-track-insert is XEmacs specific anyway.
-(defun proof-mouse-track-insert (event)
- "Copy highlighted command under mouse EVENT to point. Ignore comments.
-If there is no command under the mouse, behaves like mouse-track-insert."
- (interactive "e")
- (let ((str
- (save-window-excursion
- (save-excursion
- (let* ((span (span-at (mouse-set-point event) 'type)))
- (and
- span
- ;; Next test might be omitted to allow for non-script
- ;; buffer copying (e.g. from spans in the goals buffer)
- (eq (current-buffer) proof-script-buffer)
- ;; Test for type=vanilla means that closed goal-save regions
- ;; are not copied.
- ;; PG 3.3: remove this test, why not copy full proofs?
- ;; (wanted to remove tests for 'vanilla)
- ;; (eq (span-property span 'type) 'vanilla)
- ;; Finally, extracting the 'cmd part prevents copying
- ;; comments, and supresses leading spaces, at least.
- ;; Odd.
- (span-property span 'cmd)))))))
- ;; Insert copied command in original window,
- ;; buffer, point position.
- (if str
- (insert str proof-script-command-separator)
- (if (featurep 'xemacs)
- (mouse-track-insert event)))))
@@ -295,7 +249,7 @@ only an approximate test, or if `proof-strict-state-preserving'
is off (nil)."
(interactive
(list (read-string "Command: "
- (if (and current-prefix-arg (region-exists-p))
+ (if (and current-prefix-arg (region-active-p))
(replace-in-string
(buffer-substring (region-beginning) (region-end))
"[ \t\n]+" " "))
@@ -317,11 +271,7 @@ is off (nil)."
;; pear-shaped.
;; In fact, it's so risky, we'll disable it by default
-(if (if (featurep 'xemacs)
- (get 'proof-frob-locked-end 'disabled t)
- ;; FSF code more approximate
- (not (member 'disabled (symbol-plist 'proof-frob-locked-end))))
- (put 'proof-frob-locked-end 'disabled t))
+(put 'proof-frob-locked-end 'disabled t)
(defun proof-frob-locked-end ()
"Move the end of the locked region backwards to regain synchronization.
@@ -360,8 +310,8 @@ a proof command."
;;; Non-scripting proof assistant commands.
;;;
-;;; These are based on defcustom'd settings so that users may
-;;; re-configure the system to their liking.
+;; These are based on defcustom'd settings so that users may
+;; re-configure the system to their liking.
;; FIXME: da: add more general function for inserting into the
@@ -470,8 +420,8 @@ Typically, a list of syntax of commands available."
default-directory))
(defun proof-cd-sync ()
- "If proof-shell-cd-cmd is set, do proof-cd and wait for prover ready.
-This is intended as a value for proof-activate-scripting-hook"
+ "If `proof-shell-cd-cmd' 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-cmd may be set,
;; so we explicitly test it here.
(if proof-shell-cd-cmd
@@ -531,13 +481,13 @@ This is intended as a value for proof-activate-scripting-hook"
(defun proof-electric-terminator-enable ()
"Make sure the modeline is updated to display new value for electric terminator."
;; TODO: probably even this isn't necessary
- (redraw-modeline))
+ (force-mode-line-update))
(proof-deftoggle proof-electric-terminator-enable proof-electric-terminator-toggle)
;;;###autoload
(defun proof-electric-term-incomment-fn ()
- "Used as argument to proof-assert-until-point."
+ "Used as argument to `proof-assert-until-point'."
;; CAREFUL: (1) dynamic scoping here (incomment, ins, mrk)
;; (2) needs this name to be recognized in
;; proof-assert-until-point
@@ -585,7 +535,7 @@ comment, and insert or skip to the next semi)."
(defun proof-electric-terminator ()
"Insert the terminator, perhaps sending the command to the assistant.
-If `proof-electric-terminator-enable' is non-nil, the command will be
+If variable `proof-electric-terminator-enable' is non-nil, the command will be
sent to the assistant."
(interactive)
(if proof-electric-terminator-enable
@@ -662,19 +612,7 @@ last use time, to discourage saving these into the users database."
(funcall pg-insert-output-as-comment-fn proof-shell-last-output)
;; Otherwise the default behaviour is to use comment-region
(let ((beg (point)) end)
- ;; pg-assoc-strip-subterm-markup: should be done
- ;; for us in proof-fontify-region
(insert proof-shell-last-output)
- ;; 3.4: add fontification. Questionable since comments will
- ;; probably be re-highlighted, so colouration, especially
- ;; based on removed specials, will be lost.
- ;; X-Symbol conversion is useful, but a surprising nuisance
- ;; to achieve, mainly because x-symbol doesn't give us back
- ;; a useful pointer to end of region after converting, and
- ;; character positions change.
- ;; (FIXME: contact x-sym author about this).
- ;; proof-fontify-region does this for us, now
- (setq end (proof-fontify-region beg (point)))
(comment-region beg end)))))
@@ -879,15 +817,9 @@ If NUM is negative, move upwards. Return new span."
(defun pg-pos-for-event (event)
"Return position corresponding to position of a mouse click EVENT."
- (cond
- ((featurep 'xemacs)
- (when (event-window event)
- (select-window (event-window event))
- (event-point event)))
- (t
- (with-current-buffer
- (window-buffer (posn-window (event-start event)))
- (posn-point (event-start event))))))
+ (with-current-buffer
+ (window-buffer (posn-window (event-start event)))
+ (posn-point (event-start event))))
(defun pg-span-for-event (event)
"Return span corresponding to position of a mouse click EVENT."
@@ -1054,11 +986,7 @@ The function `substitute-command-keys' is called on the argument."
;; Note: making the binding globally is perhaps a bit obnoxious, but
;; this modifier combination is currently unused.
-(cond
- ((not (featurep 'xemacs))
- (global-set-key [C-M-mouse-2] 'pg-identifier-under-mouse-query))
- ((featurep 'xemacs)
- (global-set-key '(control meta button2) 'pg-identifier-under-mouse-query)))
+(global-set-key [C-M-mouse-2] 'pg-identifier-under-mouse-query)
(defun pg-identifier-under-mouse-query (event)
(interactive "e")
@@ -1067,18 +995,13 @@ The function `substitute-command-keys' is called on the argument."
(save-selected-window
(save-selected-frame
(save-excursion
- (if (featurep 'xemacs)
- (when (event-window event)
- (select-window (event-window event))
- (setq oldend (if (region-exists-p)
- (region-end)))))
(mouse-set-point event)
(setq identifier
;; If there's an active region in this buffer, use that
;; instead of the identifier under point. Since
;; region-end moves immediately to new point with
;; zmacs-regions we use oldend instead of current.
- (if (region-exists-p)
+ (if (region-active-p)
(buffer-substring (region-beginning)
(or oldend (region-end)))
(setq identifier (current-word))))
@@ -1110,17 +1033,15 @@ The function `substitute-command-keys' is called on the argument."
"Add or remove index menu."
(if proof-imenu-enable
(imenu-add-to-menubar "Index")
- (if (featurep 'xemacs)
- (easy-menu-remove (list "Index" :filter 'imenu-menu-filter))
- (progn
- (let ((oldkeymap (keymap-parent (current-local-map))))
- (if ;; sanity checks in case someone else set local keymap
- (and oldkeymap
- (lookup-key (current-local-map) [menu-bar index])
- (not
- (lookup-key oldkeymap [menu-bar index])))
- (use-local-map oldkeymap)))
- (remove-hook 'menu-bar-update-hook 'imenu-update-menubar)))))
+ (progn
+ (let ((oldkeymap (keymap-parent (current-local-map))))
+ (if ;; sanity checks in case someone else set local keymap
+ (and oldkeymap
+ (lookup-key (current-local-map) [menu-bar index])
+ (not
+ (lookup-key oldkeymap [menu-bar index])))
+ (use-local-map oldkeymap)))
+ (remove-hook 'menu-bar-update-hook 'imenu-update-menubar))))
@@ -1140,13 +1061,13 @@ The function `substitute-command-keys' is called on the argument."
;;
(defvar pg-input-ring nil
- "Ring of previous inputs")
+ "Ring of previous inputs.")
(defvar pg-input-ring-index nil
- "Position of last matched command")
+ "Position of last matched command.")
(defvar pg-stored-incomplete-input nil
- "Stored incomplete input: string between point and locked")
+ "Stored incomplete input: string between point and locked.")
(defun pg-previous-input (arg)
"Cycle backwards through input history, saving input."
@@ -1280,7 +1201,7 @@ If N is negative, find the next or Nth next match."
(let ((pos (pg-previous-matching-input-string-position regexp n)))
;; Has a match been found?
(if (null pos)
- (error "Match not found" regexp)
+ (error "Match not found for regexp %s" regexp)
;; If leaving the edit line, save partial input
(if (null pg-input-ring-index) ;not yet on ring
(setq pg-stored-incomplete-input (pg-get-old-input)))
@@ -1344,7 +1265,7 @@ of the last item added."
;;;###autoload
(defun pg-remove-from-input-history (cmd)
"Maybe remove CMD from the end of the input history.
-This is called when the command is undone. It's only
+This is called when the command is undone. It's only
removed if it matches the last item in the ring."
(if (and (ring-p pg-input-ring)
(not (ring-empty-p pg-input-ring))
@@ -1358,4 +1279,5 @@ removed if it matches the last item in the ring."
(provide 'pg-user)
+
;;; pg-user.el ends here
diff --git a/generic/pg-xml.el b/generic/pg-xml.el
index 3f9a0f37..46a98b2f 100644
--- a/generic/pg-xml.el
+++ b/generic/pg-xml.el
@@ -9,18 +9,10 @@
;; XML functions for Proof General.
;;
-(eval-when-compile
- (require 'xml-fixed)) ; for compile only
+(require 'xml)
(require 'proof-utils) ;; for pg-internal-warning
-(cond
- ;; We want to find a good version of xml.el
- ((featurep 'xemacs)
- (require 'xml-fixed)) ;; XEmacs: used PG bundled fixed version
- (t ;; Otherwise use GNU Emacs distrib version.
- (require 'xml)))
-
(defalias 'pg-xml-error 'error)
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 5fcfc802..98cc57fc 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -1,11 +1,10 @@
-;;; DO NOT MODIFY THIS FILE
-(if (featurep 'proof-autoloads) (error "Already loaded"))
-
-(provide 'proof-autoloads)
+;;; proof-autoloads.el --- automatically extracted autoloads
+;;
+;;; Code:
;;;### (autoloads (bufhist-exit bufhist-init) "bufhist" "../lib/bufhist.el"
-;;;;;; (18346 18016))
+;;;;;; (18568 19169))
;;; Generated autoloads from ../lib/bufhist.el
(autoload (quote bufhist-init) "bufhist" "\
@@ -26,9 +25,29 @@ Minor mode retaining an in-memory history of the buffer contents.")
;;;***
-;;;### (autoloads (holes-mode) "holes" "../lib/holes.el" (18346 18016))
+;;;### (autoloads (holes-mode holes-insert-and-expand holes-abbrev-complete
+;;;;;; holes-set-make-active-hole) "holes" "../lib/holes.el" (18568
+;;;;;; 20048))
;;; Generated autoloads from ../lib/holes.el
+(autoload (quote holes-set-make-active-hole) "holes" "\
+Make a new hole between START and END or at point, and make it active.
+
+\(fn &optional START END)" t nil)
+
+(autoload (quote holes-abbrev-complete) "holes" "\
+Complete abbrev by putting holes and indenting.
+Moves point at beginning of expanded text. Put this function as
+call-back for your abbrevs, and just expanded \"#\" and \"@{..}\" will
+become holes.
+
+\(fn)" nil nil)
+
+(autoload (quote holes-insert-and-expand) "holes" "\
+Insert S, expand it and replace #s and @{]s by holes.
+
+\(fn S)" nil nil)
+
(autoload (quote holes-mode) "holes" "\
If ARG is nil, then toggle holes mode on/off.
If arg is positive, then turn holes mode on. If arg is negative, then
@@ -39,7 +58,7 @@ turn it off.
;;;***
;;;### (autoloads (maths-menu-mode) "maths-menu" "../lib/maths-menu.el"
-;;;;;; (18346 18016))
+;;;;;; (18568 19169))
;;; Generated autoloads from ../lib/maths-menu.el
(autoload (quote maths-menu-mode) "maths-menu" "\
@@ -53,7 +72,7 @@ This mode is only useful with a font which can display the maths repertoire.
;;;***
;;;### (autoloads (proof-associated-windows proof-associated-buffers)
-;;;;;; "pg-assoc" "pg-assoc.el" (18346 18015))
+;;;;;; "pg-assoc" "pg-assoc.el" (18568 19165))
;;; Generated autoloads from pg-assoc.el
(autoload (quote proof-associated-buffers) "pg-assoc" "\
@@ -71,7 +90,7 @@ Dead or nil buffers are not represented in the list.
;;;***
;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el"
-;;;;;; (18544 41603))
+;;;;;; (18568 19165))
;;; Generated autoloads from pg-goals.el
(autoload (quote proof-goals-config-done) "pg-goals" "\
@@ -82,7 +101,7 @@ Initialise the goals buffer after the child has been configured.
;;;***
;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet)
-;;;;;; "pg-pgip" "pg-pgip.el" (18346 18015))
+;;;;;; "pg-pgip" "pg-pgip.el" (18336 38440))
;;; Generated autoloads from pg-pgip.el
(autoload (quote pg-pgip-process-packet) "pg-pgip" "\
@@ -105,8 +124,8 @@ Send an <askprefs> message to the prover.
;;;### (autoloads (pg-response-has-error-location proof-next-error
;;;;;; pg-response-display-with-face pg-response-maybe-erase proof-response-config-done
-;;;;;; proof-response-mode) "pg-response" "pg-response.el" (18544
-;;;;;; 41603))
+;;;;;; proof-response-mode) "pg-response" "pg-response.el" (18568
+;;;;;; 19166))
;;; Generated autoloads from pg-response.el
(autoload (quote proof-response-mode) "pg-response" "\
@@ -158,7 +177,7 @@ See `pg-next-error-regexp'.
;;;***
;;;### (autoloads (pg-defthymode) "pg-thymodes" "pg-thymodes.el"
-;;;;;; (18346 18015))
+;;;;;; (18568 19166))
;;; Generated autoloads from pg-thymodes.el
(autoload (quote pg-defthymode) "pg-thymodes" "\
@@ -185,7 +204,7 @@ All of these settings are optional.
;;;;;; pg-response-buffers-hint pg-slow-fontify-tracing-hint proof-electric-term-incomment-fn
;;;;;; proof-electric-terminator-enable proof-define-assistant-command-witharg
;;;;;; proof-define-assistant-command proof-interrupt-process) "pg-user"
-;;;;;; "pg-user.el" (18544 41603))
+;;;;;; "pg-user.el" (18568 19166))
;;; Generated autoloads from pg-user.el
(autoload (quote proof-interrupt-process) "pg-user" "\
@@ -219,7 +238,7 @@ Make sure the modeline is updated to display new value for electric terminator.
\(fn)" nil nil)
(autoload (quote proof-electric-term-incomment-fn) "pg-user" "\
-Used as argument to proof-assert-until-point.
+Used as argument to `proof-assert-until-point'.
\(fn)" nil nil)
@@ -284,7 +303,7 @@ of the last item added.
(autoload (quote pg-remove-from-input-history) "pg-user" "\
Maybe remove CMD from the end of the input history.
-This is called when the command is undone. It's only
+This is called when the command is undone. It's only
removed if it matches the last item in the ring.
\(fn CMD)" nil nil)
@@ -296,8 +315,8 @@ Not documented
;;;***
-;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (18346
-;;;;;; 18015))
+;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (18568
+;;;;;; 19166))
;;; Generated autoloads from pg-xml.el
(autoload (quote pg-xml-parse-string) "pg-xml" "\
@@ -308,7 +327,7 @@ Parse string in ARG, same as pg-xml-parse-buffer.
;;;***
;;;### (autoloads (proof-dependency-in-span-context-menu proof-depends-process-dependencies)
-;;;;;; "proof-depends" "proof-depends.el" (18346 18015))
+;;;;;; "proof-depends" "proof-depends.el" (18336 38440))
;;; Generated autoloads from proof-depends.el
(autoload (quote proof-depends-process-dependencies) "proof-depends" "\
@@ -326,7 +345,7 @@ Make a portion of a context-sensitive menu showing proof dependencies.
;;;***
;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el"
-;;;;;; (18346 18015))
+;;;;;; (18568 19167))
;;; Generated autoloads from proof-easy-config.el
(autoload (quote proof-easy-config) "proof-easy-config" "\
@@ -339,7 +358,7 @@ the `proof-assistant-table', which see.
;;;***
;;;### (autoloads (proof-indent-line) "proof-indent" "proof-indent.el"
-;;;;;; (18346 18015))
+;;;;;; (18336 38440))
;;; Generated autoloads from proof-indent.el
(autoload (quote proof-indent-line) "proof-indent" "\
@@ -350,7 +369,7 @@ Indent current line of proof script, if indentation enabled.
;;;***
;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-set-global)
-;;;;;; "proof-maths-menu" "proof-maths-menu.el" (18346 18015))
+;;;;;; "proof-maths-menu" "proof-maths-menu.el" (18568 19167))
;;; Generated autoloads from proof-maths-menu.el
(autoload (quote proof-maths-menu-set-global) "proof-maths-menu" "\
@@ -372,7 +391,7 @@ in future if we have just activated it for this buffer.
;;;### (autoloads (defpacustom proof-defpacustom-fn proof-aux-menu
;;;;;; proof-menu-define-specific proof-menu-define-main proof-menu-define-keys)
-;;;;;; "proof-menu" "proof-menu.el" (18558 29736))
+;;;;;; "proof-menu" "proof-menu.el" (18568 19167))
;;; Generated autoloads from proof-menu.el
(autoload (quote proof-menu-define-keys) "proof-menu" "\
@@ -415,7 +434,7 @@ evaluate can be provided instead.
;;;***
;;;### (autoloads (proof-mmm-enable proof-mmm-set-global) "proof-mmm"
-;;;;;; "proof-mmm.el" (18346 18015))
+;;;;;; "proof-mmm.el" (18360 12927))
;;; Generated autoloads from proof-mmm.el
(autoload (quote proof-mmm-set-global) "proof-mmm" "\
@@ -437,7 +456,7 @@ in future if we have just activated it for this buffer.
;;;### (autoloads (proof-config-done proof-mode proof-insert-sendback-command
;;;;;; proof-insert-pbp-command pg-set-span-helphighlights proof-locked-region-empty-p
;;;;;; proof-locked-region-full-p proof-locked-end proof-unprocessed-begin)
-;;;;;; "proof-script" "proof-script.el" (18550 34521))
+;;;;;; "proof-script" "proof-script.el" (18568 19167))
;;; Generated autoloads from proof-script.el
(autoload (quote proof-unprocessed-begin) "proof-script" "\
@@ -497,7 +516,7 @@ finish setup which depends on specific proof assistant configuration.
;;;;;; 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" (18550 34521))
+;;;;;; "proof-shell" "proof-shell.el" (18568 19167))
;;; Generated autoloads from proof-shell.el
(autoload (quote proof-shell-ready-prover) "proof-shell" "\
@@ -609,7 +628,7 @@ processing.
;;;***
;;;### (autoloads (proof-splash-message proof-splash-display-screen)
-;;;;;; "proof-splash" "proof-splash.el" (18346 18015))
+;;;;;; "proof-splash" "proof-splash.el" (18568 19168))
;;; Generated autoloads from proof-splash.el
(autoload (quote proof-splash-display-screen) "proof-splash" "\
@@ -628,7 +647,7 @@ Make sure the user gets welcomed one way or another.
;;;***
;;;### (autoloads (proof-splice-separator proof-format) "proof-syntax"
-;;;;;; "proof-syntax.el" (18346 18015))
+;;;;;; "proof-syntax.el" (18568 19982))
;;; Generated autoloads from proof-syntax.el
(autoload (quote proof-format) "proof-syntax" "\
@@ -646,7 +665,7 @@ Splice SEP into list of STRINGS.
;;;***
;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup)
-;;;;;; "proof-toolbar" "proof-toolbar.el" (18550 34521))
+;;;;;; "proof-toolbar" "proof-toolbar.el" (18568 19168))
;;; Generated autoloads from proof-toolbar.el
(autoload (quote proof-toolbar-setup) "proof-toolbar" "\
@@ -664,17 +683,18 @@ Menu made from the Proof General toolbar commands.
;;;***
-;;;### (autoloads (proof-unicode-tokens-shell-config proof-unicode-tokens-set-global
-;;;;;; proof-unicode-tokens-enable) "proof-unicode-tokens" "proof-unicode-tokens.el"
-;;;;;; (18544 41604))
+;;;### (autoloads (proof-unicode-tokens-set-global proof-unicode-tokens-enable)
+;;;;;; "proof-unicode-tokens" "proof-unicode-tokens.el" (18568 19168))
;;; Generated autoloads from proof-unicode-tokens.el
(autoload (quote proof-unicode-tokens-enable) "proof-unicode-tokens" "\
Turn on or off Unicode tokens mode in Proof General script buffer.
This invokes `unicode-tokens-mode' to toggle the setting for the current
buffer, and then sets PG's option for default to match.
-Also we arrange to have unicode tokens mode turn itself on automatically
+Also we arrange to have unicode tokens mode turn itself on automatically
in future if we have just activated it for this buffer.
+Note: this function is called when the customize setting for the prover
+is changed.
\(fn)" t nil)
@@ -684,67 +704,49 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit.
\(fn FLAG)" nil nil)
-(autoload (quote proof-unicode-tokens-shell-config) "proof-unicode-tokens" "\
-Not documented
-
-\(fn)" nil nil)
-
;;;***
-;;;### (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" (18544 41604))
-;;; Generated autoloads from proof-x-symbol.el
-
-(autoload (quote proof-x-symbol-support-maybe-available) "proof-x-symbol" "\
-A test to see whether x-symbol support may be available.
+;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "../lib/texi-docstring-magic.el"
+;;;;;; (18336 38444))
+;;; Generated autoloads from ../lib/texi-docstring-magic.el
-\(fn)" nil nil)
+(autoload (quote texi-docstring-magic) "texi-docstring-magic" "\
+Update all texi docstring magic annotations in buffer.
+With prefix arg, no errors on unknown symbols. (This results in
+@def .. @end being deleted if not known).
-(autoload (quote proof-x-symbol-enable) "proof-x-symbol" "\
-Turn on or off X-Symbol in current Proof General script buffer.
-This invokes `x-symbol-mode' to change the setting for the current
-buffer.
+\(fn &optional NOERROR)" t nil)
-\(fn)" nil nil)
+;;;***
+
+;;;### (autoloads (unicode-tokens-mode unicode-tokens-initialise)
+;;;;;; "unicode-tokens" "../lib/unicode-tokens.el" (18568 20076))
+;;; Generated autoloads from ../lib/unicode-tokens.el
-(autoload (quote proof-x-symbol-decode-region) "proof-x-symbol" "\
+(autoload (quote unicode-tokens-initialise) "unicode-tokens" "\
Not documented
-\(fn START END)" nil nil)
-
-(autoload (quote proof-x-symbol-shell-config) "proof-x-symbol" "\
-Configure the proof shell for x-symbol, if proof-x-symbol-support<>nil.
-Assumes that the current buffer is the proof shell buffer.
-
-\(fn)" nil nil)
+\(fn)" t nil)
-(autoload (quote proof-x-symbol-config-output-buffer) "proof-x-symbol" "\
-Configure the current output buffer (goals/response/trace) for X-Symbol.
+(autoload (quote unicode-tokens-mode) "unicode-tokens" "\
+Minor mode for unicode token input.
-\(fn)" nil nil)
+\(fn &optional ARG)" t nil)
;;;***
-;;;### (autoloads nil nil ("../lib/holes-load.el" "../lib/local-vars-list.el"
-;;;;;; "../lib/pg-dev.el" "../lib/pg-fontsets.el" "../lib/proof-compat.el"
-;;;;;; "../lib/span-extent.el" "../lib/span-overlay.el" "../lib/span.el"
-;;;;;; "../lib/unicode-chars.el" "../lib/unicode-tokens.el" "../lib/xml-fixed.el"
-;;;;;; "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" "pg-vars.el"
-;;;;;; "proof-auxmodes.el" "proof-config.el" "proof-site.el" "proof-utils.el"
-;;;;;; "proof.el") (18558 30696 142301))
+;;;### (autoloads nil nil ("../lib/local-vars-list.el" "../lib/pg-dev.el"
+;;;;;; "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.el"
+;;;;;; "../lib/unicode-chars.el" "pg-autotest.el" "pg-custom.el"
+;;;;;; "pg-pbrpm.el" "pg-vars.el" "proof-auxmodes.el" "proof-config.el"
+;;;;;; "proof-site.el" "proof-utils.el" "proof.el") (18568 20102
+;;;;;; 515468))
;;;***
-;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "../lib/texi-docstring-magic.el"
-;;;;;; (18346 18016))
-;;; Generated autoloads from ../lib/texi-docstring-magic.el
-
-(autoload (quote texi-docstring-magic) "texi-docstring-magic" "\
-Update all texi docstring magic annotations in buffer.
-With prefix arg, no errors on unknown symbols. (This results in
-@def .. @end being deleted if not known).
-
-\(fn &optional NOERROR)" t nil)
-
-;;;***
+;; Local Variables:
+;; version-control: never
+;; no-byte-compile: t
+;; no-update-autoloads: t
+;; End:
+;;; proof-autoloads.el ends here
diff --git a/generic/proof-auxmodes.el b/generic/proof-auxmodes.el
index f8ea8da6..d204154f 100644
--- a/generic/proof-auxmodes.el
+++ b/generic/proof-auxmodes.el
@@ -7,9 +7,7 @@
;;; Commentary:
;;
;; Startup code from auxiliary modes are collected here, allowing late
-;; loading of their main defining files.
-;;
-;; TODO: add x-symbol here too and disentangle elsewhere.
+;; loading of their main defining files and the possibility to disable them.
;;
(require 'proof-utils) ; proof-ass, proof-eval...
@@ -47,7 +45,6 @@
(defun proof-maths-menu-support-available ()
"A test to see whether maths-menu support is available."
(and
- (not (featurep 'xemacs)) ;; not XEmacs compatible
(or (featurep 'maths-menu)
;; *should* always succeed unless bundled version broken
(proof-try-require 'maths-menu))
@@ -65,11 +62,9 @@
;;
(defun proof-unicode-tokens-support-available ()
"A test to see whether unicode tokens support is available."
- (and
- (or (featurep 'unicode-tokens)
- (proof-try-require 'unicode-tokens))
- ;; Requires prover-specific config in <foo>-unicode-tokens.el
- (proof-try-require (proof-ass-sym unicode-tokens))))
+ ;; Requires prover-specific config in <foo>-unicode-tokens.el
+ ;; Loaded before unicode-tokens.el to allow load-time config there
+ (proof-try-require (proof-ass-sym unicode-tokens)))
(proof-eval-when-ready-for-assistant
(if (and (proof-ass unicode-tokens-enable)
diff --git a/generic/proof-config.el b/generic/proof-config.el
index b7790a59..c503e4b9 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -24,12 +24,12 @@
;; 3. Menus, user-level commands, toolbar
;; 4. Script mode configuration
;; 5. Shell mode configuration
-;; 5a. commands
-;; 5b. regexps
-;; 5c. hooks and others
+;; 5a. commands
+;; 5b. regexps
+;; 5c. tokens
+;; 5d. hooks and others
;; 6. Goals buffer configuration
-;; 7. X-Symbol support
-;; 8. Global constants
+;; 7. Global constants
;;
;; The user options don't need to be set on a per-prover basis,
;; and the global constants probably should not be touched.
@@ -50,7 +50,6 @@
;; proof-script : settings for proof script mode (4)
;; proof-shell : settings for proof shell mode (5)
;; proof-goals : settings for goals buffer (6)
-;; proof-x-symbol : settings for X-Symbol (8)
;; <Prover name>-config : Specific internal settings for a prover
;;
;; ======================================================================
@@ -61,7 +60,7 @@
;; (a) put it in the right customize group, and
;; (b) add a magical comment in ProofGeneral.texi/PG-Adapting.texi
;;
-;; ii. Presently the customize library seems a bit picky over the
+;; ii. Presently the customize library seems a bit picky over the
;; :type property and some correct but complex types don't work:
;; If the type is ill-formed, editing the whole group will be broken.
;; Check after updates, by killing all customize buffers and
@@ -88,18 +87,17 @@
:prefix "proof-")
;;
-;; Function for taking action when dynamically adjusting customize
-;; values
+;; Take action when dynamically adjusting customize values
;;
(defun proof-set-value (sym value)
- "Set a customize variable using set-default and a function.
+ "Set a customize variable using `set-default' and a function.
We first call `set-default' to set SYM to VALUE.
Then if there is a function SYM (i.e. with the same name as the
variable SYM), it is called to take some dynamic action for the new
setting.
If there is no function SYM, we try stripping
-proof-assistant-symbol and adding \"proof-\" instead to get
+`proof-assistant-symbol' and adding \"proof-\" instead to get
a function name. This extends proof-set-value to work with
generic individual settings.
@@ -153,15 +151,6 @@ terminator somewhere nearby. Electric!"
:type 'boolean
:group 'proof-user-options)
-(defcustom proof-output-fontify-enable t
- "*Whether to fontify output from the proof assistant.
-If non-nil, output from the proof assistant will be highlighted
-in the goals and response buffers.
-\(This is providing `font-lock-keywords' have been set for the
-buffer modes)."
- :type 'boolean
- :group 'proof-user-options)
-
;; FIXME: next one could be integer value for catchup delay
(defcustom proof-trace-output-slow-catchup t
"*If non-nil, try to redisplay less often during frequent trace output.
@@ -191,7 +180,7 @@ done if this `proof-strict-state-preserving' is turned off (nil)."
If non-nil, an error is given when an attempt is made to edit the
read-only region. If nil, Proof General is more relaxed (but may give
you a reprimand!)."
- :type 'boolean
+ :type '(choice (const strict) (const retract) (const nil))
:set 'proof-set-value
:group 'proof-user-options)
@@ -249,14 +238,6 @@ goals and response windows to fit their contents."
:type 'boolean
:group 'proof-user-options)
-(defcustom proof-toolbar-use-button-enablers t
- "*If non-nil, toolbars buttons may be enabled/disabled automatically.
-Toolbar buttons can be automatically enabled/disabled according to
-the context. Set this variable to nil if you don't like this feature
-or if you find it unreliable."
- :type 'boolean
- :group 'proof-user-options)
-
(defcustom proof-query-file-save-when-activating-scripting
t
"*If non-nil, query user to save files when activating scripting.
@@ -288,9 +269,9 @@ This option is not fully-functional at the moment." ;; TODO
(defcustom proof-prog-name-guess
nil
- "*If non-nil, use `proof-guess-command-line' to guess proof-prog-name.
-This option is compatible with proof-prog-name-ask.
-No effect if proof-guess-command-line is nil."
+ "*If non-nil, use `proof-guess-command-line' to guess `proof-prog-name'.
+This option is compatible with `proof-prog-name-ask'.
+No effect if `proof-guess-command-line' is nil."
:type 'boolean
:group 'proof-user-options)
@@ -357,7 +338,7 @@ If 'followdown, point if necessary to stay in writeable region
If 'ignore, point is never moved after movement commands or on errors.
If you choose 'ignore, you can find the end of the locked using
-`M-x proof-goto-end-of-locked'."
+\\[proof-goto-end-of-locked]"
:type '(choice
(const :tag "Follow locked region" locked)
(const :tag "Follow locked region down" followdown)
@@ -452,7 +433,7 @@ signals to the remote host."
;; TODO: get rid of this list. Does 'default work widely enough
;; by now?
-(defconst pg-defface-window-systems
+(defconst pg-defface-window-systems
'(x ;; bog standard
mswindows ;; Windows
w32 ;; Windows
@@ -461,7 +442,7 @@ signals to the remote host."
carbon ;; used by Carbon XEmacs
ns ;; NeXTstep Emacs (Emacs.app)
x-toolkit) ;; possible catch all (but probably not)
- "A list of possible values for `window-system'.
+ "A list of possible values for variable `window-system'.
If you are on a window system and your value of `window-system' is
not listed here, you may not get the correct syntax colouring behaviour.")
@@ -530,8 +511,8 @@ Exactly what uses this face depends on the proof assistant."
(defface proof-error-face
(proof-face-specs
- (:background "indianred1" :bold t)
- (:background "brown" :bold t)
+ (:background "indianred1")
+ (:background "brown")
(:bold t))
"*Face for error messages from proof assistant."
:group 'proof-faces)
@@ -601,7 +582,7 @@ Warning messages can come from proof assistant or from Proof General itself."
"*Face for showing active areas (clickable regions), outside of subterm markup."
:group 'proof-faces)
-;;; Compatibility: these are required for use in onder GNU Emacs/font-lock-keywords
+;;; Compatibility: these are required for use in GNU Emacs/font-lock-keywords
(defconst proof-face-compat-doc "Evaluates to a face name, for compatibility.")
(defconst proof-queue-face 'proof-queue-face proof-face-compat-doc)
(defconst proof-locked-face 'proof-locked-face proof-face-compat-doc)
@@ -666,7 +647,7 @@ Warning messages can come from proof assistant or from Proof General itself."
;; proof-mode-for-goals: <PA>-goals-mode
;; proof-mode-for-script: <PA>-mode
;;
-;; These are defined as constants in pg-custom.el
+;; These are defined in pg-vars.el and set in proof-site mode stub.
;;
;; Prover modes should define aliases for these if not defun'd.
@@ -899,7 +880,7 @@ as well as `proof-script-comment-end'."
(defcustom proof-script-comment-start-regexp nil
"Regexp which matches a comment start in the proof command language.
-The default value for this is set as (regexp-quote proof-script-comment-start)
+The default value for this is set as (regexp-quote `proof-script-comment-start')
but you can set this variable to something else more precise if necessary."
:type 'string
:group 'proof-script)
@@ -944,7 +925,7 @@ If left as nil, the default behaviour is to insert and call `comment-region'."
"Value for `case-fold-search' when recognizing portions of proof scripts.
Also used for completion, via `proof-script-complete'.
The default value is nil. If your prover has a case *insensitive*
-input syntax, proof-case-fold-search should be set to t instead.
+input syntax, `proof-case-fold-search' should be set to t instead.
NB: This setting is not used for matching output from the prover."
:type 'boolean :group
'proof-script)
@@ -968,9 +949,9 @@ It's safe to leave this setting as nil."
(defcustom proof-save-with-hole-result 2
"How to build theorem name after matching with `proof-save-with-hole-regexp'.
-String or Int.
-If an int N use match-string to recover the value of the Nth parenthesis matched.
-If it is a string use replace-match. In this case, proof-save-with-hole-regexp
+String or Int.
+If an int N use match-string to recover the value of the Nth parenthesis matched.
+If it is a string use replace-match. In this case, proof-save-with-hole-regexp
should match the entire command"
:type '(choice string int)
:group 'proof-script)
@@ -988,7 +969,7 @@ for `proof-script-next-entity-regexps' used for function menus."
(defcustom proof-goal-with-hole-regexp nil
"Regexp which matches a command used to issue and name a goal.
The name of the theorem is built from the variable
-proof-goal-with-hole-result using the same convention as
+`proof-goal-with-hole-result' using the same convention as
for `query-replace-regexp'.
Used for setting names of goal..save regions and for default
configuration of other modes (function menu, imenu).
@@ -999,9 +980,9 @@ It's safe to leave this setting as nil."
(defcustom proof-goal-with-hole-result 2
"How to build theorem name after matching with `proof-goal-with-hole-regexp'.
-String or Int.
-If an int N use match-string to recover the value of the Nth parenthesis matched.
-If it is a string use replace-match. In this case, proof-save-with-hole-regexp
+String or Int.
+If an int N use match-string to recover the value of the Nth parenthesis matched.
+If it is a string use replace-match. In this case, proof-save-with-hole-regexp
should match the entire command"
:type '(choice string int)
:group 'proof-script)
@@ -1077,8 +1058,8 @@ only at the end. However, it does not parse strings,
comments, or parentheses.
This variable may not need to be set: a default value which should
-work for goal..saves is calculated from proof-goal-with-hole-regexp,
-proof-goal-command-regexp, and proof-save-with-hole-regexp."
+work for goal..saves is calculated from `proof-goal-with-hole-regexp',
+`proof-goal-command-regexp', and `proof-save-with-hole-regexp'."
:type 'sexp
;; Bit tricky.
;; (list (regexp :tag "Any entity matcher")
@@ -1098,7 +1079,7 @@ cell of the name and the beginning of the entity's region.
Note that `proof-script-next-entity-regexps' is set to a default value
from `proof-goal-with-hole-regexp' and `proof-save-with-hole-regexp' in
-the function proof-config-done, so you may not need to worry about any
+the function `proof-config-done', so you may not need to worry about any
of this. See whether function menu does something sensible by
default."
:type 'function
@@ -1112,53 +1093,24 @@ and that variable for details."
:type 'sexp
:group 'proof-script)
-
-;; FIXME da: This next one is horrible. We clearly would rather
-;; have just proof-goal-command regexp instead. This was born to solve
-;; problem that Coq can have goals which look like definitions, etc.
-;; Perhaps we can generalise the matching to understand function
-;; values as well as regexps.
-;; FIXME: could just as easily give default value of
-;; proof-std-goal-command-p here, why not?
-;; Pierre: changed this to take the span as argument instead of the string,
-;; This allows coq-mode to use a 'goalcmd attribute computed by looking at
-;; coq messages when each command is sent.
+;; FIXME da: unify this with proof-save-command-regexp, to allow fn or regexp
(defcustom proof-goal-command-p 'proof-generic-goal-command-p
"A function to test: is this really a goal command span?
-This is added as a more refined addition to proof-goal-command-regexp,
+This is added as a more refined addition to `proof-goal-command-regexp',
to solve the problem that Coq and some other provers can have goals which
look like definitions, etc. (In the future we may generalize
-proof-goal-command-regexp instead)."
+`proof-goal-command-regexp' instead)."
:type 'function
:group 'proof-script)
-;; FIXME mmw: increasing the horror even more ...
-;; FIXME da: why do you need the span below? I would like to replace
-;; this mess by single config variables which are allowed to be
-;; regexps or functions, handled in proof-string-match.
-;; FIXME mmw: the span is required to scan backwards through the text,
-;; determining the depth of proof nesting.
-;; FIXME da: yuck! What I'd really like to replace the mess with is
-;; feedback from the proof assistant, saying "that was a save", etc.
-;; FIXME mmw: all we need is some tracking of the 'depth' of commands;
-;; Why not let PG track this as in spans, changing the value based
-;; on some regexps for 'open' / 'close' commands? This would basically
-;; move the code of isar-global-save-command-p to proof-done-advancing.
-;; FIXME da: sounds like a good idea, then that would give us a proper
-;; handling of nested proofs?
-;; FIXME: Pierre:Careful: in coq V8 I now need a function to detect save
-;; command. Because Proof <term>. is a term, but not Proof with ...
-;;
+;; FIXME da: unify this with proof-save-command-regexp, to allow fn or regexp
(defcustom proof-really-save-command-p (lambda (span cmd) t)
"Is this really a save command?
-This is a more refined addition to proof-save-command-regexp.
+This is a more refined addition to `proof-save-command-regexp'.
It should be a function taking a span and command as argument,
-and can be used to track nested proofs. (See what is done in
-isar/ for example). In the future, this setting should be
-removed when the generic core is extended to handle nested
-proofs smoothly."
+and can be used to track nested proofs."
:type 'function
:group 'proof-script)
@@ -1204,7 +1156,7 @@ settings `proof-non-undoables-regexp' and
(defconst proof-no-command "COMMENT"
"String used as a nullary action (send no command to the proof assistant).
-Only relevant for proof-find-and-forget-fn.
+Only relevant for `proof-find-and-forget-fn'.
\(NB: this is a CONSTANT, don't change it).")
(defcustom proof-find-and-forget-fn 'proof-generic-find-and-forget
@@ -1215,7 +1167,7 @@ It should undo the effect of all settings between its target span
up to (proof-locked-end). This may involve forgetting a number
of definitions, declarations, or whatever.
-The special string proof-no-command means there is nothing to do.
+The special string `proof-no-command' means there is nothing to do.
This is an important function for script management.
Study one of the existing instantiations for examples of how to write it,
@@ -1249,7 +1201,7 @@ will be attempted."
(defcustom proof-kill-goal-command ""
"Command to kill the currently open goal.
-If this is set to nil, PG will expect proof-find-and-forget-fn
+If this is set to nil, PG will expect `proof-find-and-forget-fn'
to do all the work of retracting to an arbitrary point in a file.
Otherwise, the generic split-phase mechanism will be used:
@@ -1285,7 +1237,7 @@ steps within the outer proof."
(defcustom proof-state-preserving-p 'proof-generic-state-preserving-p
"A predicate, non-nil if its argument (a command) preserves the proof state.
-This is a safety-test used by proof-minibuffer-cmd to filter out scripting
+This is a safety-test used by `proof-minibuffer-cmd' to filter out scripting
commands which should be entered directly into the script itself.
The default setting for this function, `proof-generic-state-preserving-p'
@@ -1304,7 +1256,7 @@ script).
When functions in this hook are called, the variable
`activated-interactively' will be non-nil if
-proof-activate-scripting was called interactively
+`proof-activate-scripting' was called interactively
\(rather than as a side-effect of some other action).
If a hook function sends commands to the proof process,
it should wait for them to complete (so the queue is cleared
@@ -1378,9 +1330,9 @@ assistant, for example, to compile a completed file."
(defcustom proof-script-font-lock-keywords nil
"Value of `font-lock-keywords' used to fontify proof scripts.
-This is currently used only by `proof-easy-config' mechanism,
-to set `font-lock-keywords' before calling proof-config-done.
-See also proof-{shell,resp,goals}-font-lock-keywords."
+The proof script mode should set this before calling `proof-config-done'.
+Used also by `proof-easy-config' mechanism.
+See also proof-{resp,goals}-font-lock-keywords."
:type 'sexp
:group 'proof-script)
@@ -1442,7 +1394,7 @@ See pg-user.el: pg-create-in-span-context-menu for more hints."
"System command to run the proof assistant in the proof shell.
May contain arguments separated by spaces, but see also `proof-prog-args'.
-Remark: if `proof-prog-args' is non-nil, then proof-prog-name is considered
+Remark: if `proof-prog-args' is non-nil, then `proof-prog-name' is considered
strictly: it must contain *only* the program name with no option, spaces
are interpreted literally as part of the program name."
:type 'string
@@ -1453,8 +1405,8 @@ are interpreted literally as part of the program name."
"Non-nil if Proof General should try to add terminator to every command.
If non-nil, whenever a command is sent to the prover using
`proof-shell-invisible-command', Proof General will check to see if it
-ends with proof-terminal-char, and add it if not.
-If proof-terminal-char is nil, this has no effect."
+ends with `proof-terminal-char', and add it if not.
+If `proof-terminal-char' is nil, this has no effect."
:type 'boolean
:group 'proof-shell)
@@ -1483,6 +1435,12 @@ See also `proof-shell-pre-sync-init-cmd'."
:type '(choice string (const nil))
:group 'proof-shell)
+;; TODO: remove proof-shell-init-cmd in favour of this hook
+(defcustom proof-shell-init-hook nil
+ "Hooks run when the proof process has started up."
+ :type '(list function)
+ :group 'proof-shell)
+
(defcustom proof-shell-restart-cmd ""
"A command for re-initialising the proof process."
:type '(choice string (const nil))
@@ -1495,7 +1453,7 @@ See also `proof-shell-pre-sync-init-cmd'."
(defcustom proof-shell-quit-timeout 4
;; FIXME could add option to quiz user before rude kill.
- "The number of seconds to wait after sending proof-shell-quit-cmd.
+ "The number of seconds to wait after sending `proof-shell-quit-cmd'.
After this timeout, the proof shell will be killed off more rudely.
If your proof assistant takes a long time to clean up (for
example writing persistent databases out or the like), you may
@@ -1509,12 +1467,12 @@ The format character `%s' is replaced with the directory, and
the escape sequences in `proof-shell-filename-escapes' are
applied to the filename.
-This setting is used to define the function proof-cd which
+This setting is used to define the function `proof-cd' which
changes to the value of (default-directory) for script buffers.
For files, the value of (default-directory) is simply the
directory the file resides in.
-NB: By default, proof-cd is called from proof-activate-scripting-hook,
+NB: By default, `proof-cd' is called from `proof-activate-scripting-hook',
so that the prover switches to the directory of a proof
script every time scripting begins."
:type 'string
@@ -1524,7 +1482,7 @@ script every time scripting begins."
"Command to turn prover goals output off when sending many script commands.
If non-nil, Proof General will automatically issue this command
to help speed up processing of long proof scripts.
-See also proof-shell-stop-silent-cmd.
+See also `proof-shell-stop-silent-cmd'.
NB: terminator not added to command."
:type '(choice string (const nil))
:group 'proof-shell)
@@ -1533,7 +1491,7 @@ NB: terminator not added to command."
"Command to turn prover output on.
If non-nil, Proof General will automatically issue this command
to help speed up processing of long proof scripts.
-See also proof-shell-start-silent-cmd.
+See also `proof-shell-start-silent-cmd'.
NB: Terminator not added to command."
:type '(choice string (const nil))
:group 'proof-shell)
@@ -1562,8 +1520,8 @@ issuing this command.
If this is set to nil, no command is issued.
-See also: proof-shell-inform-file-retracted-cmd,
-proof-shell-process-file, proof-shell-compute-new-files-list."
+See also: `proof-shell-inform-file-retracted-cmd',
+`proof-shell-process-file', `proof-shell-compute-new-files-list'."
:type '(choice string (const nil))
:group 'proof-shell)
@@ -1590,8 +1548,8 @@ be invoked on the name of the retracted file, and should remove
the ancestor files from `proof-included-files-list' by some
other calculation.
-See also: proof-shell-inform-file-processed-cmd,
-proof-shell-process-file, proof-shell-compute-new-files-list."
+See also: `proof-shell-inform-file-processed-cmd',
+`proof-shell-process-file', `proof-shell-compute-new-files-list'."
:type '(choice string (const nil)) ;; FIXME: or function
:group 'proof-shell)
@@ -1682,7 +1640,7 @@ recognize when the prover has finished processing a command.
To help speed up matching you may be able to annotate the
proof assistant prompt with a special character not appearing
in ordinary output. The special character should appear in
-this regexp, and should be the value of proof-shell-wakeup-char."
+this regexp, and should be the value of `proof-shell-wakeup-char'."
:type 'regexp
:group 'proof-shell)
@@ -1697,15 +1655,15 @@ this regexp, and should be the value of proof-shell-wakeup-char."
We assume that an error message corresponds to a failure in the last
proof command executed. So don't match mere warning messages with
this regexp. Moreover, an error message should not be matched as an
-eager annotation (see proof-shell-eager-annotation-start) otherwise it
+eager annotation (see `proof-shell-eager-annotation-start') otherwise it
will be lost.
-Error messages are considered to begin from proof-shell-error-regexp
+Error messages are considered to begin from `proof-shell-error-regexp'
and continue until the next prompt. The variable
`proof-shell-truncate-before-error' controls whether text before the
error message is displayed.
-The engine matches interrupts before errors, see proof-shell-interrupt-regexp.
+The engine matches interrupts before errors, see `proof-shell-interrupt-regexp'.
It is safe to leave this variable unset (as nil)."
:type '(choice nil regexp)
@@ -1716,9 +1674,9 @@ It is safe to leave this variable unset (as nil)."
If nil, the whole output that the prover generated before the last
error message will be shown.
-NB: the default setting for this is `t' to be compatible with
+NB: the default setting for this is t to be compatible with
behaviour in Proof General before version 3.4. The more obvious
-setting for new instances is probably `nil'.
+setting for new instances is probably nil.
Interrupt messages are treated in the same way.
See `proof-shell-error-regexp' and `proof-shell-interrupt-regexp'."
@@ -1776,10 +1734,10 @@ to a filename."
We assume that an interrupt message corresponds to a failure in the last
proof command executed. So don't match mere warning messages with
this regexp. Moreover, an interrupt message should not be matched as an
-eager annotation (see proof-shell-eager-annotation-start) otherwise it
+eager annotation (see `proof-shell-eager-annotation-start') otherwise it
will be lost.
-The engine matches interrupts before errors, see proof-shell-error-regexp.
+The engine matches interrupts before errors, see `proof-shell-error-regexp'.
It is safe to leave this variable unset (as nil)."
:type '(choice nil regexp)
@@ -1822,7 +1780,7 @@ and possibly analysed further for proof-by-pointing markup."
(defcustom proof-shell-end-goals-regexp nil
"Regexp matching the end of the proof state output, or nil.
-If nil, just use the rest of the output following proof-shell-start-goals-regexp."
+If nil, just use the rest of the output following `proof-shell-start-goals-regexp'."
:type '(choice nil regexp)
:group 'proof-shell)
@@ -1831,7 +1789,7 @@ If nil, just use the rest of the output following proof-shell-start-goals-regexp
An \"eager annotation indicates\" to Proof General that some following output
should be displayed (or processed) immediately and not accumulated for
parsing later. Note that this affects processing of output which is
-ordinarily accumulated: output which appears before the eager annotation
+ordinarily accumulated: output which appears before the eager annotation
start will be discarded.
The start/end annotations can be used to hilight the output, but
@@ -1957,7 +1915,7 @@ A good markup for the second string is to delimit with #'s, since
these are not valid syntax for elisp evaluation.
Elisp errors will be trapped when evaluating; set
-proof-general-debug to be informed when this happens.
+`proof-general-debug' to be informed when this happens.
Example uses are to adjust PG's internal copies of proof assistant's
settings, or to make automatic dynamic syntax adjustments in Emacs to
@@ -2080,7 +2038,36 @@ response buffer."
;;
-;; 5c. hooks and other miscellaneous customizations
+;; 5c. tokens mode: turning on/off tokens output
+;;
+
+(defcustom proof-tokens-activate-command nil
+ "Command to activate token input/output for prover.
+If non-nil, this command is sent to the proof assistant when
+Unicode Tokens support is activated."
+ :type 'string
+ :group 'proof-x-symbol)
+
+(defcustom proof-tokens-deactivate-command nil
+ "Command to deactivate token input/output for prover.
+If non-nil, this command is sent to the proof assistant when
+Unicode Tokens support is deactivated."
+ :type 'string
+ :group 'proof-x-symbol)
+
+(defcustom proof-tokens-extra-modes nil
+ "List of additional mode names to use with Proof General tokens.
+These modes will have Tokens enabled for the proof assistant token language,
+in addition to the four modes for Proof General (script, shell, response, pbp).
+
+Set this variable if you want additional modes to also display
+tokens (for example, editing documentation or source code files)."
+ :type '(repeat symbol)
+ :group 'proof-x-symbol)
+
+
+;;
+;; 5d. hooks and other miscellaneous customizations
;;
(defcustom proof-shell-unicode t
@@ -2157,10 +2144,10 @@ Can be used to configure the proof assistant to the interface in
various ways -- for example, to observe or alter the commands sent to
the prover, or to sneak in extra commands to configure the prover.
-This hook is called inside a `save-excursion' with the proof-shell-buffer
+This hook is called inside a `save-excursion' with the `proof-shell-buffer'
current, just before inserting and sending the text in the
variable `string'. The hook can massage `string' or insert additional
-text directly into the proof-shell-buffer.
+text directly into the `proof-shell-buffer'.
Before sending `string', it will be stripped of carriage returns.
Additionally, the hook can examine the variable `action'. It will be
@@ -2185,9 +2172,7 @@ stripped of carriage returns before being sent.
Example uses:
LEGO uses this hook for setting the pretty printer width if
the window width has changed;
-Plastic uses it to remove literate-style markup from `string'.
-The x-symbol support uses this hook to convert special characters
-into tokens for the proof assistant."
+Plastic uses it to remove literate-style markup from `string'."
:type '(repeat function)
:group 'proof-shell)
@@ -2204,8 +2189,8 @@ Hook functions may inspect `proof-shell-error-or-interrupt-seen' to
determine whether the cause was an error or interrupt. Possible
values for this hook include:
- proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window
- proof-goto-end-of-locked-if-pos-not-visible-in-window
+ `proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window'
+ `proof-goto-end-of-locked-if-pos-not-visible-in-window'
which move the cursor in the scripting buffer on an error or
error/interrupt.
@@ -2217,8 +2202,8 @@ something in scripting buffer, `save-excursion' and/or `set-buffer'."
(defcustom proof-shell-pre-interrupt-hook
nil
- "Run immediately after `comint-interrupt-subjob' is called. This
-hook is added to allow customization for systems that query the user
+ "Run immediately after `comint-interrupt-subjob' is called.
+This hook is added to allow customization for systems that query the user
before returning to the top level."
:type '(repeat function)
:group 'proof-shell)
@@ -2249,18 +2234,9 @@ retracted, or after a command has been sent to the prover with
`proof-shell-invisible-command'.
This hook is used within Proof General to refresh the toolbar."
-
:type '(repeat function)
:group 'proof-shell)
-(defcustom proof-shell-font-lock-keywords nil
- "Value of `font-lock-keywords' used to fontify the proof shell.
-This is currently used only by `proof-easy-config' mechanism, to set
-`font-lock-keywords' before calling `proof-config-done'.
-See also proof-{script,resp,goals}-font-lock-keywords."
- :type 'sexp
- :group 'proof-shell)
-
(defcustom proof-shell-syntax-table-entries nil
"List of syntax table entries for proof script mode.
A flat list of the form
@@ -2343,9 +2319,9 @@ In particular, after a `pbp-goal-command' or a `pbp-hyp-command'."
(defcustom pg-subterm-start-char nil
"Opening special character for subterm markup.
Subsequent special characters with values *below*
-pg-subterm-first-special-char are assumed to be subterm position
-indicators. Annotations should be finished with pg-subterm-sep-char;
-the end of the concrete syntax is indicated by pg-subterm-end-char.
+`pg-subterm-first-special-char' are assumed to be subterm position
+indicators. Annotations should be finished with `pg-subterm-sep-char';
+the end of the concrete syntax is indicated by `pg-subterm-end-char'.
If `pg-subterm-start-char' is nil, subterm markup is disabled.
@@ -2381,31 +2357,19 @@ for parsing the prover output is disabled."
:type 'character
:group 'proof-goals)
-
-
(defcustom proof-goals-font-lock-keywords nil
"Value of `font-lock-keywords' used to fontify the goals output.
-NB: the goals output is not kept in font lock mode because the
-fontification may rely on annotations which are erased before
-displaying. This means internal functions of PG must be used
-to display to the goals buffer to ensure fontification is done!
-This is currently used only by `proof-easy-config' mechanism,
-to set `font-lock-keywords' before calling proof-config-done.
-See also proof-{script,shell,resp}-font-lock-keywords."
+The goals shell mode should set this before calling `proof-goals-config-done'.
+Used also by `proof-easy-config' mechanism.
+See also `proof-{script,goals}-font-lock-keywords'."
:type 'sexp
:group 'proof-goals)
-;; FIXME: perhaps we need new customize group here, "goals" is
-;; not quite right for response buffer!
(defcustom proof-resp-font-lock-keywords nil
"Value of `font-lock-keywords' used to fontify the response output.
-NB: the goals output is not kept in font lock mode because the
-fontification may rely on annotations which are erased before
-displaying. This means internal functions of PG must be used
-to display to the goals buffer to ensure fontification is done!
-This is currently used only by proof-easy-config mechanism,
-to set font-lock-keywords before calling proof-config-done.
-See also proof-{script,shell,resp}-font-lock-keywords."
+The response mode should set this before calling `proof-response-config-done'.
+Used also by `proof-easy-config' mechanism.
+See also `proof-{script,goals}-font-lock-keywords'."
:type 'sexp
:group 'proof-goals)
@@ -2413,70 +2377,20 @@ See also proof-{script,shell,resp}-font-lock-keywords."
"This hook is called before fontifying a region in an output buffer.
A function on this hook can alter the region of the buffer within
the current restriction, and must return the final value of (point-max).
-[This hook is presently only used by phox-sym-lock]."
+\[This hook is presently only used by phox-sym-lock]."
:type '(repeat function)
:group 'proof-goals)
(defcustom pg-after-fontify-output-hook nil
"This hook is called before fonfitying a region in an output buffer.
-[This hook is presently only used by Isabelle]."
+\[This hook is presently only used by Isabelle]."
:type '(repeat function)
:group 'proof-goals)
;;
-;; 7. X-Symbol configuration (see also `pg-custom.el')
-;;
-
-(defgroup proof-x-symbol nil
- "Configuration of X-Symbol for Proof General."
- :group 'prover-config
- :prefix "proof-xsym-")
-
-(defcustom proof-xsym-extra-modes nil
- "List of additional mode names to use X-Symbol with Proof General tokens.
-These modes will have X-Symbol enabled for the proof assistant token language,
-in addition to the four modes for Proof General (script, shell, response, pbp).
-
-Set this variable if you want additional modes to also display
-tokens (for example, editing documentation or source code files)."
- :type '(repeat symbol)
- :group 'proof-x-symbol)
-
-;; FIXME: should perhaps be one of these per prover
-;; FIXME: actually this setting doesn't seem to be needed:
-;; instead X-Symbol uses x-symbol-<lang>-font-lock-keywords.
-(defcustom proof-xsym-font-lock-keywords nil
- "Font lock keywords to use for the proof assistants X-Symbol token language.
-This should be set to the additional font-lock-keywords used for the
-proof assistant when X-Symbol is enabled. (For example, additional
-keywords used for bold or superscript text: see isa/x-symbol-isabelle.el)"
- :type 'sexp
- :group 'proof-x-symbol)
-
-(defcustom proof-xsym-activate-command nil
- "Command to activate token input/output for X-Symbol.
-If non-nil, this command is sent to the proof assistant when
-X-Symbol support is activated."
- :type 'string
- :group 'proof-x-symbol)
-
-(defcustom proof-xsym-deactivate-command nil
- "Command to deactivate token input/output for X-Symbol.
-If non-nil, this command is sent to the proof assistant when
-X-Symbol support is deactivated."
- :type 'string
- :group 'proof-x-symbol)
-
-
-
-
-
-
-
-;;
-;; 8. Global constants
+;; 7. Global constants
;;
(defcustom proof-general-name "Proof-General"
@@ -2497,34 +2411,24 @@ X-Symbol support is deactivated."
:group 'proof-general-internals)
(defcustom proof-universal-keys
- (cons
- (if (featurep 'xemacs)
- '([(control c) \`] . proof-next-error)
- '("`" . proof-next-error))
- '(([(control c) (control c)] . proof-interrupt-process)
- ([(control c) (control n)] . proof-assert-next-command-interactive)
- ([(control c) (control u)] . proof-undo-last-successful-command)
- ([(control c) (control p)] . proof-prf)
- ([(control c) (control l)] . proof-layout-windows)
- ([(control c) (control x)] . proof-shell-exit)
- ([(control c) (control s)] . proof-shell-start)
- ([(control c) (control v)] . proof-minibuffer-cmd)
- ([(control c) (control w)] . pg-response-clear-displays)
- ;; PG 3.6: Some more key bindings moved here from script mode,
- ;; users suggest they ought to work in other PG buffers too.
- ([(control c) (control ?.)] . proof-goto-end-of-locked)
- ([(control c) (control f)] . proof-find-theorems)
- ([(control c) (control o)] . proof-display-some-buffers)))
+ '(([(control c) \`] . proof-next-error) ; ("`" . proof-next-error)
+ ([(control c) (control c)] . proof-interrupt-process)
+ ([(control c) (control n)] . proof-assert-next-command-interactive)
+ ([(control c) (control u)] . proof-undo-last-successful-command)
+ ([(control c) (control p)] . proof-prf)
+ ([(control c) (control l)] . proof-layout-windows)
+ ([(control c) (control x)] . proof-shell-exit)
+ ([(control c) (control s)] . proof-shell-start)
+ ([(control c) (control v)] . proof-minibuffer-cmd)
+ ([(control c) (control w)] . pg-response-clear-displays)
+ ([(control c) (control ?.)] . proof-goto-end-of-locked)
+ ([(control c) (control f)] . proof-find-theorems)
+ ([(control c) (control o)] . proof-display-some-buffers))
"List of key bindings made for the script, goals and response buffer.
Elements of the list are tuples `(k . f)'
where `k' is a key binding (vector) and `f' the designated function."
:type 'sexp
:group 'proof-general-internals)
-
-
-
-
-
(provide 'proof-config)
;;; proof-config.el ends here
diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el
index 0752003b..12b78242 100644
--- a/generic/proof-easy-config.el
+++ b/generic/proof-easy-config.el
@@ -32,17 +32,13 @@
(mode (intern (concat modert hyphen "mode")))
(modename (concat proof-assistant " " suffixnm))
;; FIXME: declare these variables in proof-config:
- ;; proof-{goals,resp,trace}-font-lock-keywords,
;; proof-{goals,resp,trace}-syntax-table-entries
;; FIXME: in future versions, use these settings in *-config-done
;; to simplify elisp code elsewhere.
;; FIXME: add imenu-generic-expression too
;;
- (fntlcks (intern (concat "proof-" suffixnm "-font-lock-keywords")))
(modsyn (intern (concat "proof-" suffixnm "-syntax-table-entries")))
(fullbody (append
- (if (and (boundp fntlcks) (eval fntlcks))
- (list `(setq font-lock-keywords ,fntlcks)))
(if (and (boundp modsyn) (eval modsyn))
(list `(let ((syn ,modsyn))
(while syn
diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el
index 07030623..43a69b22 100644
--- a/generic/proof-maths-menu.el
+++ b/generic/proof-maths-menu.el
@@ -23,8 +23,7 @@
(require 'cl))
(eval-when (compile)
- (if (not (featurep 'xemacs))
- (require 'maths-menu))) ; it's loaded dynamically at runtime
+ (require 'maths-menu)) ; it's loaded dynamically at runtime
;;;###autoload
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 70c0ecfc..b3504701 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -7,7 +7,7 @@
;; $Id$
;;
-(require 'proof) ; proof-deftoggle, proof-eval-when-ready-for-assistant
+(require 'proof-utils) ; proof-deftoggle, proof-eval-when-ready-for-assistant
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
@@ -106,12 +106,8 @@ without adjusting window layout."
;; C-c C-v is proof-minibuffer-cmd in universal-keys
;; C-c C-. is proof-goto-end-of-locked in universal-keys
(define-key map [(control c) (control return)] 'proof-goto-point)
- (define-key map [(control c) v] 'pg-toggle-visibility);; FIXME: Emacs binding?
- (cond ((featurep 'xemacs)
- (define-key map [(control button3)] 'proof-mouse-goto-point)
- (define-key map [(control button1)] 'proof-mouse-track-insert)) ; no Emacs binding
- (t
- (define-key map [(control mouse-3)] 'proof-mouse-goto-point)))
+ (define-key map [(control c) v] 'pg-toggle-visibility)
+ (define-key map [(control mouse-3)] 'proof-mouse-goto-point)
;; NB: next binding overwrites comint-find-source-code.
(define-key map [(meta p)] 'pg-previous-matching-input-from-input)
(define-key map [(meta n)] 'pg-next-matching-input-from-input)
@@ -182,18 +178,16 @@ without adjusting window layout."
(vector
(concat proof-assistant " information")
'proof-help
- menuvisiblep proof-info-command)
+ :visible proof-info-command)
(vector
(concat proof-assistant " web page")
'(browse-url proof-assistant-home-page)
- menuvisiblep proof-assistant-home-page))
+ :visible proof-assistant-home-page))
(proof-ass help-menu-entries))))))))
(defun proof-assistant-menu-update ()
"Update proof assistant menu in scripting buffers."
(proof-map-buffers (proof-buffers-in-mode proof-mode-for-script)
- ;; NB: easy-menu-remove is odd in XEmacs, it considerably changes the mode popup menu.
- ;; In GNU Emacs this first instruction does nothing.
(easy-menu-remove proof-assistant-menu)
(proof-menu-define-settings-menu)
(proof-menu-define-specific)
@@ -275,11 +269,7 @@ without adjusting window layout."
(proof-eval-when-ready-for-assistant
(proof-deftoggle-fn
- (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle)
- (proof-deftoggle-fn
(proof-ass-sym unicode-tokens-enable) 'proof-unicode-tokens-toggle)
-; (proof-deftoggle-fn
-; (proof-ass-sym unicode-tokens2-enable) 'proof-unicode-tokens2-toggle)
(proof-deftoggle-fn
(proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle)
(proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle))
@@ -298,61 +288,43 @@ without adjusting window layout."
"Options"
`(["Electric Terminator" proof-electric-terminator-toggle
:style toggle
- :selected proof-electric-terminator-enable]
+ :selected proof-electric-terminator-enable
+ :help "Automatically send commands as typed"]
["Fly Past Comments" proof-script-fly-past-comments-toggle
- ,menuvisiblep (not proof-script-use-old-parser)
+ :visible (not proof-script-use-old-parser)
:style toggle
- :selected proof-script-fly-past-comments]
+ :selected proof-script-fly-past-comments
+ :help "Coalesce and skip over successive comments"]
["Disppearing Proofs" proof-disappearing-proofs-toggle
:style toggle
- :selected proof-disappearing-proofs]
+ :selected proof-disappearing-proofs
+ :help "Hide proofs as they are completed"]
["Strict Read Only" proof-strict-read-only-toggle
:style toggle
- :selected proof-strict-read-only]
+ :selected proof-strict-read-only
+ :help "Do not allow editing in processed region"]
- ["X-Symbol"
- (progn
- (unless x-symbol-mode (proof-x-symbol-toggle 0))
- (proof-x-symbol-toggle (if x-symbol-mode 0 1)))
- :active (and
- ;; X-Symbol breaks abruptly on recent 23 versions
- (not (>= emacs-major-version 23))
- (not (and (boundp 'unicode-tokens-mode)
- unicode-tokens-mode))
- (proof-x-symbol-support-maybe-available))
- :style toggle
- :selected (and (boundp 'x-symbol-mode) x-symbol-mode)]
-
["Unicode Tokens"
(progn
- (unless unicode-tokens-mode (proof-x-symbol-toggle 0))
(proof-unicode-tokens-toggle (if unicode-tokens-mode 0 1)))
- :active (and (not (and (boundp 'x-symbol-mode) x-symbol-mode))
- (proof-unicode-tokens-support-available))
+ :active (proof-unicode-tokens-support-available)
:style toggle
:selected (and (boundp 'unicode-tokens-mode)
- unicode-tokens-mode)]
-
-;;; ["Unicode Tokens 2"
-;;; (progn
-;;; (unless unicode-tokens2-mode (proof-x-symbol-toggle 0))
-;;; (proof-unicode-tokens2-toggle (if unicode-tokens2-mode 0 1)))
-;;; :active (and (not (and (boundp 'x-symbol-mode) x-symbol-mode))
-;;; (proof-unicode-tokens2-support-available))
-;;; :style toggle
-;;; :selected (and (boundp 'unicode-tokens2-mode)
-;;; unicode-tokens2-mode)]
+ unicode-tokens-mode)
+ :help "Enable display of tokens as Unicode characters"]
["Unicode Maths Menu" (proof-maths-menu-toggle (if maths-menu-mode 0 1))
:active (proof-maths-menu-support-available)
:style toggle
- :selected (and (boundp 'maths-menu-mode) maths-menu-mode)]
+ :selected (and (boundp 'maths-menu-mode) maths-menu-mode)
+ :help "Maths menu for inserting Unicode characters"]
["Multiple Modes" (proof-mmm-toggle (if mmm-mode 0 1))
:active (proof-mmm-support-available)
:style toggle
- :selected (and (boundp 'mmm-mode) mmm-mode)]
+ :selected (and (boundp 'mmm-mode) mmm-mode)
+ :help "Allow multiple major modes"]
["Toolbar" proof-toolbar-toggle
;; should really be split into :active & GNU Emacs's :visible
@@ -364,7 +336,8 @@ without adjusting window layout."
;; we only turn it off in one buffer at a time)
(eq proof-buffer-type 'script))
:style toggle
- :selected proof-toolbar-enable]
+ :selected proof-toolbar-enable
+ :help "Use the Proof General toolbar"]
;;; TODO: Add this in PG 3.7.1 once; see trac #169
;;; ["Response history" proof-keep-response-history-toggle
@@ -374,40 +347,48 @@ without adjusting window layout."
["Index Menu" proof-imenu-toggle
:active (stringp (locate-library "imenu"))
:style toggle
- :selected proof-imenu-enable]
+ :selected proof-imenu-enable
+ :help "Generate an index menu of definitions"]
;; NB: convenience; speedbar isn't saved/resumed automatically.
["Speedbar" speedbar
:active (stringp (locate-library "speedbar"))
:style toggle
- :selected (and (boundp 'speedbar-frame) speedbar-frame)]
+ :selected (and (boundp 'speedbar-frame) speedbar-frame)
+ :help "Use a navigation window (Speedbar)"]
("Display"
- ["Layout Windows" proof-layout-windows]
+ ["Layout Windows" proof-layout-windows
+ :help "Rearrange windows on the screen"]
["Use Three Panes" proof-three-window-toggle
:active (not proof-multiple-frames-enable)
:style toggle
- :selected proof-three-window-enable]
+ :selected proof-three-window-enable
+ :help "Use three panes"]
;; We use non-Emacs terminology "Windows" in this menu to help
;; non-Emacs users. Cf. Gnome usability studies: menus saying
;; "Web Browser" more useful to novices than menus saying "Mozilla"!!
["Multiple Windows" proof-multiple-frames-toggle
:active (and window-system t)
:style toggle
- :selected proof-multiple-frames-enable]
+ :selected proof-multiple-frames-enable
+ :help "Use multiple windows (Emacs frames) for display"]
["Delete Empty Panes" proof-delete-empty-windows-toggle
:active (not proof-multiple-frames-enable)
:style toggle
- :selected proof-delete-empty-windows]
+ :selected proof-delete-empty-windows
+ :help "Dynamically remove empty panes from display"]
["Shrink to Fit" proof-shrink-windows-tofit-toggle
:active (not proof-multiple-frames-enable)
:style toggle
- :selected proof-shrink-windows-tofit])
+ :selected proof-shrink-windows-tofit
+ :help "Dynamically shrink size of output panes to fit contents"])
("Follow Mode"
["Follow Locked Region"
(customize-set-variable 'proof-follow-mode 'locked)
:style radio
- :selected (eq proof-follow-mode 'locked)]
+ :selected (eq proof-follow-mode 'locked)
+ :help "Point follows the locked region"]
;; Not implemented. See Trac #187
;; ["Follow On Success"
;; (customize-set-variable 'proof-follow-mode 'followsuccess)
@@ -416,23 +397,28 @@ without adjusting window layout."
["Follow Locked Region Down"
(customize-set-variable 'proof-follow-mode 'followdown)
:style radio
- :selected (eq proof-follow-mode 'followdown)]
+ :selected (eq proof-follow-mode 'followdown)
+ :help "Point follows the locked region when processsing"]
["Keep Locked Region Displayed"
(customize-set-variable 'proof-follow-mode 'follow)
:style radio
- :selected (eq proof-follow-mode 'follow)]
+ :selected (eq proof-follow-mode 'follow)
+ :help "Scroll to ensure end of lock region is visible"]
["Never Move"
(customize-set-variable 'proof-follow-mode 'ignore)
:style radio
- :selected (eq proof-follow-mode 'ignore)])
+ :selected (eq proof-follow-mode 'ignore)
+ :help "Do not move cursor during processing"])
;; Add this because it's a handy one to set (usually to retract)
("Deactivate Action"
["Retract"
- (customize-set-variable 'proof-auto-action-when-deactivating-scripting 'retract)
+ (customize-set-variable 'proof-auto-action-when-deactivating-scripting
+ 'retract)
:style radio
:selected (eq proof-auto-action-when-deactivating-scripting 'retract)]
["Process"
- (customize-set-variable 'proof-auto-action-when-deactivating-scripting 'process)
+ (customize-set-variable 'proof-auto-action-when-deactivating-scripting
+ 'process)
:style radio
:selected (eq proof-auto-action-when-deactivating-scripting 'process)]
["Query"
@@ -454,7 +440,6 @@ without adjusting window layout."
'proof-disappearing-proofs
;;'proof-output-fontify-enable
'proof-strict-read-only
- (proof-ass-sym x-symbol-enable)
(proof-ass-sym unicode-tokens-enable)
(proof-ass-sym maths-menu-enable)
(proof-ass-sym mmm-enable)
@@ -834,7 +819,7 @@ KEY is the optional key binding."
(proof-assistant-settings-cmd (quote ,name)))))))
(setq proof-assistant-settings
(cons (list name setting (eval type))
- (remassoc name proof-assistant-settings)))))
+ (assq-delete-all name proof-assistant-settings)))))
;;;###autoload
(defmacro defpacustom (name val &rest args)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 0791a56c..38626c5e 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -13,7 +13,7 @@
(require 'cl) ; various
(require 'span) ; abstraction of overlays/extents
-(require 'proof) ; loader (& proof-utils macros)
+(require 'proof-utils) ; proof-utils macros
(require 'proof-syntax) ; utils for manipulating syntax
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -57,7 +57,7 @@ This uses and updates `proof-element-counters'."
(let ((next (1+ (or (cdr-safe (assq idiom proof-element-counters)) 0))))
(setq proof-element-counters
(cons (cons idiom next)
- (remassq idiom proof-element-counters)))
+ (assq-delete-all idiom proof-element-counters)))
next))
(defun proof-element-id (idiom number)
@@ -180,21 +180,22 @@ scripting buffer may have an active queue span.")
;; ** Getters and setters
+(defun proof-span-give-warning (&rest args)
+ "Give a warning message."
+ (message "You should not edit here!"))
+
(defun proof-span-read-only (span &optional always)
"Make SPAN be read-only according to `proof-strict-read-only' or ALWAYS."
- (if (or always proof-strict-read-only)
+ (if (or always (not (memq proof-strict-read-only '(nil retract))))
(span-read-only span)
- (span-read-write span)
- (span-write-warning span)))
+ (span-write-warning span
+ (if (eq proof-strict-read-only 'retract)
+ 'proof-retract-before-change
+ 'proof-span-give-warning))))
(defun proof-strict-read-only ()
"Set locked spans in script buffers according to `proof-strict-read-only'."
- ;; NB: this implements the behaviour that read-only is synchronized
- ;; in all script buffers to follow the current setting of
- ;; `proof-strict-read-only'. Another possibility would be to
- ;; just change for local buffer, while at the same time changing
- ;; the default/global setting. This would be consistent with
- ;; behaviour of "expensive" x-symbol/mmm options.
+ ;; NB: read-only is synchronized in all script buffers
(interactive)
(proof-map-buffers
(proof-buffers-in-mode proof-mode-for-script)
@@ -206,8 +207,22 @@ scripting buffer may have an active queue span.")
((fboundp 'undo-make-selective-list)
(defsubst proof-set-queue-endpoints (start end)
"Set the queue span to be START, END. Discard undo for edits before END."
- (unless (or (eq buffer-undo-list t)
- proof-allow-undo-in-read-only)
+ (unless (or (eq buffer-undo-list t)
+ ;; FIXME: Stefan Monnier writes:
+ ;; This feature simply doesn't work well:
+ ;; - it discards undo info before knowing whether the command
+ ;; succeeds, so if it fails, the undo info corresponding to
+ ;; a still-writable region is lost. Worse yet: this region
+ ;; is the region on which the user is actively working, so
+ ;; it's where undo is most important.
+ ;; - even when it does what it's supposed to do, it's not what
+ ;; we want because the undo info is not recovered when we
+ ;; retract.
+ ;; I.e. it's the wrong place to do it. Better would be to rebind
+ ;; C-x u and C-/ and C-_ to a command that only applies to the
+ ;; writable part of the buffer.
+ t ;; proof-allow-undo-in-read-only
+ )
(setq buffer-undo-list
(undo-make-selective-list end (point-max))))
(span-set-endpoints proof-queue-span start end)))
@@ -517,15 +532,8 @@ This is used for cleaning `buffer-invisibility-spec' in
"Clear record of script portion names and types from internal list.
Also clear all visibility specifications."
(setq pg-script-portions nil)
- (setq buffer-invisibility-spec
- (if (listp buffer-invisibility-spec)
- (apply 'append
- (mapcar (lambda (propellips)
- (if (memq (car-safe propellips)
- pg-visibility-specs)
- nil (list propellips)))
- buffer-invisibility-spec))
- pg-default-invisibility-spec)))
+ (mapcar 'remove-from-invisibility-spec
+ pg-visibility-specs))
(defun pg-add-script-element (elt)
(add-to-list pg-script-portions elt))
@@ -535,8 +543,8 @@ Also clear all visibility specifications."
(newelts (remq id elts)))
(setq pg-script-portions
(if newelts
- (cons (cons ns newelts) (remassq ns pg-script-portions))
- (remassq ns pg-script-portions)))))
+ (cons (cons ns newelts) (assq-delete-all ns pg-script-portions))
+ (assq-delete-all ns pg-script-portions)))))
(defsubst pg-visname (namespace id)
"Return a unique symbol made from strings NAMESPACE and unique ID."
@@ -597,28 +605,23 @@ NAME does not need to be unique."
(defun pg-make-element-invisible (idiom id)
"Make element ID of type IDIOM invisible, with ellipsis."
(let ((visspec (cons (pg-visname idiom id) t)))
- (add-to-list 'buffer-invisibility-spec visspec)
+ (add-to-invisibility-spec visspec)
(add-to-list 'pg-visibility-specs visspec)))
(defun pg-make-element-visible (idiom id)
"Make element ID of type IDIOM visible."
- (setq buffer-invisibility-spec
- (remassq (pg-visname idiom id) buffer-invisibility-spec)))
+ (remove-from-invisibility-spec (pg-visname idiom id)))
(defun pg-toggle-element-visibility (idiom id)
"Toggle visibility of script element of type IDIOM, named ID."
- (if (and (listp buffer-invisibility-spec)
- (assq (pg-visname idiom id) buffer-invisibility-spec))
+ (if (assq (pg-visname idiom id) buffer-invisibility-spec)
(pg-make-element-visible idiom id)
(pg-make-element-invisible idiom id))
(pg-redisplay-for-gnuemacs))
(defun pg-redisplay-for-gnuemacs ()
"GNU Emacs requires redisplay for changes in buffer-invisibility-spec."
- (if (not (featurep 'xemacs))
- ;; GNU Emacs requires redisplay here to see result
- ;; (sit-for 0) not enough
- (redraw-frame (selected-frame))))
+ (redraw-frame (selected-frame)))
(defun pg-show-all-portions (idiom &optional hide)
"Show or hide all portions of kind IDIOM."
@@ -684,13 +687,9 @@ NAME does not need to be unique."
"Prover-processed"))))
(defvar pg-span-context-menu-keymap
- (let ((map (make-sparse-keymap
- "Keymap for context-sensitive menus on spans")))
- (cond
- ((featurep 'xemacs)
- (define-key map [button3] 'pg-span-context-menu))
- ((not (featurep 'xemacs))
- (define-key map [down-mouse-3] 'pg-span-context-menu)))
+ (let ((map (make-sparse-keymap
+ "Keymap for context-sensitive menus on spans")))
+ (define-key map [down-mouse-3] 'pg-span-context-menu)
map)
"Keymap for the span context menu.")
@@ -709,10 +708,8 @@ NAME does not need to be unique."
" ("
(if (span-property span 'idiom)
"with point in region, \\[pg-toggle-visibility] to show/hide; ")
- (if (featurep 'xemacs)
- "\\[popup-mode-menu]"
- "\\<pg-span-context-menu-keymap>\\[pg-span-context-menu]")
- " for menu)"))))
+ "\\<pg-span-context-menu-keymap>\\[pg-span-context-menu]"
+ " for menu)"))))
(span-set-property span 'keymap pg-span-context-menu-keymap)
(unless nohighlight
(span-set-property span 'mouse-face 'proof-mouse-highlight-face))))
@@ -1098,12 +1095,8 @@ a scripting buffer is killed it is always retracted."
;; Turn off Scripting indicator here.
(setq proof-active-buffer-fake-minor-mode nil)
- ;; Make status of inactive scripting buffer show up
- ;; FIXME da:
- ;; not really necessary when called by kill buffer, at least.
- (if (fboundp 'redraw-modeline)
- (redraw-modeline)
- (force-mode-line-update))
+ ;; Make status of inactive scripting buffer show up (necessary?)
+ (force-mode-line-update)
;; Finally, run hooks (added in 3.5 22.04.04)
(run-hooks 'proof-deactivate-scripting-hook))))))
@@ -1185,9 +1178,7 @@ activation is considered to have failed and an error is given."
;; Turn on the minor mode, make it show up.
(setq proof-active-buffer-fake-minor-mode t)
- (if (fboundp 'redraw-modeline)
- (redraw-modeline)
- (force-mode-line-update))
+ (force-mode-line-update)
;; This may be a good time to ask if the user wants to save some
;; buffers. On the other hand, it's jolly annoying to be
@@ -1657,11 +1648,12 @@ to the function which parses the script segment by segment."
;; coalescing a separate configuration option, but
;; it works well used in tandem with the fly-past
;; behaviour.
- (if (and proof-script-fly-past-comments
- (eq type 'comment)
- (eq prevtype 'comment))
- (setq segs (cons seg (cdr segs)))
- (setq segs (cons seg segs)))
+ (setq segs (cons seg
+ (if (and proof-script-fly-past-comments
+ (eq type 'comment)
+ (eq prevtype 'comment))
+ (cdr segs)
+ segs)))
;; Update state
(setq cur (point))
(setq prevtype type)))))
@@ -2163,13 +2155,13 @@ a space or newline will be inserted automatically."
(or ignore-proof-process-p
(if (proof-locked-region-full-p)
(error "Locked region is full, no more commands to do!")))
- (let ((semis))
- (save-excursion
- ;; CHANGE from old proof-assert-until-point: don't bother check
- ;; for non-whitespace between locked region and point.
- ;; CHANGE: ask proof-segment-up-to to scan until command end
- ;; (which it used to do anyway, except in the case of a comment)
- (setq semis (proof-segment-up-to (point) t)))
+ (let ((semis
+ (save-excursion
+ ;; CHANGE from old proof-assert-until-point: don't bother check
+ ;; for non-whitespace between locked region and point.
+ ;; CHANGE: ask proof-segment-up-to to scan until command end
+ ;; (which it used to do anyway, except in the case of a comment)
+ (proof-segment-up-to (point) t))))
;; old code:
;;(if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t))
;; (progn (goto-char pt)
@@ -2194,6 +2186,13 @@ a space or newline will be inserted automatically."
(proof-script-new-command-advance)
(proof-script-next-command-advance))))))
+(defun proof-retract-before-change (beg end)
+ "For use in `before-change-functions'."
+ (and (> (proof-queue-or-locked-end) beg)
+ (save-excursion
+ (goto-char beg)
+ (proof-retract-until-point))))
+
(defun proof-goto-point ()
"Assert or retract to the command at current position.
Calls proof-assert-until-point or proof-retract-until-point as
@@ -2464,23 +2463,6 @@ command."
(setq proof-buffer-type 'script)
- ;; font-lock-keywords isn't automatically buffer-local in Emacs 21.2
- (make-local-variable 'font-lock-keywords)
-
- ;; Syntax table in XEmacs 21.5.b28 does not classify newline as space,
- ;; breaking regexps using \\s- that rely on that (showed up for Coq).
- ;; In fact it seems to be broken rather more seriously than that:
- ;; default syntax table of fundamental mode is not merged at all!
- (if (and (featurep 'xemacs)
- ;; hopefully fixed for later versions but we don't know yet
- (>= 21 emacs-major-version)
- (>= 5 emacs-minor-version))
- (progn
- (derived-mode-merge-syntax-tables
- (standard-syntax-table) (syntax-table))
- ;; We also need this
- (modify-syntax-entry ?\n " ")))
-
;; Set default indent function (can be overriden in derived modes)
(make-local-variable 'indent-line-function)
(setq indent-line-function 'proof-indent-line)
@@ -2557,18 +2539,6 @@ Otherwise just do proof-restart-buffers to delete some spans from memory."
(bury-buffer (current-buffer))))
-;; Notes about how to deal with killing/reverting/renaming buffers:
-;; (As of XEmacs 21.1.9, see files.el)
-;;
-;; Killing: easy, set kill-buffer-hook
-;; Reverting: ditto, set before-revert-hook to do same as kill.
-;; Renaming (write-file): much tricker. Code for write-file does
-;; several odd things. It kills off local hook functions, calls
-;; `after-set-visited-file-name-hooks' right at the end to give the
-;; chance to restore them, but then tends to automatically (re-)set
-;; the mode anyway.
-
-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
@@ -2591,13 +2561,15 @@ This is intended for proof assistant buffers which are similar to
script buffers, but for which scripting is not enabled. In
particular, we: lock the buffer if it appears on
`proof-included-files-list'; configure font-lock support from
-`font-lock-keywords'; maybe turn on X-Symbol minor mode.
+`proof-script-font-lock-keywords'.
This is used for Isabelle theory files, which share some scripting
mode features, but are only ever processed atomically by the proof
assistant."
(setq proof-script-buffer-file-name buffer-file-name)
+ (setq font-lock-defaults '(proof-script-font-lock-keywords))
+
;; Has buffer already been processed?
;; NB: call to file-truename is needed for GNU Emacs which
;; chooses to make buffer-file-truename abbreviate-file-name
@@ -2626,20 +2598,16 @@ assistant."
(unless proof-script-comment-start-regexp
(setq proof-script-comment-start-regexp (regexp-quote proof-script-comment-start)))
(unless proof-script-comment-end-regexp
- (setq proof-script-comment-end-regexp
+ (setq proof-script-comment-end-regexp
(if (string-equal "" proof-script-comment-end)
(regexp-quote "\n") ;; end-of-line terminated comments
(regexp-quote proof-script-comment-end))))
(make-local-variable 'comment-start-skip)
(setq comment-start-skip
- (concat proof-script-comment-start-regexp "+\\s_?"))
-
- ;;
- ;; Fontlock support.
- ;;
- (proof-font-lock-configure-defaults 'autofontify)
-)
+ (if (string-equal "" proof-script-comment-end)
+ (regexp-quote "\n") ;; end-of-line terminated comments
+ (regexp-quote proof-script-comment-end))))
@@ -2770,20 +2738,11 @@ finish setup which depends on specific proof assistant configuration."
;; Common configuration for shared script/other related buffers.
(proof-config-done-related)
- ;; Preamble: make this mode class "pg-sticky" so that renaming file
- ;; to something different doesn't change the mode, no matter what
- ;; the filename. This is a hack so that write-file will work:
- ;; otherwise Emacs insists (XEmacs 21.1.9 onwards) on re-setting the
- ;; mode, which leads to problems with synchronization and losing
- ;; extents. (Attempt to catch this in proof-mode by looking for
- ;; active scripting buffer fails; perhaps because of kill buffer
- ;; function) [NB: could do this at top level at load time]
+ ;; Preamble: make this mode class "pg-sticky" so renaming
+ ;; doesn't change the mode. A hack so that write-file will work.
(put major-mode 'mode-class 'pg-sticky)
- ;; Make X-symbol ignore that we've asked for fixed mode
- (put major-mode 'x-symbol-mode-disable 'ignore)
-
(if (and proof-non-undoables-regexp
(not proof-ignore-for-undo-count))
(setq proof-ignore-for-undo-count
@@ -2831,16 +2790,6 @@ finish setup which depends on specific proof assistant configuration."
(or (buffer-file-name)
(setq buffer-offer-save t))
- ;; Localise the invisibility glyph (XEmacs only):
- (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))
-
;; Finally, make sure the user has been welcomed!
;; [NB: this doesn't work well, can get zapped by loading messages]
(proof-splash-message))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 7eeb6478..bf36dafe 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -81,9 +81,7 @@ to examine proof-shell-last-output.")
;;
(defcustom proof-shell-active-scripting-indicator
- (if (featurep 'xemacs)
- (cons (make-extent nil nil) " Scripting ")
- " Scripting")
+ " Scripting"
"Modeline indicator for active scripting buffer.
If first component is extent it will automatically follow the colour
of the queue region."
@@ -168,12 +166,7 @@ If QUEUEMODE is supplied, set the lock to that value."
(setq proof-shell-error-or-interrupt-seen nil)
(setq proof-shell-busy (or queuemode t))
;; Make modeline indicator follow state (on XEmacs at least)
- (cond
- ((featurep 'xemacs)
- (if (extentp (car proof-shell-active-scripting-indicator))
- (set-extent-properties
- (car proof-shell-active-scripting-indicator)
- '(face proof-queue-face)))))
+ ;; PG4.0: TODO: alter modeline indicator
(run-hooks 'proof-state-change-hook))
(defun proof-release-lock (&optional err-or-int)
@@ -182,13 +175,8 @@ Clear `proof-shell-busy', and set `proof-shell-error-or-interrupt-seen'
to err-or-int."
(setq proof-shell-error-or-interrupt-seen err-or-int)
(setq proof-shell-busy nil)
- (cond
- ((featurep 'xemacs)
- (if (extentp (car proof-shell-active-scripting-indicator))
- (set-extent-properties
- (car proof-shell-active-scripting-indicator)
- '(face proof-locked-face))))))
-
+ ;; PG4.0: TODO: alter modeline indicator
+ )
@@ -403,16 +391,7 @@ Does nothing if proof assistant is already running."
;; new frames (NB: sets specifiers to remove modeline)
(save-selected-window
(save-selected-frame
- (proof-multiple-frames-enable)))
- ;; Otherwise just try to remove modeline from PG buffers
- ;; in XEmacs (FIXME: hope to remove this and just have
- ;; previous case)
- (if (featurep 'xemacs)
- (proof-map-buffers
- (list proof-goals-buffer proof-response-buffer
- proof-trace-buffer proof-thms-buffer)
- (set-specifier has-modeline-p nil (current-buffer))))))
-
+ (proof-multiple-frames-enable)))))
(message "Starting %s process... done." proc))))
@@ -633,14 +612,6 @@ This is a subroutine of `proof-shell-handle-error'."
(setq string (buffer-substring-no-properties start end))
- ;; NB: if the shell buffer were in x-symbol minor mode,
- ;; this string would contain X-Symbol characters, which
- ;; is not suitable for processing with proof-fontify-region.
- ;; Better not to use X-Symbol in the shell.
- (unless (or proof-shell-unicode
- pg-use-specials-for-fontify)
- (setq string
- (pg-assoc-strip-subterm-markup string)))
;; Erase if need be, and erase next time round too.
(pg-response-maybe-erase t nil)
(pg-response-display-with-face string append-face))))
@@ -688,8 +659,6 @@ Then we call `proof-shell-error-or-interrupt-action', which see."
;; [FIXME: Why not flush goals also for interrupts?]
;; Flush goals or response buffer (from some last successful proof step)
(unless proof-shell-no-error-display
- ;; FIXME FIXME FIXME: some terrible memory leak here in XEmacs, when
- ;; next line is executed.
(save-excursion
(proof-shell-handle-delayed-output))
(proof-shell-handle-output
@@ -745,13 +714,13 @@ Then we call `proof-shell-handle-error-or-interrupt-hook'."
(defun proof-pbp-focus-on-first-goal ()
"If the `proof-goals-buffer' contains goals, bring the first one into view.
This is a hook function for proof-shell-handle-delayed-output-hook."
- (and (featurep 'xemacs) ;; FIXME: map-extents exists on Emacs21
- (fboundp 'map-extents) ;; but with different typing
- (let
- ((pos (map-extents 'proof-goals-pos proof-goals-buffer
- nil nil nil nil 'proof-top-element)))
- (and pos (set-window-point
- (get-buffer-window proof-goals-buffer t) pos)))))
+ )
+;; PG 4.0 FIXME
+; (let
+; ((pos (map-extents 'proof-goals-pos proof-goals-buffer
+; nil nil nil nil 'proof-top-element)))
+; (and pos (set-window-point
+; (get-buffer-window proof-goals-buffer t) pos)))))
(defsubst proof-shell-string-match-safe (regexp string)
@@ -870,17 +839,6 @@ which see."
;; Low-level commands for shell communication
;;
-(defconst proof-shell-insert-space-fudge
- (cond
- ((and (featurep 'xemacs)
- (string-match "21.*XEmacs" emacs-version))
- " ")
- ((featurep 'xemacs) "")
- (t " "))
- "String to insert after setting proof marker to prevent it moving.
-Allows for a difference between different versions of comint across
-different Emacs versions.")
-
;;;###autoload
(defun proof-shell-insert (string action)
"Insert STRING at the end of the proof shell, call `comint-send-input'.
@@ -898,8 +856,7 @@ used in `proof-append-alist' when we start processing a queue, and in
(with-current-buffer proof-shell-buffer
(goto-char (point-max))
- ;; This hook allows munging of `string' and other hacks.
- ;; NB: string should not be null
+ ;; Hook for munging `string' and other hacks.
(unless (null string)
(run-hooks 'proof-shell-insert-hook))
@@ -910,19 +867,16 @@ used in `proof-append-alist' when we start processing a queue, and in
(insert (or string "")) ;; robust against call with nil
;; Advance the proof-marker, if synchronization has been gained.
- ;; A null marker position indicates that synchronization is not
- ;; yet gained. (NB: Output before sync gained is ignored!)
+ ;; Null marker => no yet synced; output is ignored.
(unless (null (marker-position proof-marker))
(set-marker proof-marker (point)))
- ;; TODO: consider as possible improvement.
- ;; (set-marker proof-shell-urgent-message-marker (point))
- ;; (set-marker proof-shell-urgent-message-scanner (point))
-
;; FIXME da: this space fudge is actually a visible hack:
;; the response string begins with a space and a newline.
;; It was needed to work around differences in Emacs versions.
- (insert proof-shell-insert-space-fudge)
+ ;; PG 4.0: consider alternative of maintaining marker at
+ ;; position -1
+ (insert " ")
;; Note: comint-send-input perversely calls the output filter
;; functions on the input, sigh. This can mess up PGIP processing
@@ -932,22 +886,6 @@ used in `proof-append-alist' when we start processing a queue, and in
(let ((comint-output-filter-functions nil))
(comint-send-input))))
-;; OLD BUGGY CODE here
-;; Left in as a warning of a race condition.
-;; It seems that comint-send-input can lead to the
-;; output filter running before it returns, so that
-;; the set-marker call below is executed too late.
-;; The result is that the filter deals with
-;; the previous portion of output instead of the
-;; most recent one!
-;;
-;; xemacs and FSF emacs have different semantics for what happens when
-;; shell input is sent next to a marker
-;; the following code accommodates both definitions
-; (let ((inserted (point)))
-; (comint-send-input)
-; (set-marker proof-marker inserted))))
-
;; ============================================================
;;
@@ -1195,12 +1133,7 @@ MESSAGE should be a string annotated with
(pg-assoc-strip-subterm-markup message)))
(unless (and proof-trace-output-slow-catchup
(pg-tracing-tight-loop))
- (proof-display-and-keep-buffer proof-trace-buffer)
- ;; Force redisplay to give feedback in case in a loop which
- ;; keeps Emacs busy processing output. Potentially costly.
- (and (fboundp 'redisplay-frame)
- ;; XEmacs fn
- (redisplay-frame)))
+ (proof-display-and-keep-buffer proof-trace-buffer))
;; If user quits during tracing output, send an interrupt
;; to the prover. Helps when Emacs is "choking".
(if (and quit-flag proof-action-list)
@@ -1469,7 +1402,7 @@ however, are always processed; hence their name)."
(if proof-shell-wakeup-char
;; NB: this match doesn't work in emacs-mule, darn.
;; (string-match (char-to-string proof-shell-wakeup-char) str))
- ;; NB: this match doesn't work in FSF emacs 20.5, darn.
+ ;; NB: this match doesn't work in GNU Emacs 20.5, darn.
;; (find proof-shell-wakeup-char str)
;; So let's use both tests!
(or
@@ -1540,11 +1473,6 @@ however, are always processed; hence their name)."
(buffer-substring-no-properties
(match-beginning 0) (match-end 0)))
(backward-char (- (match-end 0) (match-beginning 0)))
- ;; NB: decoding x-symbols here is probably too
- ;; expensive; moreover it leads to problems
- ;; processing special characters as annotations
- ;; later on. So do not fontify or decode.
- ;; (proof-fontify-region startpos (point))
(setq string (buffer-substring-no-properties
startpos (point)))
(goto-char (point-max))
@@ -1682,35 +1610,6 @@ Only works when system timer has microsecond count available."
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Utility functions
-;;
-(defun proof-shell-dont-show-annotations (&optional buffer)
- "Set display values of annotations in BUFFER to be invisible.
-
-Annotations are characters 128-255."
- (interactive)
- (with-current-buffer (or buffer (current-buffer))
- (let ((disp (make-display-table))
- (i 128))
- (while (< i 256)
- (aset disp i [])
- (incf i))
- (cond ((featurep 'xemacs)
- (add-spec-to-specifier current-display-table disp (current-buffer)))
- ((boundp 'buffer-display-table)
- (setq buffer-display-table disp))))))
-
-(defun proof-shell-show-annotations ()
- "Remove display table specifier from current buffer.
-This function is for testing purposes only, to reveal 8-bit characters
-in the shell buffer. Use proof-shell-dont-show-annotations to turn
-them off again.
-XEmacs only."
- (interactive)
- (if (featurep 'xemacs)
- (remove-specifier current-display-table (current-buffer))))
@@ -1849,12 +1748,6 @@ usual, unless NOERROR is non-nil."
(setq comint-input-ring-size 1)
(setq comint-input-ring (make-ring comint-input-ring-size))
- ;; FIXME: this is a work-around for a nasty GNU Emacs 21.2
- ;; bug which HANGS Emacs sometimes if special characters
- ;; are hidden. (e.g. try M-x column-number-mode)
- (unless (not (featurep 'xemacs))
- (proof-shell-dont-show-annotations))
-
;; Proof marker is initialised in filter to first prompt found
(setq proof-marker (make-marker))
;; Urgent message marker records end position of last urgent
@@ -1865,10 +1758,6 @@ usual, unless NOERROR is non-nil."
(setq proof-shell-urgent-message-scanner (make-marker))
(set-marker proof-shell-urgent-message-scanner (point-min))
- (easy-menu-add proof-shell-mode-menu proof-shell-mode-map)
-
- ;; [ Should already be in proof-goals-buffer, really.]
-
;; FIXME da: before entering proof assistant specific code,
;; we'd do well to check that process is actually up and
;; running now. If not, call the process sentinel function
@@ -1881,11 +1770,6 @@ usual, unless NOERROR is non-nil."
;; shell startup fails. Ugly, but low priority to fix.
);)
-(easy-menu-define proof-shell-mode-menu proof-shell-mode-map
- "Menu used in Proof General shell mode."
- (proof-aux-menu))
-
-
;;
;; Sanity checks on important settings
;;
@@ -1907,7 +1791,7 @@ processing."
(proof-warn-if-unset "proof-shell-config-done" sym))
;; We do not use font-lock here, it's a waste of cycles.
- ;; (proof-font-lock-configure-defaults nil)
+ (font-lock-mode 0)
(let ((proc (get-buffer-process proof-shell-buffer)))
;; Add the kill buffer function and process sentinel
@@ -1944,14 +1828,16 @@ processing."
;; Now send the initialisation commands.
(unwind-protect
(progn
+ (run-hooks 'proof-shell-init-hook)
(if proof-shell-init-cmd
(proof-shell-invisible-command proof-shell-init-cmd t))
(if proof-assistant-settings
- (proof-shell-invisible-command (proof-assistant-settings-cmd) t)))
+ (proof-shell-invisible-command
+ (proof-assistant-settings-cmd) t)))
- ;; Configure for x-symbol or unicode input
- (proof-x-symbol-shell-config)
- (proof-unicode-tokens-shell-config)))))))
+ ;; Configure for unicode input
+ ;(proof-unicode-tokens-shell-config)
+ ))))))
(provide 'proof-shell)
diff --git a/generic/proof-site.el b/generic/proof-site.el
index dcb2deb8..4cb966f4 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -14,7 +14,6 @@
;; can be set to affect load behaviour; see info documentation.
;;
-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Master table of supported proof assistants.
@@ -55,7 +54,7 @@
(eval-and-compile
;; WARNING: do not edit next line (constant is edited in Makefile.devel)
- (defconst proof-general-version "Proof General Version 3.7.1.1. Released by da on Thu 24 Jul 2008."
+ (defconst proof-general-version "Proof General Version 4.0preXXXXXX. Released by da."
"Version string identifying Proof General release."))
(defconst proof-general-short-version
@@ -331,23 +330,5 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
(setq assistants (cdr assistants)))))
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;;
-;;; Disable any other XEmacs x-symbol packages: we load ours manually
-;;;
-
-(if (and
- (featurep 'xemacs)
- (not (featurep 'x-symbol-hooks)) ;; unless already loaded
- (file-exists-p (concat proof-home-directory ;; or our version removed
- "x-symbol/lisp/"))
- ;; proof-try-require: make robust against missing advice package
- (condition-case () (require 'advice) (file-error nil) (featurep 'advice)))
- (defadvice packages-new-autoloads (after ignore-other-x-symbols activate)
- (setq ad-return-value
- (delete-if (lambda (pkg)
- (string-match "x-symbol" pkg))
- ad-return-value))))
-
(provide 'proof-site)
;; proof-site.el ends here
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index c3e644d9..96bd59e4 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -71,16 +71,9 @@ If it is nil, a new line is inserted."
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Compatibility between Emacs/XEmacs.
-(eval-and-compile
- (if (featurep 'xemacs)
- ;; Constant nil function
- (defsubst proof-emacs-imagep (img)
- "See if IMG is an Emacs image descriptor (returns nil here on XEmacs)."
- nil)
- (defsubst proof-emacs-imagep (img)
- "See if IMG is an Emacs image descriptor."
- (and (listp img) (eq (car img) 'image)))))
+(defsubst proof-emacs-imagep (img)
+ "See if IMG is an Emacs image descriptor."
+ (and (listp img) (eq (car img) 'image)))
(defun proof-get-image (name &optional nojpeg default)
@@ -93,29 +86,15 @@ DEFAULT gives return value in case image not valid."
(concat proof-images-directory name ".jpg")))
(gif (vector 'gif :file
(concat proof-images-directory ".gif")))
- (validfn (lambda (inst)
- (and (featurep 'xemacs)
- (valid-instantiator-p inst 'image)
- (file-readable-p (aref inst 2)))))
img)
(cond
- ((and (featurep 'xemacs) window-system
- (featurep 'jpeg) (not nojpeg)
- (funcall validfn jpg))
- jpg)
- ((and (featurep 'xemacs) window-system
- (featurep 'gif) (funcall validfn gif))
- gif)
- ((and
- (not (featurep 'xemacs)) window-system
- (setq img
- (find-image
- (list
- (list :type 'jpeg
- :file (concat proof-images-directory name ".jpg"))
- (list :type 'gif
- :file (concat proof-images-directory name ".gif"))))))
- img)
+ (window-system
+ (find-image
+ (list
+ (list :type 'jpeg
+ :file (concat proof-images-directory name ".jpg"))
+ (list :type 'gif
+ :file (concat proof-images-directory name ".gif")))))
(t
(or default (concat "[ image " name " ]"))))))
@@ -132,9 +111,6 @@ Borrowed from startup-center-spaces."
(fill-area-width (* avg-pixwidth (- fill-column left-margin)))
(glyph-pixwidth (cond ((stringp glyph)
(* avg-pixwidth (length glyph)))
- ((and (featurep 'xemacs)
- (glyphp glyph))
- (glyph-width glyph))
((proof-emacs-imagep glyph)
(car (image-size glyph 'inpixels)))
(t
@@ -163,11 +139,8 @@ Borrowed from startup-center-spaces."
(progn
(if (get-buffer-window splashbuf)
;; Restore the window config if splash is being displayed
- (progn
- (if (cdr proof-splash-timeout-conf)
- (set-window-configuration (cdr proof-splash-timeout-conf)))
- (if (featurep 'xemacs)
- (redraw-frame nil t))))
+ (if (cdr proof-splash-timeout-conf)
+ (set-window-configuration (cdr proof-splash-timeout-conf))))
;; Indicate removed splash screen; disable timeout
(disable-timeout (car proof-splash-timeout-conf))
(setq proof-splash-timeout-conf nil)
@@ -200,72 +173,64 @@ by end of configuring proof mode.
Otherwise, timeout inside this function after 10 seconds or so."
(interactive "P")
(proof-splash-set-frame-titles)
- (let*
- ;; Keep win config explicitly instead of pushing/popping because
- ;; if the user switches windows by hand in some way, we want
- ;; to ignore the saved value. Unfortunately there seems to
- ;; be no way currently to remove the top item of the stack.
- ((winconf (current-window-configuration))
- (curwin (get-buffer-window (current-buffer)))
- (curfrm (and curwin (window-frame curwin)))
- (splashbuf (get-buffer-create proof-splash-welcome))
- (after-change-functions nil) ; no font-lock, thank-you.
- ;; NB: maybe leave next one in for frame-crazy folk
- ;;(pop-up-frames nil) ; display in the same frame.
- (splash-contents (append
- (eval proof-splash-contents)
- (eval proof-splash-startup-msg)))
- s)
- (with-current-buffer splashbuf
- (erase-buffer)
- ;; [ Don't use do-list to avoid loading cl ]
- (while splash-contents
- (setq s (car splash-contents))
- (cond
- ((and (featurep 'xemacs)
- (vectorp s)
- (valid-instantiator-p s 'image))
- (let ((gly (make-glyph s)))
- (indent-to (proof-splash-centre-spaces gly))
- (set-extent-begin-glyph (make-extent (point) (point)) gly)))
- ((proof-emacs-imagep s)
- (indent-to (proof-splash-centre-spaces s))
- (insert-image s))
- ((stringp s)
- (indent-to (proof-splash-centre-spaces s))
- (insert s)))
- (newline)
- (setq splash-contents (cdr splash-contents)))
- (goto-char (point-min))
- (set-buffer-modified-p nil)
- (let* ((splashwin (display-buffer splashbuf))
- (splashfm (window-frame splashwin))
- ;; Only save window config if we're on same frame
- (savedwincnf (if (eq curfrm splashfm) winconf)))
- (delete-other-windows splashwin)
- (if (fboundp 'redisplay-frame)
- (redisplay-frame nil t) ; XEmacs special
- (sit-for 0))
- (setq proof-splash-timeout-conf
- (cons
- (add-timeout (if timeout proof-splash-time 10)
- 'proof-splash-remove-screen nil)
- savedwincnf))))
- ;; PROBLEM: when to call proof-splash-display-screen?
- ;; We'd like to call it during loading/initialising. But it's
- ;; hard to make the screen persist after loading because of the
- ;; action of display-buffer invoked after the mode function
- ;; during find-file.
- ;; To approximate the best behaviour, we assume that this file is
- ;; loaded by a call to proof-mode. We display the screen now and add
- ;; a wait procedure temporarily to proof-mode-hook which prevents
- ;; redisplay until proof-splash-time has elapsed.
- (if timeout
- (add-hook 'proof-mode-hook 'proof-splash-timeout-waiter)
- ;; Otherwise, this was an "about" type of call, so we wait
- ;; for a key press or timeout event
- (proof-splash-timeout-waiter))
- (setq proof-splash-seen t)))
+ (let*
+ ;; Keep win config explicitly instead of pushing/popping because
+ ;; if the user switches windows by hand in some way, we want
+ ;; to ignore the saved value. Unfortunately there seems to
+ ;; be no way currently to remove the top item of the stack.
+ ((winconf (current-window-configuration))
+ (curwin (get-buffer-window (current-buffer)))
+ (curfrm (and curwin (window-frame curwin)))
+ (splashbuf (get-buffer-create proof-splash-welcome))
+ (after-change-functions nil) ; no font-lock, thank-you.
+ ;; NB: maybe leave next one in for frame-crazy folk
+ ;;(pop-up-frames nil) ; display in the same frame.
+ (splash-contents (append
+ (eval proof-splash-contents)
+ (eval proof-splash-startup-msg)))
+ s)
+ (with-current-buffer splashbuf
+ (erase-buffer)
+ ;; [ Don't use do-list to avoid loading cl ]
+ (while splash-contents
+ (setq s (car splash-contents))
+ (cond
+ ((proof-emacs-imagep s)
+ (indent-to (proof-splash-centre-spaces s))
+ (insert-image s))
+ ((stringp s)
+ (indent-to (proof-splash-centre-spaces s))
+ (insert s)))
+ (newline)
+ (setq splash-contents (cdr splash-contents)))
+ (goto-char (point-min))
+ (set-buffer-modified-p nil)
+ (let* ((splashwin (display-buffer splashbuf))
+ (splashfm (window-frame splashwin))
+ ;; Only save window config if we're on same frame
+ (savedwincnf (if (eq curfrm splashfm) winconf)))
+ (delete-other-windows splashwin)
+ (sit-for 10)
+ (setq proof-splash-timeout-conf
+ (cons
+ (add-timeout (if timeout proof-splash-time 10)
+ 'proof-splash-remove-screen nil)
+ savedwincnf))))
+ ;; PROBLEM: when to call proof-splash-display-screen?
+ ;; We'd like to call it during loading/initialising. But it's
+ ;; hard to make the screen persist after loading because of the
+ ;; action of display-buffer invoked after the mode function
+ ;; during find-file.
+ ;; To approximate the best behaviour, we assume that this file is
+ ;; loaded by a call to proof-mode. We display the screen now and add
+ ;; a wait procedure temporarily to proof-mode-hook which prevents
+ ;; redisplay until proof-splash-time has elapsed.
+ (if timeout
+ (add-hook 'proof-mode-hook 'proof-splash-timeout-waiter)
+ ;; Otherwise, this was an "about" type of call, so we wait
+ ;; for a key press or timeout event
+ (proof-splash-timeout-waiter))
+ (setq proof-splash-seen t)))
;;;###autoload
(defun proof-splash-message ()
@@ -285,10 +250,7 @@ Otherwise, timeout inside this function after 10 seconds or so."
"Wait for proof-splash-timeout or input, then remove self from hook."
(while (and proof-splash-timeout-conf ;; timeout still active
(not (input-pending-p)))
- (if (featurep 'xemacs)
- (sit-for 0 t) ; XEmacs: wait without redisplay
- ; (sit-for 1 0 t))) ; FSF: NODISP arg seems broken
- (sit-for 0)))
+ (sit-for 0))
(if proof-splash-timeout-conf ;; not removed yet
(proof-splash-remove-screen))
(if (fboundp 'next-command-event) ; 3.3: Emacs removed this
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 482cc5e0..95bd114d 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -14,9 +14,7 @@
(defun proof-ids-to-regexp (l)
"Maps a non-empty list of tokens `l' to a regexp matching any element"
- (if (featurep 'xemacs)
- (mapconcat (lambda (s) (concat "\\_<" s "\\_>")) l "\\|") ;; old version
- (concat "\\_<\\(?:" (mapconcat 'identity l "\\|") "\\)\\_>")))
+ (concat "\\_<\\(?:" (mapconcat 'identity l "\\|") "\\)\\_>"))
(defun proof-anchor-regexp (e)
"Anchor (\\`) and group the regexp E."
@@ -172,8 +170,6 @@ Meant to be used from `font-lock-keywords'."
;; Functions for doing something like "format" but with customizable
;; control characters.
;;
-;; Added for version 3.1 to help quote funny characters in filenames.
-;;
;;;###autoload
(defun proof-format (alist string)
@@ -236,8 +232,6 @@ return the resulting (string) value."
;;
;; Functions for inserting text into buffer.
;;
-;; Added for version 3.2 to provide more prover specific shortcuts.
-;;
; Taken from Isamode
;
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index f3f389ac..b493aa8c 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -1,36 +1,29 @@
-;; proof-toolbar.el Toolbar for Proof General
+;;; proof-toolbar.el --- Toolbar for Proof General
;;
-;; Copyright (C) 1998,9 David Aspinall / LFCS.
+;; Copyright (C) 1998-2008 David Aspinall / LFCS.
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
-;;
-;; 1. edit-toolbar cannot edit proof toolbar (even in a proof mode)
-;; Need a variable containing a specifier or similar.
-;; (defvar proof-toolbar-specifier nil
-;; "Specifier for proof toolbar.")
-;; This doesn't seem worth fixing until XEmacs toolbar implementation
-;; settles a bit. Enablers don't work too well at the moment.
-
+;;; Commentary:
+;;
;; 2. It's a little bit tricky to add prover-specific items:
;; presently it must be done before this file is loaded.
;; We could improve on that by generating everything on-thy-fly
;; in proof-toolbar-setup.
-
-;; 3. We could consider automatically disabling buttons which are
-;; not configured for the prover, e.g. if proof-info-command is
-;; not set, then the Info button should not be shown.
;;
-;; See `proof-toolbar-entries-default' and `<PA>-toolbar-entries'
-;; in pg-custom for the default generic toolbar and
+;; See `proof-toolbar-entries-default' and `<PA>-toolbar-entries'
+;; in pg-custom for the default generic toolbar and
;; the per-prover toolbar contents variable.
;;
+;;; Code:
(eval-when-compile
(require 'proof-utils))
+
+
(require 'span)
(require 'proof-config)
(require 'proof-autoloads)
@@ -48,9 +41,6 @@
(defun proof-toolbar-enabler (token)
(intern (concat "proof-toolbar-" (symbol-name token) "-enable-p")))
-(defun proof-toolbar-function-with-enabler (token)
- (intern (concat "proof-toolbar-" (symbol-name token) "-with-enabler-p")))
-
;;
;; Now the toolbar icons and buttons
;;
@@ -58,66 +48,47 @@
(defun proof-toolbar-make-icon (tle)
"Make icon variable and icon list entry from a PA-toolbar-entries entry."
(let* ((icon (car tle))
- (tooltip (nth 2 tle))
+ (toolbarp (nth 3 tle))
(iconname (symbol-name icon))
(iconvar (proof-toolbar-icon icon)))
- ;; first declare variable
- ;; (eval
- ;; `(defvar ,iconvar nil
- ;; ,(concat
- ;; "Glyph list for " iconname " button in Proof General toolbar.")))
- ;; FIXME: above doesn't quite work right. However, we only lose
- ;; the docstring which is no big deal.
- ;; now the list entry
- (if tooltip
- (list (list iconvar iconname)))))
-
-
-(defun proof-toolbar-make-toolbar-item (tle)
- "Make a toolbar button descriptor from a PA-toolbar-entries entry."
- (let*
- ((token (nth 0 tle))
- (includep (or (< (length tle) 5) (eval (nth 4 tle))))
- (menuname (and includep (nth 1 tle)))
- (tooltip (and includep (nth 2 tle)))
- (existsenabler (nth 3 tle))
- (enablep (and proof-toolbar-use-button-enablers
- (>= emacs-major-version 21)
- existsenabler))
- (enabler (proof-toolbar-enabler token))
- (enableritem (if enablep (list enabler) t))
- (buttonfn (proof-toolbar-function token))
- (buttonfnwe (proof-toolbar-function-with-enabler token))
- (icon (proof-toolbar-icon token))
- (actualfn
- (if (or enablep (not existsenabler))
- buttonfn
- ;; Add the enabler onto the function if necessary.
- (eval `(defun ,buttonfnwe ()
- (interactive)
- (if (,enabler)
- (call-interactively (quote ,buttonfn))
- (message "Button \"%s\" disabled" ,menuname))))
- buttonfnwe)))
- (if tooltip ;; no tooltip means menu-only item
- (if (featurep 'xemacs)
- (list (vector icon actualfn enableritem tooltip))
- (list (append (list icon actualfn token
- :help tooltip)
- (if enabler (list :enable (list enabler)))))))))
-
-
+ (when toolbarp
+ (set iconvar (concat "epg-" iconname)))))
+
+(defun proof-toolbar-make-toolbar-items (map tles)
+ "Make toolbar button descriptors from a PA-toolbar-entries entry."
+ ;; Entry format: (TOKEN MENUNAME TOOLTIP TOOLBAR-P [VISIBLE-P])
+ (dolist (tle tles)
+ (let* ((token (nth 0 tle))
+ (includep (nth 3 tle))
+ (visiblep (nth 4 tle))
+ (icon (proof-toolbar-icon token))
+ (buttonfn (proof-toolbar-function token))
+ (enabler (proof-toolbar-enabler token))
+ (tooltip (and includep (nth 2 tle)))
+ (props (append
+ (list :help tooltip)
+ (if (fboundp enabler)
+ (list :enable (list enabler)))
+ (if visiblep
+ (list :visible visiblep)))))
+ (if includep
+ (apply 'tool-bar-local-item
+ (eval icon) buttonfn token map props)))))
;;
;; Code for displaying and refreshing toolbar
;;
-(defvar proof-toolbar nil
- "Proof mode toolbar button list. Set in proof-toolbar-build.
-For GNU Emacs, this holds a keymap.")
+(defvar proof-toolbar-map nil
+ "Proof mode toolbar button list. Set in `proof-toolbar-setup'.")
+
+(defun proof-toolbar-available-p ()
+ (and ;; Check toolbar support...
+ window-system
+ (featurep 'tool-bar) ;; GNU Emacs tool-bar library
+ (or (image-type-available-p 'xpm) ;; and XPM
+ (image-type-available-p 'png)))) ;; or PNG
-(deflocal proof-toolbar-itimer nil
- "itimer for updating the toolbar in the current buffer")
;;;###autoload
(defun proof-toolbar-setup ()
@@ -125,106 +96,17 @@ For GNU Emacs, this holds a keymap.")
If `proof-toolbar-enable' is nil, change the current buffer toolbar
to the default toolbar."
(interactive)
- (if
- (and ;; Check toolbar support...
- window-system
- (or (and (featurep 'tool-bar) ; GNU Emacs tool-bar library
- (or (image-type-available-p 'xpm) ;; and XPM
- (image-type-available-p 'png))) ;; or PNG
- (and (featurep 'toolbar) ; or XEmacs toolbar library
- (featurep 'xpm)))) ; and XPM support
-
- ;; Toolbar support is possible.
- (progn
- ;; Check the toolbar has been built.
- (or proof-toolbar (proof-toolbar-build))
-
- ;; Now see if user wants toolbar (this can be changed dyamically).
- (if proof-toolbar-enable
-
- ;; Enable the toolbar in this buffer
- (if (not (featurep 'xemacs))
- ;; For GNU Emacs, we make a local tool-bar-map
- (set (make-local-variable 'tool-bar-map) proof-toolbar)
-
- ;; For XEmacs, we set the toolbar specifier for this buffer.
- (set-specifier default-toolbar proof-toolbar (current-buffer))
- ;; We also setup refresh hackery
- (proof-toolbar-setup-refresh))
-
- ;; Disable the toolbar in this buffer
- (if (not (featurep 'xemacs))
- ;; For GNU Emacs, we remove local value of tool-bar-map
- (kill-local-variable 'tool-bar-map)
- ;; For XEmacs, we remove specifier and disable refresh.
- (remove-specifier default-toolbar (current-buffer))
- (proof-toolbar-disable-refresh)))
-
- ;; Update the display
- (sit-for 0))))
-
-(defun proof-toolbar-build ()
- "Build proof-toolbar."
- (let
- ((icontype ".xpm")
-
- ;; List of icon variable names and their associated image
- ;; files. A list of lists of the form (VAR IMAGE). IMAGE is
- ;; the root name for a file in proof-images-directory. The
- ;; toolbar code expects to find files IMAGE.xpm
- (proof-toolbar-icon-list
- (apply 'append
- (mapcar 'proof-toolbar-make-icon
- (proof-ass toolbar-entries))))
-
- ;; A toolbar descriptor evaluated in proof-toolbar-setup.
- ;; Specifically, a list of sexps which evaluate to entries in
- ;; a toolbar descriptor. The default
- ;; `proof-toolbar-default-button-list' works for any prover.
- (proof-toolbar-button-list
- (append
- (apply 'append (mapcar 'proof-toolbar-make-toolbar-item
- (proof-ass toolbar-entries)))
- (if (featurep 'xemacs)
- (list [:style 3d])))))
-
- ;; First set the button variables to glyphs (bit long-windedly).
- (mapcar
- (lambda (buttons)
- (let ((var (car buttons))
- (iconfiles
- (mapcar (lambda (name)
- (concat proof-images-directory "pg-"
- name
- icontype)) (cdr buttons))))
- (set var
- (if (featurep 'xemacs)
- ;; On XEmacs, icon variable holds a list of glyphs
- (toolbar-make-button-list iconfiles)
- ;; On GNU Emacs, it holds a filename for the icon,
- ;; without path or extension. Watch for clashes with
- ;; icons from other packages!
- (concat "epg-" (eval (cadr buttons)))))))
- proof-toolbar-icon-list)
-
- (if (featurep 'xemacs)
- ;; For XEmacs, we evaluate the specifier.
- (setq proof-toolbar (mapcar 'eval proof-toolbar-button-list))
-
- ;; On GNU Emacs, we need to make a new "key"map.
- (setq proof-toolbar (make-sparse-keymap))
+ (when (proof-toolbar-available-p)
+ (unless proof-toolbar-map
+ (setq proof-toolbar-map (make-sparse-keymap))
(add-to-list 'image-load-path proof-images-directory) ; rude?
- (dolist (but proof-toolbar-button-list)
- (apply
- 'tool-bar-local-item
- (eval (nth 0 but)) ; image filename
- (nth 1 but) ; function symbol
- (nth 2 but) ; dummy key
- proof-toolbar
- (nthcdr 3 but)))) ; remaining properties
- ;; Finished
- ))
-
+ (mapcar 'proof-toolbar-make-icon (proof-ass toolbar-entries))
+ (proof-toolbar-make-toolbar-items proof-toolbar-map
+ (proof-ass toolbar-entries)))
+ (when proof-toolbar-enable
+ (set (make-local-variable 'tool-bar-map) proof-toolbar-map))
+ (when (not proof-toolbar-enable)
+ (kill-local-variable 'tool-bar-map))))
;; Action to take after altering proof-toolbar-enable
(defalias 'proof-toolbar-enable 'proof-toolbar-setup)
@@ -232,215 +114,91 @@ to the default toolbar."
;;;###autoload (autoload 'proof-toolbar-toggle "proof-toolbar")
(proof-deftoggle proof-toolbar-enable proof-toolbar-toggle)
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Toolbar refresh functions (hackery for XEmacs)
-;;
-
-(defun proof-toolbar-setup-refresh ()
- "Enable the XEmacs hackery to update the toolbar."
- (if (featurep 'xemacs) ; skip compilation on GNU Emacs
- (when proof-toolbar-use-button-enablers
- ;; Set the callback for updating the enablers
- (add-hook 'proof-state-change-hook 'proof-toolbar-refresh)
- ;; Also call it whenever text changes in this buffer,
- ;; provided it's a script buffer.
- (if (eq proof-buffer-type 'script)
- (add-hook 'after-change-functions
- 'proof-toolbar-refresh nil t))
- ;; And the interval timer for really refreshing the toolbar
- (setq proof-toolbar-itimer
- (start-itimer "proof toolbar refresh"
- 'proof-toolbar-really-refresh
- 0.5 ; seconds of delay
- 0.5 ; repeated
- t ; count idle time
- t ; pass argument
- (current-buffer))))))
-
-(defun proof-toolbar-disable-refresh ()
- "Disable the XEmacs hackery to update the toolbar."
- (when (featurep 'xemacs) ; skip compilation on GNU Emacs
- (remove-hook 'proof-state-change-hook 'proof-toolbar-refresh)
- (remove-hook 'after-change-functions 'proof-toolbar-refresh)
- (if proof-toolbar-itimer (delete-itimer proof-toolbar-itimer))
- (setq proof-toolbar-itimer nil)))
-
-(deflocal proof-toolbar-refresh-flag nil
- "Flag indicating that the toolbar should be refreshed.")
-
-;; &rest args needed for after change function args
-;; FIXME: don't want to do this in every buffer, really;
-;; we'll have proof-toolbar-refresh-flag defined everywhere.
-(defun proof-toolbar-refresh (&rest args)
- "Set flag to indicate that the toolbar should be refreshed."
- (setq proof-toolbar-refresh-flag t))
-
-(defvar proof-toolbar-enablers
- (mapcar (lambda (tle)
- (list (proof-toolbar-enabler (car tle))))
- (proof-ass toolbar-entries))
- "List of all toolbar's enablers")
-
-(defvar proof-toolbar-enablers-last-state
- nil
- "Last state of the toolbar's enablers")
-
-(defun proof-toolbar-really-refresh (buf)
- "Force refresh of toolbar display to re-evaluate enablers.
-This function needs to be called anytime that enablers may have
-changed state."
- (if (featurep 'xemacs) ; skip compilation on GNU Emacs
- (if ;; Be careful to only add to correct buffer, and if it's live
- (buffer-live-p buf)
- (let ((enabler-state (mapcar 'eval proof-toolbar-enablers)))
- (if
- (not (equal enabler-state proof-toolbar-enablers-last-state))
- (progn
- (setq proof-toolbar-enablers-last-state enabler-state)
- (when (featurep 'xemacs)
- ;; The official way to do this should be
- ;; (set-specifier-dirty-flag default-toolbar)
- ;; but it doesn't work, so we do what VM does instead,
- ;; removing and re-adding.
- (remove-specifier default-toolbar buf)
- (set-specifier default-toolbar proof-toolbar buf)
- ;; We set the dirty flag as well just in case it helps...
- (set-specifier-dirty-flag default-toolbar))
- (setq proof-toolbar-refresh-flag nil))))
- ;; Kill off this itimer if it's owning buffer has died
- (delete-itimer current-itimer))))
-
;;
-;; =================================================================
;;
-;;
-;; GENERIC PROOF TOOLBAR BUTTON FUNCTIONS
+;; Proof General Toolbar and Scripting Menu Functions
+;; --------------------------------------------------
;;
;; Defaults functions are provided below for: up, down, restart
;; Code for specific provers may define the symbols below to use
;; the other buttons: next, prev, goal, qed (images are provided).
;;
;; proof-toolbar-next next function
-;; proof-toolbar-next-enable enable predicate for next (or t)
+;; proof-toolbar-next-enable enable predicate for next
;;
-;; etc.
+;; If no -enable function is defined, button is always enabled.
;;
;; To add support for more buttons or alter the default
;; images, <PA>-toolbar-entries should be adjusted.
;; See proof-config.el for that.
;;
;; Note that since the toolbar is displayed for goals and response
-;; buffers too, enablers and command functions must potentially
-;; switch buffer first.
-;;
+;; buffers too, enablers and command functions must potentially switch
+;; buffer first.
;;
+;; Undo
-;;
-;; Undo button
-;;
+(defalias 'proof-toolbar-undo 'proof-undo-last-successful-command)
-(defun proof-toolbar-undo-enable-p ()
+(defun proof-toolbar-undo-enable-p ()
(proof-with-script-buffer
(and (proof-shell-available-p)
(> (proof-unprocessed-begin) (point-min)))))
-(defalias 'proof-toolbar-undo 'proof-undo-last-successful-command)
+;; Delete
-;;
-;; Delete button (not actually on toolbar)
-;;
+(defalias 'proof-toolbar-delete 'proof-undo-and-delete-last-successful-command)
-(defun proof-toolbar-delete-enable-p ()
+(defun proof-toolbar-delete-enable-p ()
(proof-with-script-buffer
(and (not buffer-read-only)
(proof-shell-available-p)
(> (proof-unprocessed-begin) (point-min)))))
-(defalias 'proof-toolbar-delete 'proof-undo-and-delete-last-successful-command)
-
-
-;;
-;; Lockedend button (not actually on toolbar)
-;;
-
-(defun proof-toolbar-lockedend-enable-p ()
- t)
+;; Lockedend
(defalias 'proof-toolbar-lockedend 'proof-goto-end-of-locked)
+;; Next
-
-
-;;
-;; Next button
-;;
+(defalias 'proof-toolbar-next 'proof-assert-next-command-interactive)
(defun proof-toolbar-next-enable-p ()
(proof-with-script-buffer
(not (proof-locked-region-full-p))))
-(defalias 'proof-toolbar-next 'proof-assert-next-command-interactive)
-
+;; Goto
-;;
-;; Goto button
-;;
+(defalias 'proof-toolbar-goto 'proof-goto-point)
(defun proof-toolbar-goto-enable-p ()
(eq proof-buffer-type 'script))
-(defalias 'proof-toolbar-goto 'proof-goto-point)
-
+;; Retract
-;;
-;; Retract button
-;;
+(defalias 'proof-toolbar-retract 'proof-retract-buffer)
(defun proof-toolbar-retract-enable-p ()
(proof-with-script-buffer
(not (proof-locked-region-empty-p))))
-(defalias 'proof-toolbar-retract 'proof-retract-buffer)
-
+;; Use
-;;
-;; Use button
-;;
-
-(defalias 'proof-toolbar-use-enable-p 'proof-toolbar-next-enable-p)
(defalias 'proof-toolbar-use 'proof-process-buffer)
+(defalias 'proof-toolbar-use-enable-p 'proof-toolbar-next-enable-p)
-;;
-;; Restart button
-;;
-
-(defun proof-toolbar-restart-enable-p ()
- ;; Could disable this unless there's something running.
- ;; But it's handy to clearup extents, etc, I suppose.
- t)
+;; Restart
(defalias 'proof-toolbar-restart 'proof-shell-restart)
-;;
-;; Goal button
-;;
-
-(defun proof-toolbar-goal-enable-p ()
- ;; Goals are always allowed, provided proof-goal-command is set.
- ;; Will crank up process if need be.
- ;; (Actually this should only be available when "no subgoals")
- proof-goal-command)
-
+;; Goal
(defalias 'proof-toolbar-goal 'proof-issue-goal)
+;; QED
-;;
-;; QED button
-;;
+(defalias 'proof-toolbar-qed 'proof-issue-save)
(defun proof-toolbar-qed-enable-p ()
(proof-with-script-buffer
@@ -448,124 +206,85 @@ changed state."
proof-shell-proof-completed
(proof-shell-available-p))))
-(defalias 'proof-toolbar-qed 'proof-issue-save)
-
-;;
-;; State button
-;;
+;; State
-(defun proof-toolbar-state-enable-p ()
- (proof-shell-available-p))
-
(defalias 'proof-toolbar-state 'proof-prf)
+(defalias 'proof-toolbar-state-enable-p 'proof-shell-available-p)
-;;
-;; Context button
-;;
+;; Context
-(defun proof-toolbar-context-enable-p ()
- (proof-shell-available-p))
-
(defalias 'proof-toolbar-context 'proof-ctxt)
+(defalias 'proof-toolbar-context-enable-p 'proof-shell-available-p)
-;;
-;; Info button
-;;
-;; Might as well enable it all the time; convenient trick to
-;; start the proof assistant.
-
-(defun proof-toolbar-info-enable-p ()
- t)
+;; Info
(defalias 'proof-toolbar-info 'proof-help)
-;;
-;; Command button
-;;
-
-(defun proof-toolbar-command-enable-p ()
- (proof-shell-available-p))
+;; Command
(defalias 'proof-toolbar-command 'proof-minibuffer-cmd)
+(defalias 'proof-toolbar-command-enable-p 'proof-shell-available-p)
-;;
-;; Help button
-;;
+;; Help
-(defun proof-toolbar-help-enable-p ()
- t)
-
(defun proof-toolbar-help ()
(interactive)
(info "ProofGeneral"))
-;;
-;; Find button
-;;
+;; Find
-(defun proof-toolbar-find-enable-p ()
- (proof-shell-available-p))
-
(defalias 'proof-toolbar-find 'proof-find-theorems)
+(defalias 'proof-toolbar-find-enable-p 'proof-shell-available-p)
-;;
-;; Visibility button (not on toolbar)
-;;
-
-(defun proof-toolbar-visibility-enable-p ()
- (span-property-safe (span-at (point) 'type) 'idiom))
+;; Visibility (not on toolbar)
(defalias 'proof-toolbar-visibility 'pg-toggle-visibility)
-;;
-;; Interrupt button
-;;
+(defun proof-toolbar-visibility-enable-p ()
+ (span-property-safe (span-at (point) 'type) 'idiom))
-(defun proof-toolbar-interrupt-enable-p ()
- proof-shell-busy)
+;; Interrupt
(defalias 'proof-toolbar-interrupt 'proof-interrupt-process)
-
+(defun proof-toolbar-interrupt-enable-p () proof-shell-busy)
;;
-;; =================================================================
+;; Scripting Menu
;;
-;; Scripting menu built from toolbar functions
-;;
-
-(defun proof-toolbar-make-menu-item (tle)
- "Make a menu item from a PA-toolbar-entries entry."
- (let*
- ((token (car tle))
- (menuname (cadr tle))
- (tooltip (nth 2 tle))
- (enablep (nth 3 tle))
- (fnname (proof-toolbar-function token))
- ;; fnval: remove defalias to get keybinding onto menu;
- ;; NB: function and alias must both be defined for this
- ;; to work!!
- (fnval (if (symbolp (symbol-function fnname))
- (symbol-function fnname)
- fnname)))
- (if menuname
- (list
- (apply 'vector
- (append
- (list menuname fnval)
- (if enablep
- (list ':active (list (proof-toolbar-enabler token))))))))))
+;; TODO: pass in map argument, don't use easymenu.
;;;###autoload
(defun proof-toolbar-scripting-menu ()
"Menu made from the Proof General toolbar commands."
- ;; Prevent evaluation too early here, otherwise this is called
- ;; during compilation when loading files with expanded easy-menu-define
- ;; (e.g. pg-response/proof-aux-menu call)
- (apply 'append
- (mapcar 'proof-toolbar-make-menu-item
- (proof-ass toolbar-entries))))
+ (let (menu)
+ (dolist (tle (proof-ass toolbar-entries))
+ ;; Entry format: (TOKEN MENUNAME TOOLTIP TOOLBAR-P VISIBLE-P)
+ (let* ((token (car tle))
+ (menuname (cadr tle))
+ (tooltip (nth 2 tle))
+ (visiblep (nth 4 tle))
+ (enabler (proof-toolbar-enabler token))
+ (fnname (proof-toolbar-function token))
+ ;; fnval: remove defalias to get keybinding onto menu;
+ ;; NB: function and alias must both be defined for this
+ ;; to work!!
+ (fnval (if (symbolp (symbol-function fnname))
+ (symbol-function fnname)
+ fnname)))
+ (when (and menuname (eval visiblep))
+ (setq menu
+ (cons
+ (vconcat
+ (vector menuname fnval :help tooltip)
+ (if (fboundp enabler)
+ ;; NB: :active not :enable, for easymenu
+ (vector :active (list (proof-toolbar-enabler token))))
+ (if visiblep
+ (vector :visible visiblep)))
+ menu)))))
+ (reverse menu)))
+
-
-;;
(provide 'proof-toolbar)
+;;; proof-toolbar.el ends here
diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el
index d8a68e88..99434c57 100644
--- a/generic/proof-unicode-tokens.el
+++ b/generic/proof-unicode-tokens.el
@@ -1,4 +1,4 @@
-;; proof-unicode-tokens.el Support Unicode tokens package
+;;; proof-unicode-tokens.el --- Support Unicode tokens package
;;
;; Copyright (C) 2008 David Aspinall / LFCS Edinburgh
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
@@ -6,6 +6,17 @@
;;
;; $Id$
;;
+;;
+;;; Commentary:
+;;
+;; Support for Unicode Tokens package: per-prover global enabling, copying
+;; configuration tables, adding mode hooks to turn on/off.
+;;
+;; Initialisation:
+;; proof-unicode-tokens-init -> proof-unicode-tokens-reconfigure*
+;;
+
+;;; Code:
(eval-when-compile
(require 'proof-utils) ; for proof-ass, proof-eval-when-ready-for-assistant
@@ -18,125 +29,114 @@
"Flag indicating whether or not we've performed startup.")
(defun proof-unicode-tokens-init ()
- "Initialise settings for unicode tokens from prover specific variables."
+ "Set tables and configure hooks for modes."
+ (proof-unicode-tokens-configure)
+ (add-hook 'proof-shell-init-hook 'proof-unicode-tokens-configure-prover)
+ (let ((hooks (mapcar (lambda (m)
+ (intern (concat (symbol-name m) "-hook")))
+ (list
+ proof-mode-for-script
+ proof-mode-for-response
+ proof-mode-for-goals))))
+ (dolist (hook hooks)
+ (add-hook hook 'proof-unicode-tokens-mode-if-enabled)))
+ (setq proof-unicode-tokens-initialised t))
+
+(defun proof-unicode-tokens-configure ()
+ "Set the Unicode Tokens table from prover instances and initialise."
+ (require 'unicode-tokens) ; load now, for unicode-tokens-configuration-variables
(mapcar
(lambda (var) ;; or defass?
(if (boundp (proof-ass-symv var))
(set (intern (concat "unicode-tokens-" (symbol-name var)))
(eval `(proof-ass ,var)))))
- '(charref-format
- token-format
- control-token-format
- token-name-alist
- glyph-list
- token-match
- control-token-match
- hexcode-match
- next-character-regexp
- token-prefix
- token-suffix
- shortcut-alist))
- (unicode-tokens-initialise)
- (setq proof-unicode-tokens-initialised t))
+ unicode-tokens-configuration-variables)
+ (unicode-tokens-initialise))
+
;;;###autoload
(defun proof-unicode-tokens-enable ()
"Turn on or off Unicode tokens mode in Proof General script buffer.
This invokes `unicode-tokens-mode' to toggle the setting for the current
buffer, and then sets PG's option for default to match.
-Also we arrange to have unicode tokens mode turn itself on automatically
-in future if we have just activated it for this buffer."
+Also we arrange to have unicode tokens mode turn itself on automatically
+in future if we have just activated it for this buffer.
+Note: this function is called when the customize setting for the prover
+is changed."
(interactive)
(when (proof-unicode-tokens-support-available) ;; loads unicode-tokens
(unless proof-unicode-tokens-initialised
(proof-unicode-tokens-init))
(proof-unicode-tokens-set-global (not unicode-tokens-mode))))
+(defun proof-unicode-tokens-mode-if-enabled ()
+ "Turn on or off the Unicode Tokens minor mode in this buffer."
+ (unicode-tokens-mode
+ (if (proof-ass unicode-tokens-enable) 1 0)))
;;;###autoload
(defun proof-unicode-tokens-set-global (flag)
"Set global status of unicode tokens mode for PG buffers to be FLAG.
Turn on/off menu in all script buffers and ensure new buffers follow suit."
- (unless proof-unicode-tokens-initialised
- (proof-unicode-tokens-init))
- (let ((hook (proof-ass-sym mode-hook)))
- (if flag
- (add-hook hook 'unicode-tokens-mode)
- (remove-hook hook 'unicode-tokens-mode))
- (proof-map-buffers
- (proof-buffers-in-mode proof-mode-for-script)
- (unicode-tokens-mode (if flag 1 0)))
- (proof-unicode-tokens-shell-config)))
-
+ (unless proof-unicode-tokens-initialised
+ (proof-unicode-tokens-init))
+ ;; Configure if already running
+ (proof-map-buffers
+ (append
+ (proof-buffers-in-mode proof-mode-for-script)
+ (proof-associated-buffers)
+ (proof-buffers-in-mode proof-tokens-extra-modes))
+ (unicode-tokens-mode (if flag 1 0)))
+ (proof-unicode-tokens-configure-prover))
;;;
;;; Interface to custom to dynamically change tables (via proof-set-value)
;;;
-(defun proof-token-name-alist ()
- "Function called after the current token name alist has been changed.
-Switch off tokens in all buffers, recalculate maps, turn on again."
+(defun proof-unicode-tokens-reconfigure ()
+ "Function called after a token configuration is changed.
+Switch off tokens in all script buffers, recalculate maps, turn on again."
+ (interactive)
(when proof-unicode-tokens-initialised ; not on startup
(when (proof-ass unicode-tokens-enable)
- (proof-map-buffers
+ (proof-map-buffers
(proof-buffers-in-mode proof-mode-for-script)
(unicode-tokens-mode 0)))
- (setq unicode-tokens-token-name-alist (proof-ass token-name-alist))
- (unicode-tokens-initialise)
+ (proof-unicode-tokens-configure)
(when (proof-ass unicode-tokens-enable)
- (proof-map-buffers
+ (proof-map-buffers
(proof-buffers-in-mode proof-mode-for-script)
(unicode-tokens-mode 1)))))
-
-(defun proof-shortcut-alist ()
- "Function called after the shortcut alist has been changed.
-Updates the input mapping for reading shortcuts."
- (when proof-unicode-tokens-initialised ; not on startup
- (setq unicode-tokens-shortcut-alist (proof-ass shortcut-alist))
- (unicode-tokens-initialise)))
+
+(eval-after-load "unicode-tokens"
+ '(dolist (var unicode-tokens-configuration-variables)
+ (funcall 'defalias
+ (intern (concat "proof-" (symbol-name var)))
+ 'proof-unicode-tokens-reconfigure)))
;;;
;;; Interface to shell
;;;
+(defun proof-unicode-tokens-configure-prover ()
+ (if (proof-ass unicode-tokens-enable)
+ (proof-unicode-tokens-activate-prover)
+ (proof-unicode-tokens-deactivate-prover)))
(defun proof-unicode-tokens-activate-prover ()
- (when (and proof-xsym-activate-command
+ (when (and proof-tokens-activate-command
(proof-shell-live-buffer)
(proof-shell-available-p))
(proof-shell-invisible-command-invisible-result
- proof-xsym-activate-command)))
+ proof-tokens-activate-command)))
(defun proof-unicode-tokens-deactivate-prover ()
- (when (and proof-xsym-deactivate-command
- ;; NB: clash with X-symbols since use same commands in prover!
- (not (proof-ass x-symbol-enable))
+ (when (and proof-tokens-deactivate-command
(proof-shell-live-buffer)
(proof-shell-available-p))
(proof-shell-invisible-command-invisible-result
- proof-xsym-deactivate-command)))
-
-;;; NB: we shouldn't bother load this if it's not enabled.
-;;;###autoload
-(defun proof-unicode-tokens-shell-config ()
- (when (proof-ass unicode-tokens-enable)
- (add-hook 'proof-shell-insert-hook
- 'proof-unicode-tokens-encode-shell-input)
- (proof-unicode-tokens-activate-prover))
- (unless (proof-ass unicode-tokens-enable)
- (remove-hook 'proof-shell-insert-hook
- 'proof-unicode-tokens-encode-shell-input)
- (proof-unicode-tokens-deactivate-prover)))
-
-(defun proof-unicode-tokens-encode-shell-input ()
- "Encode shell input in the variable STRING.
-A value for proof-shell-insert-hook."
- (if (proof-ass unicode-tokens-enable)
- (with-temp-buffer ;; TODO: better to do directly in *prover*
- (insert string)
- (unicode-tokens-unicode-to-tokens)
- (setq string (buffer-substring-no-properties
- (point-min) (point-max))))))
+ proof-tokens-deactivate-command)))
(provide 'proof-unicode-tokens)
-;; End of proof-unicode-tokens.el
+
+;;; proof-unicode-tokens.el ends here
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index c0b54cbc..c016c686 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -26,9 +26,7 @@
;;
(eval-and-compile
(defun pg-emacs-version-cookie ()
- (format (if (string-match "XEmacs" emacs-version)
- ;; (featurep 'xemacs) gets optimised!!
- "XEmacs %d.%d" "GNU Emacs %d.%d")
+ (format "GNU Emacs %d.%d"
emacs-major-version emacs-minor-version))
(defconst pg-compiled-for
@@ -36,7 +34,8 @@
"Version of Emacs we're compiled for (or running on, if interpreted)."))
(if (or (not (boundp 'emacs-major-version))
- (< emacs-major-version 21))
+ (< emacs-major-version 22)
+ (string-match "XEmacs" emacs-version))
(error "Proof General is not compatible with Emacs %s" emacs-version))
(unless (equal pg-compiled-for (pg-emacs-version-cookie))
@@ -331,148 +330,6 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
(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 latter.
-;;
-;; * 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) for
-compatibility with X-Symbol, which may hack `font-lock-keywords'
-with extra patterns (in non-mule mode).")
-
-(defun proof-font-lock-configure-defaults (autofontify)
- "Set defaults for font-lock based on current font-lock-keywords.
-This is a delicate operation, because we only want to use font-lock-mode
-in some buffers, so we have to tread carefully around the font-lock
-code to avoid it turning itself on in the buffers where that actually
-*breaks* fontification.
-
-AUTOFONTIFY must be nil for buffers where we may want to really use
-font-lock-mode; in those buffers, we enable syntactic fontification also."
- ;;
- ;; 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.
- ;;
- (setq proof-font-lock-keywords font-lock-keywords)
-
- ;; Setting font-lock-defaults explicitly is required by FSF Emacs
- ;; 20.4's version of font-lock in any case.
-
- (if autofontify
- (progn
- (make-local-variable 'font-lock-defaults) ; needed??
- (setq font-lock-defaults '(proof-font-lock-keywords))
- ;; 12.1.99: For XEmacs, we must also set the mode 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))
- ;; 11.12.01: Emacs 21 is very eager about turning on font
- ;; lock and has hooks all over the place to do it. To make
- ;; sure it doesn't happen we have to eradicate all sense of
- ;; having any fontification ability.
- (proof-font-lock-clear-font-lock-vars)
- ;; In fact, this still leaves font-lock switched on! But
- ;; hopefully in a useless way. XEmacs has better control
- ;; over which modes not to enable it for (although annoying
- ;; that it's a custom setting)
- (if (featurep 'xemacs)
- (setq font-lock-mode-disable-list
- (cons major-mode font-lock-mode-disable-list)))))
-
-(defun proof-font-lock-clear-font-lock-vars ()
- (kill-local-variable 'font-lock-defaults)
- (kill-local-variable 'font-lock-keywords)
- (setq font-lock-keywords nil)
- (put major-mode 'font-lock-defaults nil))
-
-(defun proof-font-lock-set-font-lock-vars ()
- (setq font-lock-defaults '(proof-font-lock-keywords))
- (setq font-lock-keywords proof-font-lock-keywords))
-
-(defun proof-fontify-region (start end &optional keepspecials)
- "Fontify and decode X-Symbols in region START...END.
-Fontifies (keywords only) according to the buffer's font lock defaults.
-Uses `proof-x-symbol-decode-region' to decode tokens
-if X-Symbol is enabled.
-Uses `unicode-tokens-tokens-to-unicode' to decode tokens
-if unicode symbols are enabled.
-
-If `pg-use-specials-for-fontify' is set, remove characters
-with top bit set after fontifying so they don't spoil cut and paste,
-unless KEEPSPECIALS is set to override this.
-
-Returns new END value."
- ;; We fontify first because X-sym 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.
- ;; NB: perhaps we can narrow within the whole function, but there
- ;; was an earlier problem with doing that.
- (when proof-output-fontify-enable
- (let ((normal-font-lock-verbose font-lock-verbose))
- ;; Temporarily set font-lock defaults
- (proof-font-lock-set-font-lock-vars)
- (setq font-lock-verbose nil) ; prevent display glitches in XEmacs
-
- ;; Yukky hacks to immorally interface with font-lock
- (unless (featurep 'xemacs)
- (font-lock-set-defaults))
- (let ((font-lock-keywords proof-font-lock-keywords))
- (if (and (featurep 'xemacs)
- (>= emacs-major-version 21)
- (>= emacs-minor-version 4)
- (not font-lock-cache-position))
- (progn
- (setq font-lock-cache-position (make-marker))
- (set-marker font-lock-cache-position 0)))
-
- (save-restriction
- (narrow-to-region start end)
- (run-hooks 'pg-before-fontify-output-hook)
- (setq end (point-max)))
- ;; da: protect against "Nesting too deep for parser" in bad XEmacs
- (condition-case err
- (font-lock-default-fontify-region start end nil)
- (t (proof-debug
- "Caught condition %s in `font-lock-default-fontify-region'"
- (car err)))))
-
- (save-restriction
- (narrow-to-region start end)
- (run-hooks 'pg-after-fontify-output-hook)
- (setq end (point-max)))
-
- (prog1 ;; prog1 because we return new END value.
- (cond
- ((proof-ass x-symbol-enable)
- (proof-x-symbol-decode-region start end))
- ((proof-ass unicode-tokens-enable)
- (unicode-tokens-tokens-to-unicode start end)))
- (proof-font-lock-clear-font-lock-vars)
- (setq font-lock-verbose normal-font-lock-verbose)))))
(defun pg-remove-specials (&optional start end)
"Remove special characters in region. Default to whole buffer.
@@ -489,15 +346,6 @@ Leave point at END."
-;; FIXME todo: add toggle for fontify region which turns it on/off
-
-(defun proof-fontify-buffer ()
- "Call proof-fontify-region on whole buffer."
- (proof-fontify-region (point-min) (point-max)))
-
-
-
-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Messaging and display functions
@@ -588,9 +436,18 @@ Ensure that point is visible in window."
(skip-chars-backward "\n\t "))
;; Ensure point visible. Again, window may have died
;; inside shrink to fit, for some reason
- (if (window-live-p window)
- (unless (pos-visible-in-window-p (point) window)
- (recenter -1)))))))))
+ (when (window-live-p window)
+ (unless (pos-visible-in-window-p (point) window)
+ (recenter -1))
+ (with-current-buffer buffer
+ (if (window-bottom-p window)
+ (unless (local-variable-p 'mode-line-format)
+ ;; Don't show any mode line.
+ (set (make-local-variable 'mode-line-format) nil))
+ (unless mode-line-format
+ ;; If the buffer gets displayed elsewhere, re-add
+ ;; the modeline.
+ (kill-local-variable 'mode-line-format)))))))))))
(defun proof-clean-buffer (buffer)
"Erase buffer and hide from display if proof-delete-empty-windows set.
@@ -631,41 +488,24 @@ The warning is coloured with proof-warning-face."
If proof-general-debug is nil, do nothing."
(if proof-general-debug
(let ((formatted (apply 'format msg args)))
- (if (fboundp 'display-warning) ;; use builtin warning system in XEmacs
- (display-warning 'proof-general formatted 'info)
- ;; otherwise use response buffer with dedicated font, & display it
- (progn
- (pg-response-display-with-face formatted 'proof-debug-message-face)
- (proof-display-and-keep-buffer proof-response-buffer))))))
+ (display-warning 'proof-general formatted 'info))))
-;;; A handy utility function used in the "Buffers" menu, and throughout
-;; the code.
+;; Utility used in the "Buffers" menu, and throughout
(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)
+ (and (buffer-live-p buf) ; maybe use proof-display-and-keep-buffer ?
(unless (eq buf (window-buffer (selected-window)))
(if noselect
- ;; FIXME: would like 'norecord arg here to override
- ;; previous window entering top of MRU list here.
- ;; In fact, this could be hacked in XEmacs code.
- ;; GNU Emacs seems *not* to put previously displayed
- ;; window onto the top of the list with record-buffer:
- ;; that gives much nicer behaviour than XEmacs here.
(display-buffer buf 'not-this-window)
(let ((pop-up-windows t))
- (pg-pop-to-buffer buf 'not-this-window 'norecord))))))
+ (pop-to-buffer buf 'not-this-window 'norecord))))))
;; Originally based on `shrink-window-if-larger-than-buffer', which
-;; has a pretty wierd implementation.
-;; TODO: desirable improvements would be to add some crafty history based
-;; on user resize-events. E.g. user resizes window, that becomes the
-;; new maximum size.
+;; has a pretty weird implementation.
;; FIXME: GNU Emacs has useful "window-size-fixed" which we use
;; HOWEVER, it's still not quite the right thing, it seems to me.
;; We'd like to specifiy a *minimum size* for a given buffer,
@@ -712,20 +552,29 @@ or if the window is the only window of its frame."
;;; ((cur-height (window-height window))
;; Most window is allowed to grow to
((max-height
- (/ (frame-height (window-frame window))
- (if proof-three-window-enable
- ;; we're in three-window-mode with
- ;; all horizontal splits, so share the height.
- 3
- ;; Otherwise assume a half-and-half split
- 2)))
- ;; If buffer ends with a newline, ignore it when counting
- ;; height unless point is after it.
- (extraline
- (if (and (not (eobp))
- (eq ?\n (char-after (1- (point-max)))))
- 1 0))
- (test-pos (- (point-max) extraline))
+ (/ (frame-height (window-frame window))
+ (if proof-three-window-enable
+ ;; we're in three-window-mode with
+ ;; all horizontal splits, so share the height.
+ 3
+ ;; Otherwise assume a half-and-half split.
+ 2)))
+ ;; I find that I'm willing to use a bit more than the max in
+ ;; those cases where it allows me to see the whole
+ ;; response/goal. --Stef
+ (absolute-max-height
+ (truncate
+ (/ (frame-height (window-frame window))
+ (if proof-three-window-enable
+ ;; we're in three-window-mode with
+ ;; all horizontal splits, so share the height.
+ 2
+ ;; Otherwise assume a half-and-half split.
+ 1.5))))
+ ;; If buffer ends with a newline and point is right after it, then
+ ;; add a final empty line (to display the cursor).
+ (extraline (if (and (eobp) (bolp)) 1 0))
+ ;; (test-pos (- (point-max) extraline))
;; Direction of resizing based on whether max position is
;; currently visible. [ FIXME: not completely sensible:
;; may be displaying end fraction of buffer! ]
@@ -736,32 +585,17 @@ or if the window is the only window of its frame."
;; buffers? Probably not an issue for us, but one
;; wonders at the shrink to fit strategy.
;; NB: way to calculate pixel fraction?
- (+ extraline 1 (count-lines (point-min) (point-max)))))
+ (+ extraline (count-lines (point-min) (point-max)))))
;; Let's shrink or expand. Uses new GNU Emacs function.
(let ((window-size-fixed nil))
- (set-window-text-height window desired-height))
-;; (cond
-;; ((and shrink
-;; (> cur-height window-min-height)
-;; ;; don't shrink if already too big; leave where it is
-;; (< cur-height max-height))
-;; (with-selected-window
-;; window
-;; (shrink-window (- cur-height (max window-min-height desired-height)))))
-;; (;; expand
-;; (< cur-height max-height)
-;; (with-selected-window window
-;; (enlarge-window
-;; (- (min max-height desired-height) cur-height)))))
- ;; If we're at least the desirable height, it must be that the
- ;; whole buffer can be seen --- so make sure display starts at
- ;; beginning.
- ;; NB: shrinking windows can sometimes delete them
- ;; (although we don't want it to here!), but make this next
- ;; check for robustness.
+ (set-window-text-height window
+ ;; As explained earlier: use abs-max-height
+ ;; but only if that makes it display all.
+ (if (> desired-height absolute-max-height)
+ max-height desired-height)))
(if (window-live-p window)
(progn
- (if (>= (window-height window) desired-height)
+ (if (>= (window-text-height window) desired-height)
(set-window-start window (point-min)))
;; window-size-fixed is a GNU Emacs buffer local variable
;; which determines window size of buffer.
@@ -784,8 +618,7 @@ or if the window is the only window of its frame."
(reporter-submit-bug-report
"da+pg-bugs@inf.ed.ac.uk"
"Proof General"
- (list 'proof-general-version 'proof-assistant
- 'x-symbol-version)
+ (list 'proof-general-version 'proof-assistant)
nil nil
"*** Proof General now uses Trac for project management and bug reporting, please go to:
***
@@ -881,6 +714,9 @@ The name of the defined function is returned."
;;; Macris for defining user-level functions (previously in proof-menu.el)
;;;
+(defun proof-escape-keymap-doc (string)
+ ;; avoid work of substitute-command-keys
+ (replace-in-string string "\\\\" "\\\\=\\\\"))
(defmacro proof-defshortcut (fn string &optional key)
"Define shortcut function FN to insert STRING, optional keydef KEY.
@@ -892,7 +728,7 @@ KEY is added onto proof-assistant map."
(define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
(defun ,fn ()
,(concat "Shortcut command to insert "
- (replace-in-string string "\\\\" "\\\\=") ;; for substitute-command-keys
+ (proof-escape-keymap-doc string)
" into the current buffer.\nThis simply calls `proof-insert', which see.")
(interactive)
(proof-insert ,string))))
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
deleted file mode 100644
index 2fdc0f83..00000000
--- a/generic/proof-x-symbol.el
+++ /dev/null
@@ -1,337 +0,0 @@
-;; proof-x-symbol.el Support for X-Symbol package
-;;
-;; Copyright (C) 1998-2002 LFCS Edinburgh
-;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
-;; Id: $Id$
-;;
-;; The X-Symbol package is at http://x-symbol.sourceforge.net/
-;;
-;; With enormous thanks to David von Oheimb for providing the original
-;; patches for using X-Symbol with Isabelle Proof General, and
-;; of course, to Christoph Wedler for providing the wonderful
-;; X-Symbol package in the first place. Christoph also helped
-;; with configuration and tweaks in X-Symbol for Proof General.
-;;
-;; ================================================================
-;;
-;; NB: X-Symbol is now bundled with Proof General, and PG will select
-;; it's own version before any other version on the Emacs load path.
-;; If you want to override this, simply load your version before
-;; starting Emacs, with (require 'x-symbol-hooks).
-;;
-;; =================================================================
-;;
-;; Notes on interacing to X-Symbol.
-;;
-;; 1. Proof script buffers.
-;; Font lock and X-Symbol minor modes are engaged as usual. We use
-;; proof-x-symbol-enable to add/remove PG buffers to X-Symbol's
-;; auto-mode list.
-;;
-;; 2. Output buffers (goals, response, tracing)
-;; Neither font-lock nor X-Symbol mode is engaged. Instead, we simply
-;; set `x-symbol-language', and call `x-symbol-decode' or
-;; `x-symbol-decode-region', via `proof-fontify-region' (which see).
-;;
-;; ================================================================
-;;
-;; Ideally this file ought to be standalone so that the X-Symbol mode
-;; for particular proof assistants may be used elsewhere (e.g. in
-;; document modes), without loading all of Proof General.
-;;
-;; =================================================================
-
-(eval-when-compile
- (require 'proof-utils)) ; proof-ass
-
-(require 'proof-config) ; variables
-(require 'proof-autoloads) ;
-
-
-(defvar proof-x-symbol-initialized nil
- "Non-nil if x-symbol support has been initialized.")
-
-(defun proof-x-symbol-tokenlang-file ()
- "Return filename (sans extension) of token language file."
- (concat "x-symbol-"
- (symbol-name proof-assistant-symbol)))
-
-;;;###autoload
-(defun proof-x-symbol-support-maybe-available ()
- "A test to see whether x-symbol support may be available."
- (and
- (or (featurep 'x-symbol-hooks)
- (and window-system
- (progn
- ;; put bundled version on load path
- (setq load-path
- (cons
- (concat proof-home-directory "x-symbol/lisp/")
- load-path))
- ;; avoid warning about installing in proper place
- (setq x-symbol-data-directory
- (concat proof-home-directory "x-symbol/etc/"))
- ;; *should* always succeed unless bundled version broken
- (proof-try-require 'x-symbol-hooks))))
- ;; See if there is prover-specific config in x-symbol-<foo>.el
- (if (locate-library (proof-x-symbol-tokenlang-file)) t)))
-
-
-(defun proof-x-symbol-initialize (&optional error)
- "Initialize x-symbol support for Proof General, if possible.
-If ERROR is non-nil, give error on failure, otherwise a warning."
- (interactive)
- (unless (or proof-x-symbol-initialized ; already done
- (not proof-assistant-symbol) ; too early
- (not (proof-x-symbol-support-maybe-available)))
- (let*
- ((xs-lang (proof-ass x-symbol-language))
- (xs-lang-name (symbol-name xs-lang))
- (xs-feature (concat "x-symbol-" xs-lang-name))
- (xs-feature-sym (intern xs-feature))
- (error-or-warn
- (lambda (str)
- (progn
- (if error (error str) (warn str))))))
- ;; Check that support is provided.
- (cond
- ;; First, some checks on x-symbol.
- ((and (not (featurep 'x-symbol))
- (not (proof-try-require 'x-symbol)))
- (funcall error-or-warn
- "Proof General: x-symbol package must be installed for x-symbol-support!
-The package is available at http://x-symbol.sourceforge.net/"))
- ((not window-system)
- (funcall error-or-warn
- "Proof General: x-symbol package only runs under a window system!"))
- ((or (not (fboundp 'x-symbol-initialize))
- (not (fboundp 'x-symbol-register-language)))
- (funcall error-or-warn
- "Proof General: x-symbol package installation faulty!"))
- ;;
- ;; Now check proof assistant has support provided
- ;;
- ;; FIXME: maybe we should let x-symbol load the feature, in
- ;; case it uses x-symbol stuff inside?
- ;; NB: however, we're going to assume two files (thanks
- ;; to Isabelle: the standard x-symbol-<foo>.el, and one
- ;; named after the language feature).
- ((not (proof-try-require (intern (proof-x-symbol-tokenlang-file))))
- (funcall error-or-warn
- (format
- "Proof General: for x-symbol support, you must provide a library %s.el"
- xs-feature)))
- (t
- ;; We've got everything we need! So initialize.
- (require 'x-symbol-vars) ;; [new requirement to require this]
- (let*
- ((xs-xtra-modes proof-xsym-extra-modes)
- (xs-std-modes (list
- proof-mode-for-shell
- proof-mode-for-response
- proof-mode-for-script
- proof-mode-for-goals))
- (all-xs-modes (append xs-std-modes xs-xtra-modes))
- (am-entry (list proof-xsym-extra-modes t
- `(quote ,xs-lang)))
- (symmode-nm (concat xs-lang-name "sym-mode"))
- (symmode (intern symmode-nm))
- (symnamevar (intern (concat xs-feature "-name")))
- (symname (concat (capitalize xs-lang-name) " Symbols"))
- (symmodelinevar (intern (concat xs-feature "-modeline-name")))
- (symmodelinenm xs-lang-name)
- (flks proof-xsym-font-lock-keywords))
-
-
- (x-symbol-initialize) ;; No harm in doing this multiple times
- ;; Set default name and modeline indicator for the symbol
- ;; minor mode
- (set symnamevar symname)
- (set symmodelinevar symmodelinenm)
- (x-symbol-register-language xs-lang xs-feature-sym all-xs-modes)
- ;; FIXME: Need for Isabelle sup/sub scripts presently; loads
- ;; too early and extends in modedef setups. Adjust here.
- (if flks
- (put symmode 'font-lock-defaults (list flks)))
- ;;
- ;; Finished.
- (setq proof-x-symbol-initialized t)))))))
-
-
-
-;;;###autoload
-(defun proof-x-symbol-enable ()
- "Turn on or off X-Symbol in current Proof General script buffer.
-This invokes `x-symbol-mode' to change the setting for the current
-buffer. "
- (when (proof-ass x-symbol-enable)
- (unless proof-x-symbol-initialized ;; Check inited
- (set (proof-ass-sym x-symbol-enable) nil) ; assume failure!
- (proof-x-symbol-initialize 'giveerrors)
- (set (proof-ass-sym x-symbol-enable) t)))
-
- (when (and proof-x-symbol-initialized
- (fboundp 'x-symbol-mode))
- (x-symbol-mode (if (proof-ass x-symbol-enable) 1 0))
- (proof-x-symbol-mode-associated-buffers)))
-
-;; Old behaviour for proof-x-symbol-enable was to update state in all
-;; buffers --- but this can take ages if there are many buffers!
-;; Refreshing output buffers also causes glitches
-;; (proof-x-symbol-mode-all-buffers)
-;; (proof-x-symbol-refresh-output-buffers))
-
-
-(defun proof-x-symbol-refresh-output-buffers ()
- ;; NB: this isn't used. Might be nice to do so again, turning
- ;; off X-Sym can leave junk displayed. OTOH, sending messages to PA
- ;; can give errors, because there is no generic "refresh" or
- ;; "repeat" option. (Isar: gives errors outside proof mode).
- ;; Another possibility would just be to clear the display.
- "Clear the response buffer and send proof-showproof-command.
-This function is intended to clean the display after a change
-in the status of X-Symbol display.
-This is a subroutine of proof-x-symbol-enable."
- (pg-response-maybe-erase nil t t)
- (if (and proof-showproof-command (proof-shell-available-p))
- (proof-shell-invisible-command proof-showproof-command)))
-
-
-(defun proof-x-symbol-mode-associated-buffers ()
- "Activate/deactivate x-symbols in all Proof General associated buffers.
-A subroutine of proof-x-symbol-enable."
- (proof-map-buffers (list proof-goals-buffer
- proof-response-buffer
- proof-trace-buffer)
- (proof-x-symbol-config-output-buffer))
- (proof-with-current-buffer-if-exists proof-shell-buffer
- (proof-x-symbol-shell-config)))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Functions to decode output and encode input
-;;
-
-;;;###autoload
-(defun proof-x-symbol-decode-region (start end)
- (let ((newend (x-symbol-decode-region start end)))
- ;; subscripts in non-mule mode are done with fontification, see x-symbol-fontify
- (if (featurep 'mule)
- (let ((font-lock-keywords x-symbol-font-lock-keywords) ;; TODO: compile keywords
- (font-lock-defaults '(x-symbol-font-lock-keywords t))
- ;; GE 21.1: the `font-lock-set-defaults' flag prevents font lock
- ;; complaining (in font-lock-compile-keywords) that
- ;; we've not run font-lock-set-defaults. It gives dire
- ;; warnings what may happen otherwise but dynamic
- ;; binding of `font-lock-keywords' here should prevent
- ;; global changes to that variable.
- (font-lock-set-defaults t)
- (x-symbol-mode t)
- (x-symbol-subscripts t))
- (condition-case err
- (font-lock-fontify-keywords-region start newend nil)
- (t (proof-debug "Caught condition %s in `font-lock-fontify-keywords-region'"
- (car err))))))))
-
-
-(defun proof-x-symbol-encode-shell-input ()
- "Encode shell input in the variable STRING.
-A value for proof-shell-insert-hook."
- (and x-symbol-language
- (setq string
- (x-symbol-encode-string
- string (current-buffer)))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; There are three functions for configuring buffers:
-;;
-;; x-symbol-mode: script buffer (X-Symbol minor mode)
-;; proof-x-symbol-shell-config: shell buffer (input hook)
-;; proof-x-symbol-config-output-buffer: goals/response buffer (font lock)
-;;
-
-(defun proof-x-symbol-set-language ()
- "Set x-symbol-language for the current proof assistant."
- (setq x-symbol-language (proof-ass x-symbol-language)))
-
-;;;###autoload
-(defun proof-x-symbol-shell-config ()
- "Configure the proof shell for x-symbol, if proof-x-symbol-support<>nil.
-Assumes that the current buffer is the proof shell buffer."
- ;; The best strategy seems to be *not* to turn on decoding in the
- ;; shell itself. The reason is that there can be a clash between
- ;; annotations and X-Symbol characters which leads to funny effects
- ;; later. Moreover, the user isn't encouraged to interact directly
- ;; with the shell, so we don't need to be helpful there. So we keep
- ;; the shell buffer as plain text plus annotations. Even font-lock
- ;; is problematical, so it should be switched off too.
-
- ;; NB: after changing X-Symbols in output it would be nice to
- ;; refresh display, but there's no robust way of doing that yet
- ;; (see proof-x-symbol-refresh-output-buffers above)
- ;; [ The activate/decativate prover command itself could do it ]
- ;;
- (if proof-x-symbol-initialized
- (progn
- (cond
- ((proof-ass x-symbol-enable)
- (proof-x-symbol-set-language)
- (if (and proof-xsym-activate-command
- (proof-shell-live-buffer)
- ;; may fail if triggered during scripting.
- ;; Also: should cache status of x-symbol mode in
- ;; proof shell; current behaviour re-calls this
- ;; code every time a script file is loaded...
- (proof-shell-available-p))
- (proof-shell-invisible-command-invisible-result
- proof-xsym-activate-command))
- ;; We do encoding as the first step of input manipulation
- (add-hook 'proof-shell-insert-hook
- 'proof-x-symbol-encode-shell-input))
- ((not (proof-ass x-symbol-enable))
- (if (and proof-xsym-deactivate-command
- ;; NB: overlap with unicode tokens: don't disable that
- (not (proof-ass unicode-tokens-enable))
- (proof-shell-live-buffer))
- (proof-shell-invisible-command-invisible-result
- proof-xsym-deactivate-command))
- (remove-hook 'proof-shell-insert-hook
- 'proof-x-symbol-encode-shell-input)
- ;; NB: x-symbol automatically adds an output filter but
- ;; it doesn't actually get used unless the minor mode is
- ;; active. Removing it here is just tidying up.
- (remove-hook 'comint-output-filter-functions
- 'x-symbol-comint-output-filter))))))
-
-;;;###autoload
-(defun proof-x-symbol-config-output-buffer ()
- "Configure the current output buffer (goals/response/trace) for X-Symbol."
- (when (proof-ass x-symbol-enable)
- (proof-x-symbol-set-language)
- ;; BEGIN: Code below from x-symbol.el/x-symbol-mode-internal
- (unless (or (not (boundp 'enable-multibyte-characters))
- (not (fboundp 'set-buffer-multibyte))
- enable-multibyte-characters)
- ;; Emacs: we need to convert the buffer from unibyte to multibyte
- ;; since we'll use multibyte support for the symbol charset.
- ;; TODO: try to do it less often
- (let ((modified (buffer-modified-p))
- (inhibit-read-only t)
- (inhibit-modification-hooks t))
- (unwind-protect
- (progn
- (decode-coding-region (point-min) (point-max) 'undecided)
- (set-buffer-multibyte t))
- (set-buffer-modified-p modified))))
- ;; END code from x-symbol.el/x-symbol-mode-internal
-
- ;; If we're turning on x-symbol, attempt to convert current contents.
- ;; (reverse doesn't work so cleanly so we don't try it)
- (proof-x-symbol-decode-region (point-min) (point-max))))
-
-(provide 'proof-x-symbol)
-;; End of proof-x-symbol.el
diff --git a/generic/proof.el b/generic/proof.el
index 3db52db6..13ce9cb6 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -22,8 +22,7 @@
;;
;;; Code:
-(require 'proof-site) ; site/prover config, global vars
-(require 'proof-autoloads) ; autoloaded functions
+(require 'proof-site) ; site/prover config, global vars, autoloads
(require 'proof-compat) ; Emacs and OS compatibility
(require 'proof-utils) ; utilities
(require 'proof-config) ; configuration variables
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 16:54:26 +0000