Reorganization and fixes.

2 files changed, 220 insertions, 276 deletions

diff --git a/isa-syntax.el b/isa-syntax.el
index 2cba6435..f7667127 100644
--- a/isa-syntax.el
+++ b/isa-syntax.el
@@ -3,50 +3,79 @@
 
 (require 'proof-syntax)
 
-;; ----- keywords for font-lock.
+
+;;; 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)
+
+;; ----- 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.
+;;  Alternatively: customize this for Marcus Wenzel's 
+;;  proof language.
 
 (defvar isa-keywords-decl
-  '(
-))
+  '("val")
+  "Isabelle keywords for declarations")
+;  :group 'isa-syntax
+;  :type '(repeat string))
 
 (defvar isa-keywords-defn
-  '(
-"bind_thm"
-))
+  '("bind_thm")
+  "Isabelle keywords for definitions")
+;  :group 'isa-syntax
+;  :type '(repeat string))
 
+;; isa-keywords-goal is used to manage undo actions
 (defvar isa-keywords-goal
-  '(
-"goal"
-))
+  '("goal" "goalw" "goalw_cterm")
+  "Isabelle commands to begin an interactive proof")
+;  :group 'isa-syntax
+;  :type '(repeat string))
 
 (defvar isa-keywords-save
-  '(
-"qed"
-))
-
-(defvar isa-keywords-kill-goal '(
-))
+  '("qed" "result" "uresult" "bind_thm" "store_thm")
+  "Isabelle commands to extract the proved theorem")
+;  :group 'isa-syntax
+;  :type '(repeat string))
 
+;; FIXME: and a whole lot more... should be conservative
+;; and use any identifier
 (defvar isa-keywords-commands
-  '(
-"by"
-"goal"
-))
+  '("by" "goal"))
 
 ;; See isa-command-table in Isamode/isa-menus.el to get this list.
+;; BUT: tactics are not commands, so appear inside some expression.
 (defvar isa-tactics
-  '(
-"resolve_tac" "assume_tac"
-))
+  '("resolve_tac" "assume_tac"))
 
 (defvar isa-keywords
   (append isa-keywords-goal isa-keywords-save isa-keywords-decl
 	  isa-keywords-defn isa-keywords-commands isa-tactics)
-  "All keywords in a Isa script")
+  "All keywords in a Isabelle script")
 
-(defvar isa-tacticals '(
-"REPEAT" "THEN" "ORELSE" "TRY"
-))
+(defvar isa-tacticals '("REPEAT" "THEN" "ORELSE" "TRY"))
 
 ;; ----- regular expressions
 
@@ -77,9 +106,6 @@
 		   isa-id ")\\)?") 'font-lock-type-face))
   "*Font-lock table for Isa terms.")
 
