Debuggin pg-pgip-haspref.

1 files changed, 37 insertions, 22 deletions

diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index b35941c6..a75200f2 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -6,30 +6,38 @@
 ;;
 ;; $Id$
 ;;
-;; STATUS: Experimental, not in use.
+;; STATUS: Experimental
 ;;
 ;; Proof General Kit uses PGIP, an XML-message protocol
 ;; for interactive proof.  This file contains functions 
 ;; to process PGIP commands sent from the proof assistant.
 ;;
 
+;; Halt on errors during development: later may accumulate and ignore.
+(defalias 'pg-pgip-error 'error)	
+
 ;;;###autoload
-(defun pg-pgip-process-cmd (pgip) 
+(defun pg-pgip-process-cmd (pgips) 
   "Process the command in PGIP, which should be parsed XML according to pg-xml-parse-*."
-  (while (pgip)
-    (let ((elt   (caar  pgip))
-	  (attrs (cdar  pgip)))
+  (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)
-	(message "Received usespgml message, version %s"
-		 (pg-pgip-get-version "usespgml" attrs)))
+	(proof-debug "Received usespgml message, version %s"
+		     (pg-pgip-get-version "usespgml" attrs)))
        ;; <haspref>
        ((eq elt 'haspref)
-	(pg-pgip-haspref attrs) ;; (cadr pgip))
-	(setq pgip (cdr pgip)))
+	(pg-pgip-haspref attrs (car-safe body)))
+
        ;; <prefval>
        ((eq elt 'prefval)
 	)
@@ -48,10 +56,14 @@
        ((eq elt 'menudel)
 	))
       ;; Move on to next element
-      (setq pgip (cdr pgip)))))
+      (setq pgips (cdr pgips)))))
+
 
-(defun pg-pgip-haspref (attrs)
-  "Issue a defpacustom from a <haspref> element with attributes ATTRS"
+;; test: (pg-pgip-haspref '((type . "boolean") (kind . "user")) "verbose_flag")
+(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)
@@ -62,15 +74,17 @@
 		   (pg-pgip-get-attr "haspref" "kind" attrs t)
 		   ;; Default to kind user
 		   "user")))
-       (name     (intern (pg-pgip-get-attr "haspref" "name")))
        (subst    (pg-pgip-subst-for type))
-       (setting  (concat "<pgip><setpref name=\"" name "\">" subst "</setpref></pgip>")))
+       (setting  
+	;; FIXME: deal with provers that don't understand PGIP here.
+	(concat "<pgip><setpref name=\"" name "\">" subst "</setpref></pgip>"))
+       (symname  (intern name))) ;; FIXME: consider Emacs ID normalising
     (eval
-     (list 'defpacustom name default 
-	   ;; FIXME: better docstring
-	   "Setting configured by <haspref> PGIP message"
-	   :type type
-	   :setting setting))))
+     `(defpacustom ,symname ,default 
+	;; FIXME: better docstring
+	"Setting configured by <haspref> PGIP message"
+	:type (quote ,type)
+	:setting ,setting))))
     
 (defun pg-pgip-default-for (type)
   "Synthesize a default value for type TYPE."
@@ -81,7 +95,7 @@
    ((eq (car-safe type) 'choice)
 	(car-safe (cdr-safe type)))
    (t
-    (error "pg-pgip-default-for: unrecognized type passed in"))))
+    (pg-pgip-error "pg-pgip-default-for: unrecognized type passed in"))))
 
 (defun pg-pgip-subst-for (type)
   "Return a substitution string for type TYPE."
@@ -92,7 +106,8 @@
 
 (defun pg-pgip-get-type (attrs)
   "Extract and check type value from ATTRS.  Normalize to custom format."
-  (let ((rawtype (pg-pgip-get-attr "haspref" "type" attrs)))
+  (let 
+      ((rawtype (pg-pgip-get-attr "haspref" 'type attrs)))
     (cond
      ((string-match "choice(\\(.*\\))" rawtype)
       (let* ((choiceslist (match-string 1 rawtype))
@@ -113,7 +128,7 @@
 ;; Auxiliary functions for parsing
 
 (defun pg-pgip-get-attr (elt attrnm attrs &optional optional)
-  (let ((vrs (assoc attrnm attrs)))
+  (let ((vrs (cdr-safe (assoc attrnm attrs))))
     (if optional
 	vrs
       (or vrs