Fix backward compatibility with Isabelle 2004.

2 files changed, 18 insertions, 14 deletions

diff --git a/generic/pg-pgip-old.el b/generic/pg-pgip-old.el
index ff7dc8e1..b4672ee0 100644
--- a/generic/pg-pgip-old.el
+++ b/generic/pg-pgip-old.el
@@ -20,22 +20,21 @@
 
 (defun pg-pgip-process-haspref (node)    ;; for Isabelle 2003
   "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-old-get-type attrs))
-       (defattr  (pg-pgip-get-attr "default" node t))
+      ((name     (pg-xml-get-text-content node))  ;; old PGIP: <haspref>name<haspref>
+       (type	 (pg-pgip-old-get-type node))
+       (defattr  (pg-xml-get-attr 'default node t))
        (default  (if defattr 
 		     (pg-pgip-old-interpret-value defattr type)
 		   (pg-pgip-old-default-for type)))
        (kind	 (intern
-		  (pg-pgip-get-attr "kind" node t "user"))
-       (descr    (pg-pgip-get-attr "descr" node t ""))
+		  (pg-xml-get-attr 'kind node t "user")))
+       (descr    (pg-xml-get-attr 'descr node t ""))
        (subst    (pg-pgip-subst-for type))
        (setting  
-	(pg-prover-interpret-pgip-command
-	 (concat "<pgip><setpref name=\"" name "\">" subst "</setpref></pgip>")))
-       (symname  (intern name))) ;; FIXME: consider Emacs ID normalising
+	(pg-pgip-string-of-command
+	 (concat "<setpref name=\"" name "\">" subst "</setpref>")))
+       (symname  (intern name)))
     (ignore-errors 
       ;; FIXME: allow rest of PGIP to be processed, would be better to
       ;; accumulate errors somehow.
@@ -47,7 +46,7 @@
 	  (concat descr (if descr "\n")
 	   "Setting configured by <haspref> PGIP message")
 	  :type (quote ,type)
-	  :setting ,setting))))))
+	  :setting ,setting)))))
     
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -132,7 +131,7 @@
 (defun pg-pgip-old-get-type (node)
   "Extract and check type value from NODE.  Return type in internal (custom) format."
   (let 
-      ((rawtype (pg-pgip-old-get-attr "type" node)))
+      ((rawtype (pg-xml-get-attr 'type node)))
     (pg-pgip-old-pgiptype rawtype)))
  
 
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index e46b4c33..b44bf7e1 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -39,13 +39,16 @@ The list PGIPS may contain one or more PGIP packets, whose contents are processe
 
 (defun pg-pgip-process-pgip (pgip)
   "Process the commands in the PGIP XML-node PGIP."
+  ;; FIXME: appearances of 'notreallyoptional below should be removed,
+  ;; but they are needed for compatibility with Isabelle 2004 whose
+  ;; PGIP messages are incomplete.
   (let* ((name	   (xml-node-name pgip))
 	 (origin   (pg-xml-get-attr 'origin pgip 'optional))
 	 (id	   (pg-xml-get-attr 'id pgip 'optional))
-	 (class	   (pg-xml-get-attr 'class pgip))
+	 (class	   (pg-xml-get-attr 'class pgip 'notreallyoptional))
 	 (refseq   (pg-xml-get-attr 'refseq pgip 'optional))
 	 (refid    (pg-xml-get-attr 'refid pgip 'optional))
-	 (seq	   (pg-xml-get-attr 'seq pgip)))
+	 (seq	   (pg-xml-get-attr 'seq pgip 'notreallyoptional)))
     (setq pg-pgip-last-seen-id id)
     (setq pg-pgip-last-seen-seq seq)
     (if (eq name 'pgip)
@@ -60,7 +63,8 @@ Return a symbol representing the PGIP command processed, or nil."
 	 (fname	      (intern (concat "pg-pgip-process-" (symbol-name name)))))
     (if (fboundp fname)
 	(progn
-	  (pg-pgip-debug "Processing PGIP message seq %s, type %s" (pg-xml-get-attr 'seq pgip) name)
+	  (pg-pgip-debug "Processing PGIP message seq %s, type %s" 
+			 (pg-xml-get-attr 'seq pgip 'notreallyoptional) name)
 	  (funcall fname pgipmsg)
 	  name)
       (pg-internal-warning "!!! unrecognized/unimplemented PGIP message element `%s'" name)
@@ -68,6 +72,7 @@ Return a symbol representing the PGIP command processed, or nil."
 
 (defvar pg-pgip-post-process-functions
   '((hasprefs . proof-assistant-menu-update)
+    (oldhaspref . proof-assistant-menu-update) ;; FIXME: for Isabelle2004 backward compat
     (menuadd  . proof-assistant-menu-update)
     (menudel  . proof-assistant-menu-update)
     (idtable  . pg-pgip-update-idtables)    ;; TODO: not yet implemented