-;; According to Isa, "Definition" is both a declaration and a goal.
-;; It is understood here as being a goal.  This is important for
-;; recognizing global identifiers, see isa-global-p.
 (defconst isa-save-command-regexp
   (concat "^" (ids-to-regexp isa-keywords-save)))
 (defconst isa-save-with-hole-regexp
diff --git a/isa.el b/isa.el
index c750d5b4..ceeae833 100644
--- a/isa.el
+++ b/isa.el
@@ -2,108 +2,138 @@
 ;; Copyright (C) 1994-1998 LFCS Edinburgh. 
 ;; Author: David Aspinall
 
-;; $Log$
-;; Revision 2.1  1998/08/21 14:37:18  da
-;; First attempt, proof state works.
-;;
-;; Revision 2.0  1998/08/11 14:59:57  da
-;; New branch
-;;
-;; Revision 1.1  1998/08/11 14:43:34  da
-;; Isabelle proof.el support.
+;; $Id$
 ;;
 
-;; STATUS:
-;;   - Basic proof state extraction works, using prompt regexp
-;;   - Undo needs attention
-
 
 (require 'isa-syntax)
 (require 'outline)
 (require 'proof)
 
-; Configuration
 
-(defvar isa-assistant "Isabelle"
-  "Name of proof assistant")
+;;;
+;;; ======== User settings for Isabelle ========
+;;;
 
-(defvar isa-tags nil ; "/usr/local/lib/isa/theories/TAGS"
-  "the default TAGS table for the Isa library")
+(defvar isa-prog-name "/usr/lib/Isabelle98/bin/isabelle"
+  "*Name of program to run Isabelle.")
 
-(defconst isa-process-config nil
-  "Command to configure pretty printing of the Isa process for emacs.")
+(defvar isa-thy-file-tags-table "/usr/lib/Isabelle98/src/TAGS.thy"
+  "*Name of theory file tags table for Isabelle.")
 
-(defconst isa-interrupt-regexp "Interrupt"
-  "Regexp corresponding to an interrupt")
+(defvar isa-ML-file-tags-table  "/usr/lib/Isabelle98/src/TAGS.ML"
+  "*Name of ML file tags table for Isabelle.")
 
+(defvar isa-indent 2
+  "*Indentation degree in proof scripts.
+Utterly irrelevant for Isabelle because normal proof scripts have
+no regular or easily discernable structure.")
+  
+
+;;;
+;;; ======== Configuration of generic modes ========
+;;;
+
+(defvar isa-mode-config-table
+  '(;; general
+    proof-assistant		"Isabelle"
+    proof-www-home-page
+     "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html"
+    ;; proof script syntax
+    proof-terminal-char	 ?\;		; ends a proof
+    proof-comment-start	"(*"		; comment in a proof
+    proof-comment-end		"*)"		; 
+    ;; proof engine output syntax
+    proof-save-command-regexp   isa-save-command-regexp
+    proof-save-with-hole-regexp isa-save-with-hole-regexp
+    proof-goal-with-hole-regexp isa-goal-with-hole-regexp
+    proof-kill-goal-command	""   ; FIXME: proof.el should allow nil
+    proof-commands-regexp	 (ids-to-regexp isa-keywords)
+    ;; proof engine commands
+    proof-prf-string		"pr()"
+    proof-ctxt-string		"the_context();" 
+    proof-help-string
+     "print \"No in-built help for Isabelle.\"" ; FIXME: proof.el should allow nil
+    ;; command hooks
+    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-global-p		'isa-global-p    ; FIXME: proof.el should allow nil
+    proof-parse-indent		'isa-parse-indent
+    proof-stack-to-indent	'isa-stack-to-indent)
+  "Table of settings for configuration of proof mode to Isabelle.")
+
+
+(defconst isa-shell-mode-config-table
+  '(;;
+    proof-shell-prompt-pattern		"^2?[---=#>]>? *\\|^\\*\\* .*" ; for ML
+    proof-shell-cd			"cd \"%s\";"
+    ;; this one not set: proof-shell-abort-goal-regexp 
+    proof-shell-proof-completed-regexp "No subgoals!"
+    proof-shell-error-regexp		isa-error-regexp
+    proof-shell-interrupt-regexp        "Interrupt"     ; FIXME: only good for NJ/SML
+    proof-shell-noise-regexp	        ""
+    proof-shell-assumption-regexp	isa-id		   ; matches name of assumptions
+    proof-shell-goal-regexp		"^[ \t]*[0-9]+\\. " ; matches subgoal heading
+    ;; We can't hack the SML prompt, so set wakeup-char to nil.
+    proof-shell-wakeup-char		nil
+    proof-shell-start-goals-regexp	"\370"
+    proof-shell-end-goals-regexp	"\371"
+    ;; initial command configures Isabelle by hacking print functions.
+    ;; may need to set directory somewhere for this:
+    ;; /home/da/devel/lego/elisp/   or  $PROOFGENERIC_HOME ?
+    proof-shell-init-cmd		"use \"isa-print-functions.ML\";"
+    ;; === ANNOTATIONS  === remaining ones broken
+    proof-shell-goal-char	        ?\375
+    proof-shell-first-special-char	?\360
+    proof-shell-eager-annotation-start  "\376" 
+    proof-shell-eager-annotation-end    "\377" 
+    proof-shell-annotated-prompt-regexp proof-shell-prompt-pattern ; impossible to annotate!
+    proof-shell-result-start	        "\372 Pbp result \373"
+    proof-shell-result-end		"\372 End Pbp result \373"
+    proof-analyse-using-stack		t
+    proof-shell-start-char		?\372	
+    proof-shell-end-char		?\373 
+    proof-shell-field-char		?\374)
+    "Table of settings for configuration of proof shell mode to Isabelle.")
+
+
+;; =========================================================================
+;; FIXME: THESE TWO ARE DEAD?
 (defvar isa-save-query t
   "*If non-nil, ask user for permission to save the current buffer before
   processing a module.")
 
-(defvar isa-default-undo-limit 100
-  "Maximum number of Undo's possible when doing a proof.")
-
-;; ----- web documentation
-
-(defvar isa-www-home-page "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html")
-
-;; ----- isa-shell configuration options
-
-;; FIXME: needs to have special characters for proof.el, also path
-;; name shouldn't be here.
-(defvar isa-prog-name "/usr/lib/Isabelle98/bin/isabelle"
-  "*Name of program to run as Isabelle.")
-
 (defvar isa-shell-working-dir ""
   "The working directory of the isabelle shell")
+;; =========================================================================
 
-(defvar isa-shell-prompt-pattern 
-  ;; borrowed from somewhere?
-  ;; "^2?[---=#>]>? *\\|^\\*\\* .*"
-  "^> "
-  "*The prompt pattern for the inferior shell running isabelle.")
-
-(defvar isa-shell-cd "cd \"%s\";"
-  "*Command of the inferior process to change the directory.") 
 
-;; FIXME: check this?
-; Don't define this, no correspondence.
-;(defvar isa-shell-abort-goal-regexp nil 
-;  "*Regular expression indicating that the proof of the current goal
-;  has been abandoned.")
+;; ===== outline mode
 
-(defvar isa-shell-proof-completed-regexp "No subgoals!"
-  "*Regular expression indicating that the proof has been completed.")
-
-(defvar isa-goal-regexp
-  "^[ \t]*[0-9]+\\. "
-  "Regexp to match subgoal heading.")
-
-;; ----- outline
-
-;;; FIXME: BROKEN
+;;; FIXME: test and add more things here
 (defvar isa-outline-regexp
-  (ids-to-regexp 
-	   '("Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact"
-	   "Remark" "Record" "Inductive" "Definition")))
+  (ids-to-regexp '("goal" "Goal" "prove_goal"))
+  "Outline regexp for Isabelle ML files")
 
-(defvar isa-outline-heading-end-regexp "\.\\|\\*)")
+;;; End of a command needs parsing to find, so this is approximate.
+(defvar isa-outline-heading-end-regexp ";[ \t\n]*")
 
+;; 
 (defvar isa-shell-outline-regexp isa-goal-regexp)
 (defvar isa-shell-outline-heading-end-regexp isa-goal-regexp)
 
 ;;; ---- end-outline
 
-(defconst isa-kill-goal-command nil) ; "Abort."
-(defconst isa-forget-id-command nil) ; "Reset "
-
-;;; FIXME!!
-(defconst isa-undoable-commands-regexp (ids-to-regexp isa-tactics))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Derived modes - they're here 'cos they define keymaps 'n stuff ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+;;  FIXME: I don't think they should be here at all.
+
 (define-derived-mode isa-shell-mode proof-shell-mode
    "isa-shell" "Inferior shell mode for isabelle shell"
    (isa-shell-mode-config))
@@ -116,17 +146,21 @@
   "pbp" "Proof-by-pointing support for Isabelle"
   (isa-pbp-mode-config))
 
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Code that's Isabelle specific                                  ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;(defun isa-shell-init-hook ()
-;  (remove-hook 'proof-shell-insert-hook 'isa-shell-init-hook))
 
-;(defun isa-set-undo-limit (undos)
-;  (proof-invisible-command (format "Set Undo %s." undos)))
+;; FIXME: think about the next variable.  I've changed sense from
+;;  LEGO and Coq's treatment.
+(defconst isa-not-undoable-commands-regexp
+  (ids-to-regexp '("undo" "back"))
+  "Regular expression matching commands which are *not* undoable.")
 
+;; This next function is the important one for undo operations.
 (defun isa-count-undos (span)
+  "Count number of undos in a span, return the command needed to undo that far."
   (let ((ct 0) str i)
     (if (and span (prev-span span 'type)
 	     (not (eq (span-property (prev-span span 'type) 'type) 'comment))
@@ -136,10 +170,13 @@
       (while span
 	(setq str (span-property span 'cmd))
 	(cond ((eq (span-property span 'type) 'vanilla)
-	       (if (string-match isa-undoable-commands-regexp str)
+	       (or (string-match isa-not-undoable-commands-regexp str)
 		   (setq ct (+ 1 ct))))
 	      ((eq (span-property span 'type) 'pbp)
-	       (cond ((string-match isa-undoable-commands-regexp str)
+	       ;; this case probably redundant for Isabelle, unless
+	       ;; we think of some nice ways of matching non-undoable
+	       ;; commands.
+	       (cond ((not (string-match isa-not-undoable-commands-regexp str))
 		      (setq i 0)
 		      (while (< i (length str))
 			(if (= (aref str i) proof-terminal-char)
@@ -149,15 +186,21 @@
 	(setq span (next-span span 'type)))
       (concat "choplev " (int-to-string ct) proof-terminal-string))))
 
+(defun isa-goal-command-p (str)
+  "Decide whether argument is a goal or not"
+  (string-match isa-goal-command-regexp str)) ; this regexp defined in isa-syntax.el
+
+;; Isabelle has no concept of a Linear context, so forgetting back
+;; to the declaration of a particular something makes no real
+;; sense.  Perhaps in the future there will be functions to remove
+;; theorems from theories, but even then all we could do is
+;; forget particular theorems one by one.
+
+;; FIXME: next function and variable DEAD, irrelevant.
 (defconst isa-keywords-decl-defn-regexp
   (ids-to-regexp (append isa-keywords-decl isa-keywords-defn))
   "Declaration and definition regexp.")
 
-(defun isa-goal-command-p (str)
-  "Decide whether argument is a goal or not"
-  (and (string-match isa-goal-command-regexp str)
-       (not (string-match "Definition.*:=" str))))
-
 (defun isa-find-and-forget (span)
   (let (str ans)
     (while (and span (not ans))
@@ -190,107 +233,59 @@
 (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 ()
-  (cond 
-   ((looking-at "============================\n")
-    (goto-char (match-end 0))
-    (cons 'goal (int-to-string isa-current-goal)))
-   ((looking-at "subgoal \\([0-9]+\\) is:\n")
-    (goto-char (match-end 0))
-    (cons 'goal (match-string 1))
-    (setq isa-current-goal (string-to-int (match-string 1))))
-   ((looking-at proof-shell-assumption-regexp)
-    (cons 'hyp (match-string 1)))
-   (t nil)))
+  (if (looking-at proof-shell-goal-regexp)
+      (cons 'goal (match-string 1))))
 
 (defun isa-state-preserving-p (cmd)
-  (not (string-match isa-undoable-commands-regexp cmd)))
+  "Non-nil if command preserves the proofstate."
+  (string-match isa-not-undoable-commands-regexp cmd))
 
+;; FIXME: I don't really know what this means, but lego sets
+;; it to always return nil.  Probably should be able to
+;; leave it unset.
 (defun isa-global-p (cmd)
-  (or (string-match isa-keywords-decl-defn-regexp cmd)
-      (and (string-match
-	    (concat "Definition\\s-+\\(" isa-id "\\)\\s-*:") cmd)
-	   (string-match ":=" cmd))))
+  nil)
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Commands specific to Isabelle                                  ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun isa-Intros () 
-  "List proof state." 
-  (interactive) 
-  (insert "printlev"))
-
-(defun isa-Apply () 
-  "List proof state."  
-  (interactive) 
-  (insert "Apply "))
-
-(defun isa-Search ()
-  "Search for type in goals."
-  (interactive)
-  (let (cmd)
-    (proof-check-process-available)
-    (setq cmd (read-string "Search Type: " nil 'proof-minibuffer-history))
-    (proof-invisible-command (concat "Search " cmd proof-terminal-string))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Indentation                                                    ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; "Case" is represented by 'c' on the stack, and
-;; "CoInductive is represented by 'C'.
+;;
+;; Sadly this is pretty pointless for Isabelle.
+;; Proof scripts in Isabelle don't really have an easily-observed
+;; block structure  -- a case split can be done by any obscure tactic,
+;; and then solved in a number of steps that bears no relation to the
+;; number of cases!  And the end is certainly not marked in anyway.
+;; 
 (defun isa-stack-to-indent (stack)
-  (cond
+    (cond
    ((null stack) 0)
    ((null (car (car stack)))
     (nth 1 (car stack)))
-   (t (let ((col (save-excursion
-		   (goto-char (nth 1 (car stack)))
-		   (current-column))))
-	(cond
-	 ((eq (car (car stack)) ?c)
-	  (save-excursion (move-to-column (current-indentation))
-			  (cond 
-			   ((eq (char-after (point)) ?|) (+ col 3))
-			   ((looking-at "end") col)
-			   (t (+ col 5)))))	  
-	 ((or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C))
-	  (+ col (if (eq ?| (save-excursion 
-			      (move-to-column (current-indentation))
-			      (char-after (point)))) 2 4)))
-	 (t (1+ col)))))))
+   (t (save-excursion
+	(goto-char (nth 1 (car stack)))
+	(+ isa-indent (current-column))))))
 
 (defun isa-parse-indent (c stack)
-  (cond
-   ((eq c ?C)
-    (cond ((looking-at "Case")
-	   (cons (list ?c (point)) stack))
-	  ((looking-at "CoInductive")
-	   (forward-char (length "CoInductive"))
-	   (cons (list c (- (point) (length "CoInductive"))) stack))
-	  (t stack)))
-   ((and (eq c ?e) (looking-at "end") (eq (car (car stack)) ?c))
-    (cdr stack))
-
-   ((and (eq c ?I) (looking-at "Inductive"))
-    (forward-char (length "Inductive"))
-    (cons (list c (- (point) (length "Inductive"))) stack))
-
-   ((and (eq c ?.) (or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C)))
-    (cdr stack))
-
-   (t stack)))
+  "Indentation function for Isabelle.  Does nothing."
+  stack)
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Isa shell startup and exit hooks                               ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun isa-pre-shell-start ()
-  (setq proof-prog-name isa-prog-name)
-  (setq proof-mode-for-shell 'isa-shell-mode)
-  (setq proof-mode-for-pbp 'isa-pbp-mode)
-)
+  (setq proof-prog-name		isa-prog-name)
+  (setq proof-mode-for-shell    'isa-shell-mode)
+  (setq proof-mode-for-pbp	'isa-pbp-mode))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Configuring proof and pbp mode and setting up various utilities  ;;
@@ -298,7 +293,6 @@
 
 (defun isa-init-syntax-table ()
   "Set appropriate values for syntax table in current buffer."
-
   (modify-syntax-entry ?\$ ".")
   (modify-syntax-entry ?\/ ".")
   (modify-syntax-entry ?\\ ".")
@@ -317,116 +311,40 @@
   (modify-syntax-entry ?\) ")(4"))
 
 (defun isa-mode-config ()
-
-  (setq proof-terminal-char ?\;)
-  (setq proof-comment-start "(*")
-  (setq proof-comment-end "*)")
-
-  (setq proof-assistant isa-assistant
-	proof-www-home-page isa-www-home-page)
-
-  (setq proof-prf-string "pr()"
-	proof-ctxt-string "print \"No context for Isabelle.\""
-	proof-help-string "print \"No in-built help for Isabelle.\"")
-
-  (setq proof-goal-command-p 'isa-goal-command-p
-	proof-count-undos-fn 'isa-count-undos
-	;; this one won't be relevant.
-	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-global-p 'isa-global-p
-	proof-parse-indent 'isa-parse-indent
-	proof-stack-to-indent 'isa-stack-to-indent)
-
-  (setq proof-save-command-regexp isa-save-command-regexp
-	proof-save-with-hole-regexp isa-save-with-hole-regexp
-	proof-goal-with-hole-regexp isa-goal-with-hole-regexp
-	proof-kill-goal-command isa-kill-goal-command
-	proof-commands-regexp (ids-to-regexp isa-keywords))
-
+  (apply 'setq isa-mode-config-table)
   (isa-init-syntax-table)
-
-;; font-lock
-
+  ;; font-lock
   (setq font-lock-keywords isa-font-lock-keywords-1)
-
   (proof-config-done)
-
   (define-key (current-local-map) [(control c) ?I] 'isa-Intros)
   (define-key (current-local-map) [(control c) ?a] 'isa-Apply)
   (define-key (current-local-map) [(control c) (control s)] 'isa-Search)
-
-;; outline
-  
+  ;; outline
+  ;; FIXME: do we need to call make-local-variable here?
   (make-local-variable 'outline-regexp)
   (setq outline-regexp isa-outline-regexp)
-
   (make-local-variable 'outline-heading-end-regexp)
   (setq outline-heading-end-regexp isa-outline-heading-end-regexp)
-
-;; tags
-  (and (boundp 'tag-table-alist)
-       (setq tag-table-alist
-	     (append '(("\\.v$" . isa-tags)
-		       ("isa"  . isa-tags))
-		     tag-table-alist)))
-
+  ;; tags
+  ;  (and (boundp 'tag-table-alist)
+  ;       (setq tag-table-alist
+  ;	     (append '(("\\.ML$"  . isa-ML-file-tags-table)
+  ;		       ("\\.thy$" . isa-thy-file-tags-table))
+  ;		     tag-table-alist)))
   (setq blink-matching-paren-dont-ignore-comments t)
-
-;; hooks and callbacks
-
-  (add-hook 'proof-shell-exit-hook 'isa-zap-line-width nil t)
+  ;; hooks and callbacks
   (add-hook 'proof-pre-shell-start-hook 'isa-pre-shell-start nil t))
 
 
-
 (defun isa-shell-mode-config ()
-  (setq proof-shell-prompt-pattern isa-shell-prompt-pattern
-        proof-shell-cd isa-shell-cd
-; this one not set.
-;        proof-shell-abort-goal-regexp isa-shell-abort-goal-regexp
-        proof-shell-proof-completed-regexp isa-shell-proof-completed-regexp
-        proof-shell-error-regexp isa-error-regexp
-	proof-shell-interrupt-regexp isa-interrupt-regexp
-        proof-shell-noise-regexp ""
-        proof-shell-assumption-regexp isa-id
-        proof-shell-goal-regexp isa-goal-regexp
-        proof-shell-first-special-char ?\360
-        ; The next three represent path annotation information
-
-	proof-shell-eager-annotation-start "\376" 
-	proof-shell-eager-annotation-end "\377" 
-        proof-shell-annotated-prompt-regexp proof-shell-prompt-pattern
-	;(concat proof-shell-prompt-pattern
-	;	(char-to-string proof-shell-wakeup-char))
-        proof-shell-result-start "\372 Pbp result \373"
-        proof-shell-result-end "\372 End Pbp result \373"
-	proof-analyse-using-stack t
-	proof-shell-start-char ?\372 ; not done
-        proof-shell-end-char ?\373 ; not done
-        proof-shell-field-char ?\374  ; not done
-	;; da: settings below here WORK
-	;; ============================
-        proof-shell-goal-char ?\375
-	;; We can't hack the SML prompt, so set wakeup-char to nil.
-        proof-shell-wakeup-char nil
-        proof-shell-start-goals-regexp "\370"
-        proof-shell-end-goals-regexp "\371"
-	;; initial command configures Isabelle by hacking print functions.
-	;; may need directory for this: /home/da/devel/lego/elisp/
-        proof-shell-init-cmd 
-	   "use \"isa-print-functions.ML\";")
-
-
   ;; The following hook is removed once it's called.
   ;; FIXME: maybe add this back later.
   ;;(add-hook 'proof-shell-insert-hook 'isa-shell-init-hook nil t)
-
   (isa-init-syntax-table)
-
+  (apply 'setq isa-shell-mode-config-table)
   (proof-shell-config-done))
 
+;; FIXME: broken, of course, as is all PBP everywhere.
 (defun isa-pbp-mode-config ()
   (setq pbp-change-goal "Show %s.")
   (setq pbp-error-regexp isa-error-regexp))