Generalise context menu for other spans; grey out show/hide when unavailable.

1 files changed, 14 insertions, 5 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 158ce9c8..acf74e54 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -712,15 +712,24 @@ last use time, to discourage saving these into the users database."
     (while (setq cspan (span-property span 'controlspan))
       (setq span cspan))
     (let* 
-      ((idiom      (symbol-name (span-property span 'idiom)))
-       (portname   (span-property span 'name)))
-    (popup-menu (pg-create-in-span-context-menu span idiom portname)))))
+	((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)))))
 
 (defun pg-create-in-span-context-menu (span idiom name)
+  "Create the dynamic context-sensitive menu for a span."
+  ;; FIXME: performance here, consider caching in the span itself?
+  ;; (or maybe larger menu spans which are associated with a menu).
+  ;; FIXME: treat proof and non-proof regions alike, could add
+  ;; visibility controls for non-proof regions also, redesigning
+  ;; idiom notion.
   (append
-   (list (concat (if idiom (upcase-initials idiom)) (if name (concat ": " name))))
+   (list (pg-span-name span))
    (list (vector
-	  "Show/hide"   (list 'pg-toggle-element-visibility idiom name) idiom))
+	  "Show/hide"   
+	  (if idiom (list 'pg-toggle-element-visibility idiom name) idiom)
+	  (not (not idiom))))
    (list (vector
 	  "Copy"	(list 'pg-copy-span-contents span) t))
    (if (featurep 'proof-depends)