Next iteration: add post-processing step, descriptions in haspref.

1 files changed, 119 insertions, 55 deletions

diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index a75200f2..42060e13 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -14,78 +14,129 @@
 ;;
 
 ;; Halt on errors during development: later may accumulate and ignore.
-(defalias 'pg-pgip-error 'error)	
+(defalias 'pg-pgip-error 'error)
 
 ;;;###autoload
-(defun pg-pgip-process-cmd (pgips) 
-  "Process the command in PGIP, which should be parsed XML according to pg-xml-parse-*."
-  (while pgips
-    (let* ((pgip  (car pgips))
-	   (elt   (or (car-safe (car pgip))         ; normalise to symbol
-		      (car pgip)))
-	   (attr  (cdr-safe (car pgip)))
-	   (attrs (and attr (if (listp (cdr attr)) ; normalise to list
-				attr (list attr))))
-	   (body  (cdr pgip)))
-      (cond 
-       ;; <pgip> 
-       ((eq elt 'pgip))			;; ignore pgip attributes for now
-       ;; <usespgml>
-       ((eq elt 'usespgml)
-	(proof-debug "Received usespgml message, version %s"
-		     (pg-pgip-get-version "usespgml" attrs)))
-       ;; <haspref>
-       ((eq elt 'haspref)
-	(pg-pgip-haspref attrs (car-safe body)))
-
-       ;; <prefval>
-       ((eq elt 'prefval)
-	)
-       ;; <idtable>
-       ((eq elt 'idtable)
-	)
-       ;; <addid>
-       ((eq elt 'addid)
-	)
-       ;; <delid>
-       ((eq elt 'delid)
-	)
-       ;; <menuadd>
-       ((eq elt 'menuadd)
-	)
-       ((eq elt 'menudel)
-	))
-      ;; Move on to next element
-      (setq pgips (cdr pgips)))))
-
-
-;; test: (pg-pgip-haspref '((type . "boolean") (kind . "user")) "verbose_flag")
+(defun pg-pgip-process-packet (pgip)
+  "Process the command packet PGIP, which is parsed XML according to pg-xml-parse-*"
+  ;; PGIP processing is split into two steps:
+  ;; (1) process each command, altering internal data structures
+  ;; (2) post-process for each command type, affecting external interface (menus, etc).
+  (mapcar 'pg-pgip-post-process 
+	  (pg-pgip-process-cmds pgip)))
+
+(defun pg-pgip-process-cmds (pgips)
+  "Process the command(s) in PGIP, returning list of command symbols processed."
+  (let (cmdtys)
+    (while pgips
+      (let* ((pgip  (car pgips))
+	     (elt   (or (car-safe (car pgip))         ; normalise to symbol
+			(car pgip)))
+	     (attr  (cdr-safe (car pgip)))
+	     (attrs (and attr (if (listp (cdr attr)) ; normalise to list
+				  attr (list attr))))
+	     (body  (cdr pgip)))
+	(add-to-list 'cmdtys elt)
+	(cond 
+	 ;; <pgip> 
+	 ((eq elt 'pgip))			;; ignore pgip attributes for now
+	 ;; <usespgml>
+	 ((eq elt 'usespgml)
+	  (proof-debug "Received usespgml message, version %s"
+		       (pg-pgip-get-version "usespgml" attrs)))
+	 ;; <haspref>
+	 ((eq elt 'haspref)
+	  (pg-pgip-haspref attrs (car-safe body)))
+	 
+	 ;; <prefval>
+	 ((eq elt 'prefval)
+	  )
+	 ;; <idtable>
+	 ((eq elt 'idtable)
+	  )
+	 ;; <addid>
+	 ((eq elt 'addid)
+	  )
+	 ;; <delid>
+	 ((eq elt 'delid)
+	  )
+	 ;; <menuadd>
+	 ((eq elt 'menuadd)
+	  )
+	 ((eq elt 'menudel)
+	  ))
+	;; Move on to next element
+	(setq pgips (cdr pgips))))
+    ;; Return list  of command types processed.
+    cmdtys))
+
+(defun pg-pgip-post-process (pgip)
+  "Perform post-processing for a PGIP command type PGIP-ELT."
+  (cond
+   ((eq pgip 'pgip))
+   ((eq pgip 'usespgml))
+   ((or
+     (eq pgip 'haspref)
+     (eq pgip 'prefval))
+    ;; Update preferences view/menu
+    (proof-assistant-menu-update))
+   ((or
+     (eq pgip 'idtable)
+     (eq pgip 'addid)
+     (eq pgip 'delid))
+    ;; Update completion tables/view
+    )
+   ((or
+     (eq pgip 'menuadd)
+     (eq pgip 'menudel))
+    ;; Update menus
+    )))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; <haspref default="d" kind="k" description="d" class="c">name</haspref>
+;; 
+
 (defun pg-pgip-haspref (attrs name)
   "Issue a defpacustom from a <haspref> element with attributes ATTRS, name NAME."
   (unless (stringp name)
     (pg-pgip-error "pg-pgip-haspref: missing NAME in <haspref>NAME</haspref>."))
   (let*
       ((type	 (pg-pgip-get-type attrs))
-       (default  (or (pg-pgip-get-attr "haspref" "default" attrs t)
-		     ;; If no default is supplied, make one
+       (default  (or (pg-pgip-get-attr "haspref" 'default attrs t)
+		     ;; If no default is supplied, make one 
+		        ;; [NB: boolean default is nil anyway]
 		     (pg-pgip-default-for type)))
        (kind	 (intern
 		  (or 
-		   (pg-pgip-get-attr "haspref" "kind" attrs t)
+		   (pg-pgip-get-attr "haspref" 'kind attrs t)
 		   ;; Default to kind user
 		   "user")))
+       (descr    (or (pg-pgip-get-attr "haspref" 'descr attrs t) ""))
        (subst    (pg-pgip-subst-for type))
        (setting  
-	;; FIXME: deal with provers that don't understand PGIP here.
-	(concat "<pgip><setpref name=\"" name "\">" subst "</setpref></pgip>"))
+	(pg-prover-interpret-pgip-command
+	 (concat "<pgip><setpref name=\"" name "\">" subst "</setpref></pgip>")))
        (symname  (intern name))) ;; FIXME: consider Emacs ID normalising
-    (eval
-     `(defpacustom ,symname ,default 
-	;; FIXME: better docstring
-	"Setting configured by <haspref> PGIP message"
-	:type (quote ,type)
-	:setting ,setting))))
+    (ignore-errors 
+      ;; FIXME: allow rest of PGIP to be processed, would be better to
+      ;; accumulate errors somehow.
+      (proof-debug "haspref calling defpacustom: name:%s default:%s type:%s setting:%s" symname default type setting)
+      (eval
+       `(defpacustom ,symname ,default 
+	  (concat descr (if descr "\n")
+	   "Setting configured by <haspref> PGIP message")
+	  :type (quote ,type)
+	  :setting ,setting)))))
     
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Dealing with <pgiptype>
+;; 
+
 (defun pg-pgip-default-for (type)
   "Synthesize a default value for type TYPE."
   (cond
@@ -125,7 +176,10 @@
       (error "pg-pgip-get-type: unrecognized type %s" rawtype)))))
     
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
 ;; Auxiliary functions for parsing
+;;
 
 (defun pg-pgip-get-attr (elt attrnm attrs &optional optional)
   (let ((vrs (cdr-safe (assoc attrnm attrs))))
@@ -138,6 +192,16 @@
   (pg-pgip-get-attr elt "version" attrs optional))
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Function to interface PGIP commands sent to prover.
+;;
+(defun pg-prover-interpret-pgip-command (pgip)
+  (if proof-shell-issue-pgip-cmd
+      (format proof-shell-issue-pgip-cmd pgip)
+    "")) ;; Empty setting: might be better to send a comment
+         ;; for debugging purposes.
+
 
 
 (provide 'pg-pgip)