From e5bcf476f0a5348f98e9ef663d76f056cf895cc4 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Wed, 30 Jun 1999 13:39:02 +0000
Subject: isar-preprocessing: sync markers;

---
 isar/isar.el | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/isar/isar.el b/isar/isar.el
index 955952ee..e42c5bd2 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -574,6 +574,11 @@ Resulting output from Isabelle will be parsed by Proof General."
   (modify-syntax-entry ?\{ "(}1")
   (modify-syntax-entry ?\} "){4"))
 
+(defun isar-preprocessing ()
+  "insert sync markers - acts on variable string by dynamic scoping"
+  (if (not (string-match "^cd \\|^ProofGeneral\\.init " string))   ;; FIXME hack to detect initial ML stuff
+      (setq string (concat "\\<^sync>" string "\\<^sync>;"))))
+
 (defun isar-mode-config ()
   (isar-mode-config-set-variables)
   (isar-init-syntax-table)
@@ -592,7 +597,8 @@ Resulting output from Isabelle will be parsed by Proof General."
   ;	     (append '(("\\.ML$"  . isar-ML-file-tags-table)
   ;		       ("\\.thy$" . thy-file-tags-table))
   ;		     tag-table-alist)))
-  (setq blink-matching-paren-dont-ignore-comments t))
+  (setq blink-matching-paren-dont-ignore-comments t)
+  (add-hook 'proof-shell-insert-hook 'isar-preprocessing))
 
 
 ;; MMW FIXME: ??
-- 
cgit v1.2.3