From fcb6f0745c966fe600fc5b54ef8a21ca2944c228 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 7 Jun 2000 18:07:25 +0000
Subject: Failed attempted hack to support ML files in isar mode (see comments
 in isar-preprocessing).

---
 isar/isar.el | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/isar/isar.el b/isar/isar.el
index d5b6401e..c513f4ca 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -534,7 +534,18 @@ proof-shell-retract-files-regexp."
     (setq string (concat 
 		  "\\<^sync>" 
 		  (isar-shell-adjust-line-width) 
-		  string 
+		  ;; da: this was an attempted hack to deal with ML files,
+		  ;; unfortunately Isar complains about not seeing a theory
+		  ;; command first: ML_setup illegal at first line
+		  ;; Another failure is that: (* comment *) foo; 
+		  ;; ignores foo.  This could be fixed by scanning for
+		  ;; comment end in proof-script.el's function 
+		  ;; proof-segment-upto-cmdstart (which becomes even more
+		  ;; Isar specific, then...)
+		  ;; (if (string-match "\\.ML$" (buffer-name proof-script-buffer))
+		  ;;    (format "ML_setup {* %s *};" string)
+		  ;;    string)
+		  string
 		  "\\<^sync>;"))))
 
 (defun isar-markup-ml (string)
-- 
cgit v1.2.3