Generalise proof elements to include comments, show/hiding of comments.

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
 ;;