diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2002-08-08 21:49:20 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-08 21:49:20 +0000 |
commit | f3c331b28eb79a08131df723444eb0ebfc7452c2 (patch) | |
tree | 5bde7a535ba062f56c8445ed49e5c82c8e6e2112 | |
parent | 04b55ba97d2942875e888fe72af713cce6568fb2 (diff) |
Generalise proof elements to include comments, show/hiding of comments.
-rw-r--r-- | generic/pg-user.el | 24 | ||||
-rw-r--r-- | generic/proof-config.el | 2 | ||||
-rw-r--r-- | generic/proof-menu.el | 11 | ||||
-rw-r--r-- | generic/proof-script.el | 85 | ||||
-rw-r--r-- | generic/proof-toolbar.el | 12 |
5 files changed, 84 insertions, 50 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index 26859c5b..6055ff3a 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -883,21 +883,22 @@ If NUM is negative, move upwards. Return new span." ;; Find controlling span (while (setq cspan (span-property span 'controlspan)) (setq span cspan)) - (let* - ((idiom (span-property span 'idiom)) - (idiomnm (if idiom (symbol-name idiom))) - (portname (span-property span 'name))) - (popup-menu (pg-create-in-span-context-menu span idiomnm portname))))) + (let* + ((idiom (and span (span-property span 'idiom))) + (id (and span (span-property span 'id)))) + (popup-menu (pg-create-in-span-context-menu + span + (if idiom (symbol-name idiom)) + (if id (symbol-name id))))))) (defun pg-toggle-visibility () "Toggle visibility of region under point." (interactive) (let* ((span (span-at (point) 'type)) - (idiom (and span (span-property span 'idiom))) - (idiomnm (and idiom (symbol-name idiom))) - (portname (and span (span-property span 'name)))) - (and portname idiomnm - (pg-toggle-element-visibility idiomnm portname)))) + (idiom (and span (span-property span 'idiom))) + (id (and span (span-property span 'id)))) + (and idiom id + (pg-toggle-element-visibility (symbol-name idiom) (symbol-name id))))) (defun pg-create-in-span-context-menu (span idiom name) @@ -911,7 +912,8 @@ If NUM is negative, move upwards. Return new span." (list (pg-span-name span)) (list (vector "Show/hide" - (if idiom (list 'pg-toggle-element-visibility idiom name) idiom) + (if idiom (list `pg-toggle-element-visibility idiom name) + idiom) (not (not idiom)))) (list (vector "Copy" (list 'pg-copy-span-contents span) t)) diff --git a/generic/proof-config.el b/generic/proof-config.el index f88ac91c..9e85b866 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -722,8 +722,6 @@ If a function, it should return the command string to insert." proof-find-theorems-command) (command "Issue Command" "Issue a non-scripting command" t) (interrupt "Interrupt Prover" "Interrupt the proof assistant (warning: may break synchronization)" t) - (show "Show Proofs" nil t) - (hide "Hide Proofs" nil t) (info nil "Show online proof assistant information" t proof-info-command) (help nil "Proof General manual" t)) diff --git a/generic/proof-menu.el b/generic/proof-menu.el index de74e24b..763d4e89 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -165,6 +165,15 @@ If in three window or multiple frame mode, display both buffers." ["Send Bug Report" proof-submit-bug-report t]) "Proof General help menu.") +(defvar proof-show-hide-menu + '(("Show all" + ["Proofs" (pg-show-all-portions "proof") t] + ["Comments" (pg-show-all-portions "comment") t]) + ("Hide all" + ["Proofs" (pg-show-all-portions "proof" 'hide) t] + ["Comments" (pg-show-all-portions "comment" 'hide) t])) + "Show/hide submenu.") + (defvar proof-buffer-menu (cons "Buffers" (append @@ -194,6 +203,7 @@ If in three window or multiple frame mode, display both buffers." :active (buffer-live-p proof-trace-buffer)]))) "Proof General buffer menu.") + ;; Make the togglers used in options menu below (proof-deftoggle proof-three-window-mode) @@ -308,6 +318,7 @@ If in three window or multiple frame mode, display both buffers." (cons proof-general-name (append proof-toolbar-scripting-menu + proof-show-hide-menu proof-menu proof-config-menu (list proof-help-menu))) diff --git a/generic/proof-script.el b/generic/proof-script.el index 75381b38..d4465299 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -44,6 +44,10 @@ Zero means outside a proof, 1 means inside a top-level proof, etc. This variable is maintained in proof-done-advancing; it is zeroed in proof-shell-clear-state.") +(defvar proof-element-counters nil + "Table of (name . count) pairs, counting elements in scripting buffer.") + + ;; Buffer-local variables (deflocal proof-active-buffer-fake-minor-mode nil @@ -60,6 +64,30 @@ kill buffer hook. This variable is used when buffer-file-name is nil.") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;; Counting and naming proof elements +;; + +(defun proof-next-element-count (idiom) + "Return count for next element of type IDIOM. +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))) + next)) + +(defun proof-element-id (idiom number) + "Return a string identifier composed from symbol IDIOM and NUMBER." + (concat (symbol-name idiom) "-" (int-to-string number))) + +(defun proof-next-element-id (idiom) + (proof-element-id idiom (proof-next-element-count idiom))) + + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; Configuration of function-menu (aka "fume") ;; ;; FIXME: we would like this code only enabled if the user loads @@ -254,6 +282,7 @@ Also clear list of script portions." (set-span-property proof-locked-span 'face 'proof-locked-face) (detach-span proof-locked-span) (setq proof-last-theorem-dependencies nil) + (setq proof-element-counters nil) (pg-clear-script-portions)) @@ -485,7 +514,7 @@ IDIOM, ID, and optional NAME are all strings. Identifiers must be unique for a given idiom; the optional NAME will be recorded as a textual name used instead of ID for users; NAME does not need to be unique." - (let* ((idiomsym (intern idiom)) + (let* ((idiomsym (intern idiom)) (idsym (intern id)) (name (or name id)) (visname (pg-visname idiom id)) @@ -518,7 +547,7 @@ NAME does not need to be unique." (and idiom id (if invisible (pg-make-element-invisible - (symbol-name idiom) (symbol-name id)) + (symbol-name idiom) id) (pg-make-element-visible (symbol-name idiom) (symbol-name id)))))) @@ -557,40 +586,36 @@ NAME does not need to be unique." (symbol-name arg))) (lambda (arg) (pg-make-element-visible idiom (symbol-name arg)))))) - (mapcar alterfn elts))) - -(defun pg-show-all-proofs () - "Display all completed proofs in the buffer." - (interactive) - (pg-show-all-portions "proof") + (mapcar alterfn elts)) (unless proof-running-on-XEmacs ;; GNU Emacs requires redisplay here to see result ;; (sit-for 0) not enough (redraw-frame (selected-frame)))) - + +(defun pg-show-all-proofs () + "Display all completed proofs in the buffer." + (interactive) + (pg-show-all-portions "proof")) (defun pg-hide-all-proofs () "Hide all completed proofs in the buffer." (interactive) - (pg-show-all-portions "proof" 'hide) - (unless proof-running-on-XEmacs - ;; GNU Emacs requires redisplay here to see result - ;; (sit-for 0) not enough - (redraw-frame (selected-frame)))) + (pg-show-all-portions "proof" 'hide)) (defun pg-add-proof-element (name span controlspan) "Add a nested span proof element." - ;; FIXME: make unique ID here. - (pg-add-element "proof" name span) - ;; Make a navigable link between the two spans. - (set-span-property span 'controlspan controlspan) - (set-span-property controlspan 'children - (cons span (span-property controlspan 'children))) - ;; (set-span-property span 'context-menu (pg-proof-element-menu name)) - (pg-set-span-helphighlights span 'nohighlight) - (if proof-disappearing-proofs - (pg-make-element-invisible "proof" name))) + (let ((proofid (proof-next-element-id 'proof))) + (pg-add-element "proof" proofid span name) + ;; Set id in controlspan + (set-span-property controlspan 'id (intern proofid)) + ;; Make a navigable link between the two spans. + (set-span-property span 'controlspan controlspan) + (set-span-property controlspan 'children + (cons span (span-property controlspan 'children))) + (pg-set-span-helphighlights span 'nohighlight) + (if proof-disappearing-proofs + (pg-make-element-invisible "proof" name)))) (defun pg-span-name (span) "Return a user-level name for SPAN." @@ -1209,9 +1234,19 @@ With ARG, turn on scripting iff ARG is positive." (proof-set-queue-start end)) (setq cmd (span-property span 'cmd)) (cond + ;; CASE 1: Comments just get highlighted ((eq (span-property span 'type) 'comment) - (pg-set-span-helphighlights span)) + (pg-set-span-helphighlights span) + ;; Add an element for a new span, which should span + ;; the text of the comment. + (let ((bodyspan (make-span + (+ (length comment-start) (span-start span)) + (- (span-end span) (length comment-end)))) + (id (proof-next-element-id 'comment))) + (pg-add-element "comment" id bodyspan) + (set-span-property span 'id (intern id)) + (set-span-property span 'idiom 'comment))) ;; CASE 2: Save command seen, now we may amalgamate spans. ((and proof-save-command-regexp diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index 406d42a1..83e895a9 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -528,18 +528,6 @@ changed state." (defalias 'proof-toolbar-find 'proof-find-theorems) ;; -;; Show and hide buttons (not on toolbar) -;; - -(defun proof-toolbar-show-enable-p () t) -(defalias 'proof-toolbar-show 'pg-show-all-proofs) - -(defun proof-toolbar-hide-enable-p () t) -(defalias 'proof-toolbar-hide 'pg-hide-all-proofs) - - - -;; ;; Interrupt button ;; |