New files.

1 files changed, 162 insertions, 0 deletions

diff --git a/generic/pg-pgip-old.el b/generic/pg-pgip-old.el
new file mode 100644
index 00000000..ff7dc8e1
--- /dev/null
+++ b/generic/pg-pgip-old.el
@@ -0,0 +1,162 @@
+;; pg-pgip-old.el	 Functions for processing PGIP for Proof General
+;;
+;; This file contains some backwards compatiblity functions for
+;; dealing with PGIP 1.X messages.  The only case that these are
+;; needed is for interim backward compatibility with Isabelle2003 and
+;; Isabelle2004, for processing preference settings.
+;;
+
+;; FIXME: resurrect pg-prover-interpret-pgip-command (could try with pg-pgip-string-of-command)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; 
+;; Message processing: BACKWARD COMPATIBILITY
+;;
+;; <haspref default="d" kind="k" type="t"
+;;	    description="d" class="c">name</haspref>
+
+(defun pg-pgip-process-oldhaspref (node) ;; for Isabelle 2004
+  (pg-pgip-process-haspref node))
+
+(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))
+       (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 ""))
+       (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
+    (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
+       ;; FIXME: would like unique custom group for settings introduced by haspref.
+       ;; (preferences or something).
+       `(defpacustom ,symname ,default 
+	  (concat descr (if descr "\n")
+	   "Setting configured by <haspref> PGIP message")
+	  :type (quote ,type)
+	  :setting ,setting))))))
+    
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Interpretation of types in old format
+;;
+
+(defun pg-pgip-old-interpret-bool (value)
+  (cond 
+   ((string-equal value "true") t)
+   ((string-equal value "false") nil)
+   ;; Non-boolean value: return false, give debug message.
+   (t (progn
+	(proof-debug "pg-pgip-old-interpret-bool: received non-bool value %s" value)
+	nil))))
+
+(defun pg-pgip-old-interpret-int (value)
+  ;; FIXME: string-to-int returns zero for non int string,
+  ;; should have better validation here.
+  (string-to-int value))
+
+(defun pg-pgip-old-interpret-string (value)
+  value)
+
+(defun pg-pgip-old-interpret-choice (choices value)
+  ;; Untagged union types: test for each type in turn.
+  ;; FIXME: nested unions not supported here.
+  (cond
+   ((and 
+     (memq 'boolean choices)
+     (or (string-equal value "true") (string-equal value "false")))
+    (pg-pgip-old-interpret-value value 'boolean))
+   ((and 
+     (memq 'integer choices)
+     (string-match "[0-9]+$" value))
+    (pg-pgip-old-interpret-value value 'integer))
+   ((memq 'string choices)
+    ;; FIXME: No special syntax for string inside PGIP yet, should be?
+    (pg-pgip-old-interpret-value value 'string))
+   (t
+    (pg-pgip-old-error 
+     "pg-pgip-old-interpret-choice: mismatching value %s for choices %s" 
+     value choices))))
+
+(defun pg-pgip-old-interpret-value (value type)
+  (cond
+   ((eq type 'boolean)
+    (pg-pgip-old-interpret-bool value))
+   ((eq type 'integer)
+    (pg-pgip-old-interpret-int value))
+   ((eq type 'string)
+    (pg-pgip-old-interpret-string value))
+   ((and (consp type) (eq (car type) 'choice))
+    (pg-pgip-old-interpret-choice (cdr type) value))
+   (t
+    (pg-pgip-old-error "pg-pgip-old-interpret-value: unkown type %s" type))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Dealing with <pgiptype> in old format
+;; 
+
+(defun pg-pgip-old-default-for (type)
+  "Synthesize a default value for type TYPE."
+  (cond
+   ((eq type 'boolean) nil)
+   ((eq type 'integer) 0)
+   ((eq type 'string)  "")
+   ((eq (car-safe type) 'choice)
+	(car-safe (cdr-safe type)))
+   (t
+    (pg-pgip-old-error "pg-pgip-old-default-for: unrecognized type passed in"))))
+
+(defun pg-pgip-old-subst-for (type)
+  "Return a substitution string for type TYPE."
+  (cond
+   ((eq type 'boolean) "%b")
+   ((eq type 'integer) "%i")
+   (t "%s")))
+
+(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)))
+    (pg-pgip-old-pgiptype rawtype)))
+ 
+
+(defun pg-pgip-old-pgiptype (rawtype)
+  "Return internal (custom format) representation for <pgiptype> element."
+    (cond
+     ((string-match "choice\(\\(.*\\)\)" rawtype)
+      (let* ((choiceslist (match-string 1 rawtype))
+	     ;; FIXME: nested choices not supported yet
+	     (choices	  (split-string choiceslist "[ \f\t\n\r\v]*,[ \f\t\n\r\v]*")))
+	(list 'choice (mapcar 'pg-pgip-old-pgiptype choices))))
+     ((equal rawtype "boolean")
+      'boolean)
+     ((equal rawtype "int")
+      'integer)
+     ((equal rawtype "nat")		;; nat treated as int 
+      'integer)
+     ((equal rawtype "string")
+      'string)
+     (t
+      (error "pg-pgip-old-pgiptype: unrecognized type %s" rawtype))))
+
+
+
+
+(provide 'pg-pgip-old)
+;; End of `pg-pgip-old.el'