aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-script.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r--generic/proof-script.el12
1 files changed, 7 insertions, 5 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 7b45c797..447d4176 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2459,7 +2459,10 @@ command."
;; We also need this
(modify-syntax-entry ?\n " ")))
-
+ ;; Set default indent function (can be overriden in derived modes)
+ (make-local-variable 'indent-line-function)
+ (setq indent-line-function 'proof-indent-line)
+
;; During write-file it can happen that we re-set the mode for
;; the currently active scripting buffer. The user might also
;; do this for some reason. We could maybe let
@@ -2474,10 +2477,12 @@ command."
;; that they can be adjusted by prover specific code if need be.
(proof-script-set-buffer-hooks)
- (add-hook 'after-set-visited-file-name-hooks 'proof-script-set-visited-file-name nil t)
+ (add-hook 'after-set-visited-file-name-hooks
+ 'proof-script-set-visited-file-name nil t)
(add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t))
+
(proof-menu-define-keys proof-mode-map) ;; NB: proof-mode-map declared above
(defun proof-script-set-visited-file-name ()
@@ -2779,9 +2784,6 @@ finish setup which depends on specific proof assistant configuration."
(define-key proof-mode-map (vector proof-terminal-char)
'proof-electric-terminator)))
- (make-local-variable 'indent-line-function)
- (setq indent-line-function 'proof-indent-line)
-
;; Toolbar and scripting menu
;; NB: autoloads proof-toolbar, which defines proof-toolbar-scripting-menu.
(proof-toolbar-setup)