diff options
| -rw-r--r-- | isa/isa-syntax.el | 14 | ||||
| -rw-r--r-- | 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) @@ -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();" |