diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-08-26 10:34:27 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-08-26 10:34:27 +0000 |
| commit | 69acb64240643aed9784a2602004652da5737a9d (patch) | |
| tree | ae92a1ea36dbdba9aa5a30e783ad72c19c876aa3 /generic/pg-pgip.el | |
| parent | 05acfead84ac70b6e5162f3fa669129016fe4070 (diff) | |
Fixes for idtables
Diffstat (limited to 'generic/pg-pgip.el')
| -rw-r--r-- | generic/pg-pgip.el | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index c8ee6523..e46b4c33 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -199,6 +199,9 @@ Return a symbol representing the PGIP command processed, or nil." ;; Identifiers: managing obarrays of symbols used for completion ;; +(defvar proof-assistant-idtables nil + "List of idtables (objtype symbols) for currently running proof assistant.") + (defun pg-pgip-process-ids (node) "Manipulate identifier tables, according to setids/addids/delids in NODE." (let ((idtables (pg-xml-child-elts node)) @@ -211,7 +214,11 @@ Return a symbol representing the PGIP command processed, or nil." (obarray (or (and (not (eq opn 'setids)) (get objtype 'pgsymbols)) ;; new empty obarray for setids or if unset - (set objtype 'pg-symbols (make-vector 31 0))))) + (put objtype 'pg-symbols (make-vector 31 0))))) + (setq proof-assistant-idtables + (if (and (null idents) (eq opn 'setids)) + (delete objtype proof-assistant-idtables) + (adjoin objtype proof-assistant-idtables))) (cond ((or (eq opn 'setids) (eq opn 'addids)) (mapcar (lambda (i) (intern i obarray)) idents)) @@ -221,6 +228,11 @@ Return a symbol representing the PGIP command processed, or nil." (pg-pgip-error "pg-pgip-process-ids: called on wrong node %s" (xml-node-name node)))))))) +(defun pg-complete-idtable-symbol () + (interactive) + ;; TODO: complete based on blah + ) + (defalias 'pg-pgip-process-setids 'pg-pgip-process-ids) (defalias 'pg-pgip-process-addids 'pg-pgip-process-ids) (defalias 'pg-pgip-process-delids 'pg-pgip-process-ids) @@ -653,7 +665,8 @@ the prover. For remaining optional args, see doc of pg-pgip-last-seen-id nil pg-pgip-last-seen-seq nil pg-pgip-seq 0 - proof-assistant-settings nil)) + proof-assistant-settings nil ;; optional + proof-assistant-idtables nil)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; |