From afac912bfc8f41ccaca548ea8d0bb557fbea88a9 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 16 Nov 1999 21:04:16 +0000 Subject: Cleanups and a bit more highlighting --- isa/isa-syntax.el | 61 +++++++------------ isa/isa.el | 171 +++++++++--------------------------------------------- 2 files changed, 51 insertions(+), 181 deletions(-) diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el index c18ea0a7..d6ad598e 100644 --- a/isa/isa-syntax.el +++ b/isa/isa-syntax.el @@ -7,34 +7,9 @@ ;; $Id$ ;; ;; -;; FIXME: the syntax needs checking carefully, and splitting -;; into output vs input syntax. -;; - (require 'proof-syntax) -;;; Proof mode customization: how should it work? -;;; Presently we have a bunch of variables in proof.el which are -;;; set from a bunch of similarly named variables in -syntax.el. -;;; -;;; Seems a bit daft: why not just have the customization in -;;; one place, and settings hardwired in -syntax.el. -;;; -;;; That way we can see which settings are part of instantiation of -;;; proof.el, and which are part of cusomization for . - -;; ------ customize groups - -;(defgroup isa-scripting nil -; "Customization of Isabelle script management" -; :group 'external -; :group 'languages) - -;(defgroup isa-syntax nil -; "Customization of Isabelle's syntax recognition" -; :group 'isa-scripting) - -;; ----- character syntax +;; character syntax (defun isa-init-syntax-table () "Set appropriate values for syntax table in current buffer." @@ -63,20 +38,21 @@ ;; inside them (modify-syntax-entry ?\" " ")) +;; +;; Syntax for font-lock and other features +;; -;; ----- syntax for font-lock and other features - -;; FIXME: this command-keyword orientation isn't good -;; enough for Isabelle, since we can have arbitrary -;; ML code around. One solution is to define a -;; restricted language consisting of the interactive -;; commands. We'd still need regexps below, though. -;; Alternative 1: customize this for Markus Wenzel's -;; proof language. Markus has done this now! -;; Alternative 2: add hooks from Isabelle to say -;; "I've just seen a goal command" or "I've just seen a -;; tactic". This would allow more accurate -;; counting of undos. +;; Note: this command-keyword recognition of the proof script isn't +;; good enough for Isabelle, since we can have arbitrary ML code +;; around. +;; Alternatives: +;; 1) propose a restricted language consisting of the interactive +;; commands. Or try Markus Wenzel's Isar proof language! +;; 2) add hooks from Isabelle to say "I've just seen a goal command" +;; or "I've just seen a tactic". This would allow more accurate +;; counting of undos. We could even approximate this without hooks, +;; by examining the proof state output carefully. +;; ;; FIXME da: here are some examples of input failures I've ;; found in real proofs: @@ -302,5 +278,12 @@ ) "*Font-lock table for Isabelle terms.") +(defvar isa-goals-font-lock-keywords + (append + (list + "^Level [0-9].*" + "^No subgoals!$" + "\\s-*[0-9][0-9]?\\. ") + isa-output-font-lock-keywords-1)) (provide 'isa-syntax) diff --git a/isa/isa.el b/isa/isa.el index 34697768..abccc07f 100644 --- a/isa/isa.el +++ b/isa/isa.el @@ -10,6 +10,7 @@ ;; Add Isabelle image onto splash screen +;; (customize-set-variable 'proof-splash-extensions '(list @@ -19,25 +20,6 @@ (require 'proof) (require 'isa-syntax) -;; To make byte compiler be quiet. -;; NASTY: these result in loads when evaluated -;; ordinarily (from non-byte compiled code). -;(eval-when-compile -; (require 'proof-script) -; (require 'proof-shell) -; (require 'outline) -; (cond ((fboundp 'make-extent) (require 'span-extent)) -; ((fboundp 'make-overlay) (require 'span-overlay)))) - - - -;;; variable: proof-analyse-using-stack -;;; proof-locked-region-empty-p, proof-shell-insert, pbp-mode, -;;; proof-complete-buffer-atomic, proof-shell-invisible-command, -;;; prev-span, span-property, next-span, proof-unprocessed-begin, -;;; proof-config-done, proof-shell-config-done - - ;;; ;;; ======== User settings for Isabelle ======== ;;; @@ -71,9 +53,6 @@ no regular or easily discernable structure." ;;; ======== Configuration of generic modes ======== ;;; -;; ===== outline mode - -;;; FIXME: test and add more things here (defcustom isa-outline-regexp (proof-ids-to-regexp '("goal" "Goal" "prove_goal")) "Outline regexp for Isabelle ML files" @@ -86,18 +65,12 @@ no regular or easily discernable structure." :type 'regexp :group 'isabelle-config) -;; FIXME: not sure about this one (defvar isa-shell-outline-regexp "\370[ \t]*\\([0-9]+\\)\\.") (defvar isa-shell-outline-heading-end-regexp "$") -;;; ---- end-outline -;;; NB! Disadvantage of *not* shadowing variables is that user -;;; cannot override them. It might be nice to override some -;;; variables, which ones? - (defun isa-mode-config-set-variables () "Configure generic proof scripting/thy mode variables for Isabelle. Settings here are the ones which are needed for both shell mode @@ -141,7 +114,6 @@ and script mode." proof-goal-command-p 'isa-goal-command-p proof-count-undos-fn 'isa-count-undos proof-find-and-forget-fn 'isa-find-and-forget - proof-goal-hyp-fn 'isa-goal-hyp proof-state-preserving-p 'isa-state-preserving-p proof-parse-indent 'isa-parse-indent proof-stack-to-indent 'isa-stack-to-indent @@ -150,8 +122,10 @@ and script mode." proof-completed-proof-behaviour 'closeany proof-shell-compute-new-files-list 'isa-shell-compute-new-files-list - proof-shell-inform-file-processed-cmd "ProofGeneral.inform_file_processed \"%s\";" - proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%s\";")) + proof-shell-inform-file-processed-cmd + "ProofGeneral.inform_file_processed \"%s\";" + proof-shell-inform-file-retracted-cmd + "ProofGeneral.inform_file_retracted \"%s\";")) (defun isa-shell-mode-config-set-variables () @@ -161,12 +135,8 @@ and script mode." proof-shell-wakeup-char ?\372 proof-shell-annotated-prompt-regexp "\\(val it = () : unit\n\\)?> \372" - ;; "^\\(val it = () : unit\n\\)?> " - ;; non-annotation, with val it's: "^\\(val it = () : unit\n\\)?> " - ;; This pattern is just for comint, it matches a range of - ;; prompts from a range of MLs, including Isabelle's edited - ;; version. + ;; This pattern is just for comint proof-shell-prompt-pattern "^2?[ML-=#>]>? \372?" ;; for issuing command, not used to track cwd in any way. @@ -205,11 +175,6 @@ and script mode." proof-shell-clear-response-regexp "Proof General, please clear the response buffer." proof-shell-clear-goals-regexp "Proof General, please clear the goals buffer." - ;; Tested values of proof-shell-eager-annotation-start: - ;; "^\\[opening \\|^###\\|^Reading\\|^Proof General\\|^Not reading" - ;; "^---\\|^\\[opening " - ;; could be last bracket on end of line, or with ### and ***. - ;; Dirty hack to allow font-locking for output based on hidden ;; annotations, see isa-output-font-lock-keywords-1 proof-shell-leave-annotations-in-output t @@ -251,27 +216,19 @@ and script mode." ;;; Theory loader operations ;;; -(defun isa-update-thy-only (file try wait) - "Tell Isabelle to update current buffer's theory, and all ancestors." - (proof-shell-invisible-command - (format "ProofGeneral.%supdate_thy_only \"%s\";" - (if try "try_" "") (file-name-sans-extension file)) - wait)) - ;; Experiments for background non-blocking loading of theory: this is -;; quite difficult, actually: we need to set a callback from +;; quite difficult, actually: we need to set a callback from ;; proof-done-invisible to take the final step in switching on ;; scripting. We may be able to pass the hook argument into the ;; action list using the "span" argument which means nothing for ;; invisible command usually. -;(defun isa-update-error (&rest args) -; "Callback for proof-invisible-command. -;In case an update leads to an error/interrupt in Isabelle, -;we make sure scripting is deactivated and raise an elisp error." -; (if proof-shell-error-or-interrupt-seen -; (proof-deactivate-scripting)) -; (proof-shell-done-invisible "Isabelle Proof General: error during use_thy, scripting not activated!")) +(defun isa-update-thy-only (file try wait) + "Tell Isabelle to update current buffer's theory, and all ancestors." + (proof-shell-invisible-command + (format "ProofGeneral.%supdate_thy_only \"%s\";" + (if try "try_" "") (file-name-sans-extension file)) + wait)) (defun isa-shell-update-thy () "Possibly issue update_thy_only command to Isabelle. @@ -287,14 +244,13 @@ This is a hook function for proof-activate-scripting-hook." ;; up to date, after all, the user wasn't allowed to edit ;; anything that this file depends on, was she? (progn - ;; Wait after sending, so that queue is cleared - ;; for further commands without giving "proof process - ;; busy" error. + ;; Wait after sending, so that queue is cleared for further + ;; commands without giving "proof process busy" error. (isa-update-thy-only buffer-file-name t ;; whether to block or not (if (and (boundp 'activated-interactively) activated-interactively) - t ; was nil, but will falsely leave Scripting on! + t ; was nil, but falsely leaves Scripting on! t)) ;; Leave the messages from the update around. (setq proof-shell-erase-response-flag nil)))) @@ -344,14 +300,10 @@ proof-shell-retract-files-regexp." "Isabelle script" nil (isa-mode-config))) -; (define-key isa-proofscript-mode-map -; [(control c) (control l)] 'proof-prf) ; keybinding like Isamode - - - - +;; ;; Automatically selecting theory mode or Proof General script mode. +;; (defun isa-mode () "Mode for Isabelle buffers: either isa-proofscript-mode or thy-mode. @@ -420,7 +372,6 @@ you will be asked to retract the file or process the remainder of it. (file-name-nondirectory (file-name-sans-extension file))))) - ;; Next bits taken from isa-load.el ;; isa-load.el,v 3.8 1998/09/01 @@ -470,13 +421,10 @@ you will be asked to retract the file or process the remainder of it. -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Code that's Isabelle specific ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - +;; +;; Code that's Isabelle specific +;; -;; FIXME: think about the next variable. I've changed sense from -;; LEGO and Coq's treatment. (defcustom isa-not-undoable-commands-regexp (proof-ids-to-regexp '("undo" "back")) "Regular expression matching commands which are *not* undoable." @@ -500,10 +448,10 @@ you will be asked to retract the file or process the remainder of it. (or (proof-string-match isa-not-undoable-commands-regexp str) (setq ct (+ 1 ct)))) ((eq (span-property span 'type) 'pbp) - ;; this case probably redundant for Isabelle, unless - ;; we think of some nice ways of matching non-undoable - ;; commands. - (cond ((not (proof-string-match isa-not-undoable-commands-regexp str)) + ;; this case probably redundant for Isabelle, unless we + ;; think of some nice ways of matching non-undoable cmds. + (cond ((not (proof-string-match + isa-not-undoable-commands-regexp str)) (setq i 0) (while (< i (length str)) (if (= (aref str i) proof-terminal-char) @@ -511,7 +459,8 @@ you will be asked to retract the file or process the remainder of it. (setq i (+ 1 i)))) (t nil)))) (setq span (next-span span 'type))) - (concat "ProofGeneral.repeat_undo " (int-to-string ct) proof-terminal-string)))) + (concat "ProofGeneral.repeat_undo " + (int-to-string ct) proof-terminal-string)))) (defun isa-goal-command-p (str) "Decide whether argument is a goal or not" @@ -523,74 +472,12 @@ you will be asked to retract the file or process the remainder of it. ;; theorems from theories, but even then all we could do is ;; forget particular theorems one by one. So we ought to search ;; backwards in isa-find-and-forget, rather than forwards as -;; the old code below does. +;; the code from the type theory provers does. ;; MMW: this version even does nothing at all (defun isa-find-and-forget (span) proof-no-command) -;(defun isa-find-and-forget (span) -; "Return a command to be used to forget SPAN." -; (save-excursion -; ;; FIXME: bug here: too much gets retracted. -; ;; See if we are going to part way through a completely processed -; ;; buffer, in which case it should be removed from -; ;; proof-included-files-list along with any other buffers -; ;; depending on it. However, even though we send the retraction -; ;; command to Isabelle we don't want to *completely* unlock -; ;; the current buffer. How can this be avoided? -; (goto-char (point-max)) -; (skip-chars-backward " \t\n") -; (if (>= (proof-unprocessed-begin) (point)) -; (format isa-retract-thy-file-command -; (file-name-sans-extension -; (file-name-nondirectory -; (buffer-file-name)))) -; proof-no-command))) - - -;; BEGIN Old code (taken from Coq.el) -;(defconst isa-keywords-decl-defn-regexp -; (ids-to-regexp (append isa-keywords-decl isa-keywords-defn)) -; "Declaration and definition regexp.") -;(defun isa-find-and-forget (span) -; (let (str ans) -; (while (and span (not ans)) -; (setq str (span-property span 'cmd)) -; (cond -; ((eq (span-property span 'type) 'comment)) - -; ((eq (span-property span 'type) 'goalsave) -; (setq ans (concat isa-forget-id-command -; (span-property span 'name) proof-terminal-string))) - -; ((proof-string-match (concat "\\`\\(" isa-keywords-decl-defn-regexp -; "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str) -; (setq ans (concat isa-forget-id-command -; (match-string 2 str) proof-terminal-string))) -; ;; If it's not a goal but it contains "Definition" then it's a -; ;; declaration -; ((and (not (isa-goal-command-p str)) -; (proof-string-match -; (concat "Definition\\s-+\\(" proof-id "\\)\\s-*:") str)) -; (setq ans (concat isa-forget-id-command -; (match-string 2 str) proof-terminal-string)))) -; (setq span (next-span span 'type))) -; (or ans "COMMENT"))) -; END old code - -(defvar isa-current-goal 1 - "Last goal that emacs looked at.") - -;; Parse proofstate output. Isabelle does not display -;; named hypotheses in the proofstate output: they -;; appear as a list in each subgoal. Ignore -;; that aspect for now and just return the -;; subgoal number. -(defun isa-goal-hyp () - (if (looking-at proof-shell-goal-regexp) - (cons 'goal (match-string 1)))) - (defun isa-state-preserving-p (cmd) "Non-nil if command preserves the proofstate." (not (proof-string-match isa-not-undoable-commands-regexp cmd))) @@ -671,7 +558,7 @@ you will be asked to retract the file or process the remainder of it. (setq pbp-change-goal "Show %s.") (setq pbp-error-regexp proof-shell-error-regexp) (isa-init-output-syntax-table) - (setq font-lock-keywords isa-output-font-lock-keywords-1) + (setq font-lock-keywords isa-goals-font-lock-keywords) (proof-goals-config-done)) -- cgit v1.2.3