From cdd22a2c2f4c5c5f52124f3e4ef8a51d447646c2 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sat, 5 Jan 2008 11:50:31 +0000 Subject: Deleted file --- generic/pg-pgip-old.el | 161 ------------------------------------------------- 1 file changed, 161 deletions(-) delete mode 100644 generic/pg-pgip-old.el (limited to 'generic') diff --git a/generic/pg-pgip-old.el b/generic/pg-pgip-old.el deleted file mode 100644 index 49287b7e..00000000 --- a/generic/pg-pgip-old.el +++ /dev/null @@ -1,161 +0,0 @@ -;; 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 -;; -;; name - -(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 element with attributes ATTRS, name NAME." - (let* - ((name (pg-xml-get-text-content node)) ;; old PGIP: name - (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-xml-get-attr 'kind node t "user"))) - (descr (pg-xml-get-attr 'descr node t "")) - (subst (pg-pgip-subst-for type)) - (setting - (pg-pgip-string-of-command - (concat "" subst ""))) - (symname (intern name))) - (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 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-number returns zero for non int string, - ;; should have better validation here. - (string-to-number 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 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-xml-get-attr 'type node))) - (pg-pgip-old-pgiptype rawtype))) - - -(defun pg-pgip-old-pgiptype (rawtype) - "Return internal (custom format) representation for 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' -- cgit v1.2.3