From 07104f014aa8a696ac1aee4f4f839c1092d1f160 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Fri, 16 Jun 2000 17:10:24 +0000
Subject: proper indentation setup;

---
 isa/isa-syntax.el | 14 ++++++++++++++
 isa/isa.el        | 22 ++++++++--------------
 2 files changed, 22 insertions(+), 14 deletions(-)

diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 99152eee..d8697cb8 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -287,4 +287,18 @@
    isa-output-font-lock-keywords-1)
   "*Font-lock table for Isabelle goals output.")
 
+
+;; ----- indentation
+
+(defconst isa-indent-any-regexp
+  (proof-regexp-alt (proof-ids-to-regexp isa-keywords) "\\s(" "\\s)"))
+(defconst isa-indent-inner-regexp
+  (proof-regexp-alt "\\s(" "\\s)"))
+(defconst isa-indent-enclose-regexp
+  (proof-ids-to-regexp isa-keywords-save))
+(defconst isa-indent-open-regexp
+  (proof-regexp-alt (proof-ids-to-regexp isa-keywords-goal) "\\s("))
+(defconst isa-indent-close-regexp
+  (proof-regexp-alt (proof-ids-to-regexp isa-keywords-save) "\\s)"))
+
 (provide 'isa-syntax)
diff --git a/isa/isa.el b/isa/isa.el
index 2ecad011..1e3ac17b 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -96,20 +96,14 @@ and script mode."
 	 (list isa-save-with-hole-regexp 2
 	       'backward isa-goal-command-regexp))
 
-   ;; Indentation 
-   ;; FIXME: I don't understand how this works.  
-   ;; Also it doesn't work because of anchoring problems.
-   ;; Tips from Markus?
-   proof-indent-close-offset	-1
-   proof-indent-open-regexp     (proof-regexp-alt 
-				 isa-goal-command-regexp 
-				 "\\s(")
-   proof-indent-close-regexp    (proof-regexp-alt 
-				 isa-save-command-regexp
-				 "\\s)")
-   proof-indent-any-regexp      (apply 'proof-regexp-alt 
-				       isa-keywords-commands)
-   
+   proof-indent-enclose-offset  (- proof-indent)
+   proof-indent-open-offset     0
+   proof-indent-close-offset    0
+   proof-indent-any-regexp      isa-indent-any-regexp
+   proof-indent-inner-regexp    isa-indent-inner-regexp
+   proof-indent-enclose-regexp  isa-indent-enclose-regexp
+   proof-indent-open-regexp     isa-indent-open-regexp
+   proof-indent-close-regexp    isa-indent-close-regexp
    
    ;; proof engine commands
    proof-showproof-command	"pr();"
-- 
cgit v1.2.3