First attempt at using new indentation for Isabelle. Utterly broken.

1 files changed, 15 insertions, 0 deletions

diff --git a/isa/isa.el b/isa/isa.el
index 68814701..58e6dc82 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -95,6 +95,21 @@ and script mode."
 	 (list isa-goal-with-hole-regexp 2)
 	 (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 engine commands
    proof-showproof-command	"pr();"