diff options
| author | Makarius Wenzel | 1999-06-30 13:39:02 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-06-30 13:39:02 +0000 |
| commit | e5bcf476f0a5348f98e9ef663d76f056cf895cc4 (patch) | |
| tree | 49ecd5e51e9815083866df1d0cebf2b137010675 | |
| parent | cef8f95b4893ce1c6510a54cea8854c9d7413d9b (diff) | |
isar-preprocessing: sync markers;
| -rw-r--r-- | isar/isar.el | 8 |
1 files changed, 7 insertions, 1 deletions
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: ?? |