diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-vars.el | 10 | ||||
| -rw-r--r-- | generic/proof-autoloads.el | 2 | ||||
| -rw-r--r-- | generic/proof-config.el | 18 | ||||
| -rw-r--r-- | generic/proof-script.el | 34 | ||||
| -rw-r--r-- | generic/proof-shell.el | 9 | ||||
| -rw-r--r-- | generic/proof-site.el | 1 |
6 files changed, 30 insertions, 44 deletions
diff --git a/generic/pg-vars.el b/generic/pg-vars.el index 7e46e7cb..5a83bb19 100644 --- a/generic/pg-vars.el +++ b/generic/pg-vars.el @@ -161,16 +161,6 @@ assistant during the last group of commands.") If non-nil, the value counts the commands from the last command of the proof (starting from 1).") -;; TODO da: remove proof-terminal-string. At the moment some -;; commands need to have the terminal string, some don't. -;; It's used variously in proof-script and proof-shell, which -;; is another mess. [Shell mode implicitly assumes script mode -;; has been configured]. -;; We should assume commands are terminated at the specific level. - -(defvar proof-terminal-string nil - "End-of-line string for proof process.") - ;; diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index ab4da2aa..bc6f3671 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -739,7 +739,7 @@ Send CMD to the proof process. The CMD is `invisible' in the sense that it is not recorded in buffer. CMD may be a string or a string-yielding expression. -Automatically add `proof-terminal-char' if necessary, examining +Automatically add `proof-terminal-string' if necessary, examining `proof-shell-no-auto-terminate-commands'. By default, let the command be processed asynchronously. diff --git a/generic/proof-config.el b/generic/proof-config.el index b0944a07..b817b10b 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -223,12 +223,12 @@ conversion, etc. (No changes are done if nil)." :group 'prover-config :prefix "proof-") -(defcustom proof-terminal-char nil - "Character that terminates commands sent to prover; nil if none. +(defcustom proof-terminal-string nil + "String that terminates commands sent to prover; nil if none. To configure command recognition properly, you must set at least one of these: `proof-script-sexp-commands', `proof-script-command-end-regexp', -`proof-script-command-start-regexp', `proof-terminal-char', +`proof-script-command-start-regexp', `proof-terminal-string', or `proof-script-parse-function'." :type 'character :group 'prover-config) @@ -244,7 +244,7 @@ You should set this variable in script mode configuration. To configure command recognition properly, you must set at least one of these: `proof-script-sexp-commands', `proof-script-command-end-regexp', -`proof-script-command-start-regexp', `proof-terminal-char', +`proof-script-command-start-regexp', `proof-terminal-string', or `proof-script-parse-function'." :type 'boolean :group 'prover-config) @@ -262,7 +262,7 @@ i.e. (match-beginning 1), rather than (match-end 0). To configure command recognition properly, you must set at least one of these: `proof-script-sexp-commands', `proof-script-command-end-regexp', -`proof-script-command-start-regexp', `proof-terminal-char', +`proof-script-command-start-regexp', `proof-terminal-string', or `proof-script-parse-function'." :type 'string :group 'prover-config) @@ -273,7 +273,7 @@ You should set this variable in script mode configuration. To configure command recognition properly, you must set at least one of these: `proof-script-sexp-commands', `proof-script-command-end-regexp', -`proof-script-command-start-regexp', `proof-terminal-char', +`proof-script-command-start-regexp', `proof-terminal-string', or `proof-script-parse-function'." :type 'string :group 'prover-config) @@ -310,7 +310,7 @@ a symbol indicating what has been parsed: nil if there is no complete next segment in the buffer If this is left unset, it will be configured automatically to -a generic function according to which of `proof-terminal-char' +a generic function according to which of `proof-terminal-string' and its friends are set." :type 'string :group 'prover-config) @@ -806,8 +806,8 @@ are interpreted literally as part of the program name." "Non-nil if Proof General should try to add terminator to every command. If non-nil, whenever a command is sent to the prover using `proof-shell-invisible-command', Proof General will check to see if it -ends with `proof-terminal-char', and add it if not. -If `proof-terminal-char' is nil, this has no effect." +ends with `proof-terminal-string', and add it if not. +If `proof-terminal-string' is nil, this has no effect." :type 'boolean :group 'proof-shell) diff --git a/generic/proof-script.el b/generic/proof-script.el index e97e313e..53880933 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1875,13 +1875,13 @@ always defaults to inserting a semi (nicer might be to parse for a comment, and insert or skip to the next semi)." (let ((mrk (point)) ins incomment) (if (< mrk (proof-unprocessed-begin)) - (insert proof-terminal-char) ; insert immediately in locked region + (insert proof-terminal-string) ; insert immediately in locked region (if (proof-only-whitespace-to-locked-region-p) (error "There's nothing to do!")) (skip-chars-backward " \t\n") (unless (or proof-electric-terminator-noterminator (and (char-after (point)) - (= (char-after (point)) proof-terminal-char))) + (= (char-after (point)) proof-terminal-string))) (insert proof-terminal-string) (setq ins t)) (let* ((pos @@ -2313,12 +2313,6 @@ assistant." proof-included-files-list) (proof-complete-buffer-atomic (current-buffer))) - ;; calculate some strings and regexps for searching - (setq proof-terminal-string - (if proof-terminal-char - (char-to-string proof-terminal-char) - "")) - (make-local-variable 'comment-start) (setq comment-start (concat proof-script-comment-start " ")) (make-local-variable 'comment-end) @@ -2379,7 +2373,8 @@ For this function to work properly, you must configure `proof-undo-n-times-cmd' and `proof-ignore-for-undo-count'." (let ((case-fold-search proof-case-fold-search) - (ct 0) str i) + (ct 0) str i + (tl (length proof-terminal-string))) (while span (setq str (span-property span 'cmd)) (cond ((eq (span-property span 'type) 'vanilla) @@ -2388,7 +2383,8 @@ For this function to work properly, you must configure ((eq (span-property span 'type) 'pbp) (setq i 0) (while (< i (length str)) - (if (= (aref str i) proof-terminal-char) (incf ct)) + (if (string-equal (substring str i (+ i tl)) proof-terminal-string) + (incf ct)) (incf i)))) (setq span (next-span span 'type))) (if (= ct 0) @@ -2484,13 +2480,13 @@ finish setup which depends on specific proof assistant configuration." (dolist (sym proof-script-important-settings) (proof-warn-if-unset "proof-config-done" sym)) - ;; Additional key def for terminal char - (if proof-terminal-char + ;; Additional key def for (first character of) terminal string + (if proof-terminal-string (progn (define-key proof-mode-map - (vconcat [(control c)] (vector proof-terminal-char)) + (vconcat [(control c)] (vector (aref proof-terminal-string 0))) 'proof-electric-terminator-toggle) - (define-key proof-mode-map (vector proof-terminal-char) + (define-key proof-mode-map (vector (aref proof-terminal-string 0)) 'proof-electric-terminator))) ;; Toolbar and main menu (loads proof-toolbar,setting p.-toolbar-scripting-menu) @@ -2538,16 +2534,16 @@ Choice of function depends on configuration setting." (setq proof-script-parse-function 'proof-script-generic-parse-sexp)) (proof-script-command-start-regexp (setq proof-script-parse-function 'proof-script-generic-parse-cmdstart)) - ((or proof-script-command-end-regexp proof-terminal-char) + ((or proof-script-command-end-regexp proof-terminal-string) (setq proof-script-parse-function 'proof-script-generic-parse-cmdend) (unless proof-script-command-end-regexp - (proof-warn-if-unset "probof-config-done" 'proof-terminal-char) + (proof-warn-if-unset "probof-config-done" 'proof-terminal-string) (setq proof-script-command-end-regexp - (if proof-terminal-char - (regexp-quote (char-to-string proof-terminal-char)) + (if proof-terminal-string + (regexp-quote proof-terminal-string) "$")))) (t - (error "Configuration error: must set `proof-terminal-char' or one of its friends"))))) + (error "Configuration error: must set `proof-terminal-string' or one of its friends"))))) (defun proof-setup-imenu () "Setup a default for imenu, perhaps using `proof-script-imenu-generic-expression'." diff --git a/generic/proof-shell.el b/generic/proof-shell.el index acca04ed..58ea9844 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1570,7 +1570,7 @@ Calls proof-state-change-hook." The CMD is `invisible' in the sense that it is not recorded in buffer. CMD may be a string or a string-yielding expression. -Automatically add `proof-terminal-char' if necessary, examining +Automatically add `proof-terminal-string' if necessary, examining `proof-shell-no-auto-terminate-commands'. By default, let the command be processed asynchronously. @@ -1588,13 +1588,12 @@ FLAGS are put onto the If NOERROR is set, surpress usual error action." (setq cmd (eval cmd))) (if cmd (progn - (unless (or (null proof-terminal-char) + (unless (or (null proof-terminal-string) (not proof-shell-auto-terminate-commands) (string-match (concat - (regexp-quote - (char-to-string proof-terminal-char)) + (regexp-quote proof-terminal-string) "[ \t]*$") cmd)) - (setq cmd (concat cmd (char-to-string proof-terminal-char)))) + (setq cmd (concat cmd proof-terminal-string))) (if wait (proof-shell-wait)) (proof-shell-ready-prover) ; start proof assistant; set vars. (let* ((callback diff --git a/generic/proof-site.el b/generic/proof-site.el index f15e492e..dead3a79 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -28,6 +28,7 @@ (coq "Coq" "\\.v$\\|\\.v8$\\|\\.v7$") (phox "PhoX" "\\.phx$") (lego "LEGO" "\\.l$") + (hol-light "HOL Light" "\\.l$") ;; Obscure: |