From 2a56a34d18cdf30010c8063497f3d492240787c0 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 5 Mar 2003 13:19:29 +0000
Subject: Add function to parse consts part of syntax output

---
 isa/isabelle-system.el | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

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
-- 
cgit v1.2.3