diff options
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r-- | generic/proof-script.el | 12 |
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) |