From 61ea2d3ec09ab63ba14be0e8c8ef5889f53e0026 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 14 Nov 2002 00:46:46 +0000 Subject: Next iteration: add post-processing step, descriptions in haspref. --- generic/pg-pgip.el | 174 ++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 119 insertions(+), 55 deletions(-) (limited to 'generic/pg-pgip.el') 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 - ;; - ((eq elt 'pgip)) ;; ignore pgip attributes for now - ;; - ((eq elt 'usespgml) - (proof-debug "Received usespgml message, version %s" - (pg-pgip-get-version "usespgml" attrs))) - ;; - ((eq elt 'haspref) - (pg-pgip-haspref attrs (car-safe body))) - - ;; - ((eq elt 'prefval) - ) - ;; - ((eq elt 'idtable) - ) - ;; - ((eq elt 'addid) - ) - ;; - ((eq elt 'delid) - ) - ;; - ((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 + ;; + ((eq elt 'pgip)) ;; ignore pgip attributes for now + ;; + ((eq elt 'usespgml) + (proof-debug "Received usespgml message, version %s" + (pg-pgip-get-version "usespgml" attrs))) + ;; + ((eq elt 'haspref) + (pg-pgip-haspref attrs (car-safe body))) + + ;; + ((eq elt 'prefval) + ) + ;; + ((eq elt 'idtable) + ) + ;; + ((eq elt 'addid) + ) + ;; + ((eq elt 'delid) + ) + ;; + ((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 + ))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; name +;; + (defun pg-pgip-haspref (attrs name) "Issue a defpacustom from a element with attributes ATTRS, name NAME." (unless (stringp name) (pg-pgip-error "pg-pgip-haspref: missing NAME in NAME.")) (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 "" subst "")) + (pg-prover-interpret-pgip-command + (concat "" subst ""))) (symname (intern name))) ;; FIXME: consider Emacs ID normalising - (eval - `(defpacustom ,symname ,default - ;; FIXME: better docstring - "Setting configured by 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 PGIP message") + :type (quote ,type) + :setting ,setting))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Dealing with +;; + (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) -- cgit v1.2.3