diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-03-05 13:19:29 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-03-05 13:19:29 +0000 |
| commit | 2a56a34d18cdf30010c8063497f3d492240787c0 (patch) | |
| tree | 33486e2e0b75265c7299d6c796adbc6a512562b7 | |
| parent | ddbd935f4f5d4be8918efb5352af32f0af478e0a (diff) | |
Add function to parse consts part of syntax output
| -rw-r--r-- | isa/isabelle-system.el | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el index 03dbd5a4..d294f9ed 100644 --- a/isa/isabelle-system.el +++ b/isa/isabelle-system.el @@ -544,5 +544,27 @@ the function `pg-remove-specials' can be used instead)." "")) ;; Empty string in case called with non PGIP-aware Isabelle. +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Understanding syntax configuration (really should be PGIP, but...) +;; +;; [PRESENTLY UNUSED; WORK IN PROGRESS] + +(defun isabelle-parse-syntax-dump (buf) + (save-excursion + (let (consts start lim) + (set-buffer buf) + (goto-char (point-min)) + (if (re-search-forward "consts:" nil t) + (progn + (setq start (point)) + (setq lim (re-search-forward "parse_ast_translation:" nil t)) + (goto-char start) + (while (re-search-forward "\"\\([^\"]*\\)\"" lim t) + (if (< 0 (length (match-string 1))) + (setq consts (cons (match-string 1) consts)))))) + consts))) + + (provide 'isabelle-system) ;; End of isabelle-system.el |