Cleanups and a bit more highlighting

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 <engine>-syntax.el.
-;;;
-;;;   Seems a bit daft: why not just have the customization in
-;;;   one place, and settings hardwired in <engine>-syntax.el.
-;;;
-;;;   That way we can see which settings are part of instantiation of
-;;;   proof.el, and which are part of cusomization for <engine>.
-
-;; ------ 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))