Renamed/added defcustom support.

3 files changed, 684 insertions, 0 deletions

diff --git a/isa/isa-print-functions.ML b/isa/isa-print-functions.ML
new file mode 100644
index 00000000..3af539a5
--- /dev/null
+++ b/isa/isa-print-functions.ML
@@ -0,0 +1,172 @@
+(* 
+   isa-print-functions.ML
+
+   Customized version of Isabelle printing for script management
+   mode.
+
+   $Id$
+
+*)
+
+
+
+val proof_state_special_prefix="\248";
+val proof_state_special_suffix="\249";
+val goal_start_special="\253";
+
+
+
+(* val orig_prs_fn = !prs_fn; *)
+(* val orig_warning_fn = !warning_fn; *)
+(* val orig_error_fn = !error_fn; *)
+
+(* copied from Pure/library.ML: *)
+local
+  fun out s =
+    (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+
+  fun prefix_lines prfx txt =
+    txt |> split_lines |> map (fn s => prfx ^ s ^ "\n") |> implode;
+in
+
+(*hooks for output channels: normal, warning, error*)
+
+(* da: NO CHANGES NEEDED YET *)
+val () =
+	(prs_fn := (fn s => out s);
+	 warning_fn := (fn s => out (prefix_lines "### " s));
+	error_fn := (fn s => out (prefix_lines "*** " s)))
+
+end;
+
+
+
+local
+
+  (* utils *)
+
+  fun ins_entry (x, y) [] = [(x, [y])]
+    | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
+        if x = x' then (x', y ins ys') :: pairs
+        else pair :: ins_entry (x, y) pairs;
+
+  fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
+    | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
+    | add_consts (Abs (_, _, t), env) = add_consts (t, env)
+    | add_consts (_, env) = env;
+
+  fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
+    | add_vars (Var (xi, T), env) = ins_entry (T, xi) env
+    | add_vars (Abs (_, _, t), env) = add_vars (t, env)
+    | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
+    | add_vars (_, env) = env;
+
+  fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env)
+    | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
+    | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
+
+  fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
+  fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
+
+
+  (* prepare atoms *)
+
+  fun consts_of t = sort_cnsts (add_consts (t, []));
+  fun vars_of t = sort_idxs (add_vars (t, []));
+  fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
+
+in
+
+  fun script_print_goals maxgoals state =
+    let
+      val {sign, ...} = rep_thm state;
+
+      val prt_term = Sign.pretty_term sign;
+      val prt_typ = Sign.pretty_typ sign;
+      val prt_sort = Sign.pretty_sort sign;
+
+      fun prt_atoms prt prtT (X, xs) = Pretty.block
+        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
+          Pretty.brk 1, prtT X];
+
+      fun prt_var (x, ~1) = prt_term (Syntax.free x)
+        | prt_var xi = prt_term (Syntax.var xi);
+
+      fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
+        | prt_varT xi = prt_typ (TVar (xi, []));
+
+      val prt_consts = prt_atoms (prt_term o Const) prt_typ;
+      val prt_vars = prt_atoms prt_var prt_typ;
+      val prt_varsT = prt_atoms prt_varT prt_sort;
+
+
+      fun print_list _ _ [] = ()
+        | print_list name prt lst = (writeln "";
+            Pretty.writeln (Pretty.big_list name (map prt lst)));
+
+      fun print_subgoals (_, []) = ()
+        | print_subgoals (n, A :: As) = (Pretty.writeln (Pretty.blk (0,
+            [Pretty.str (goal_start_special ^
+			  " " ^ string_of_int n ^ ". "), prt_term A]));
+              print_subgoals (n + 1, As));
+
+      val print_ffpairs =
+        print_list "Flex-flex pairs:" (prt_term o Logic.mk_flexpair);
+
+      val print_consts = print_list "Constants:" prt_consts o consts_of;
+      val print_vars = print_list "Variables:" prt_vars o vars_of;
+      val print_varsT = print_list "Type variables:" prt_varsT o varsT_of;
+
+
+      val {prop, ...} = rep_thm state;
+      val (tpairs, As, B) = Logic.strip_horn prop;
+      val ngoals = length As;
+
+      fun print_gs (types, sorts) =
+       (Pretty.writeln (prt_term B);
+        if ngoals = 0 then writeln "No subgoals!"
+        else if ngoals > maxgoals then
+          (print_subgoals (1, take (maxgoals, As));
+            writeln ("A total of " ^ string_of_int ngoals ^ " subgoals..."))
+        else print_subgoals (1, As);
+
+        print_ffpairs tpairs;
+
+        if types andalso ! show_consts then print_consts prop else ();
+        if types then print_vars prop else ();
+        if sorts then print_varsT prop else ());
+    in
+      setmp show_no_free_types true
+        (setmp show_types (! show_types orelse ! show_sorts)
+          (setmp show_sorts false print_gs))
+     (! show_types orelse ! show_sorts, ! show_sorts)
+  end;
+
+end;
+
+
+
+
+(* Pure/goals.ML declares print_current_goals_fn. *)
+
+val orig_print_current_goals_fn = !print_current_goals_fn;
+
+fun script_mode_print_current_goals_fn n max th =
+  (writeln ("Level " ^ string_of_int n); script_print_goals max th);
+
+local
+  fun out s =
+    (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+  fun cgf i j t =
+     (out proof_state_special_prefix;
+      script_mode_print_current_goals_fn i j t;
+      out proof_state_special_suffix)
+in
+ val () = (print_current_goals_fn := cgf)
+end
+
+
+
+
+
+				
\ No newline at end of file
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
new file mode 100644
index 00000000..2672ae68
--- /dev/null
+++ b/isa/isa-syntax.el
@@ -0,0 +1,146 @@
+;; isa-syntax.el Syntax expressions for Isabelle
+;;
+
+(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)
+
+;; ----- 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.
+
+
+(defgroup isa-syntax nil
+  "Customization of Isabelle syntax for proof mode"
+  :group 'isa-settings)
+
+(defcustom isa-keywords-decl
+  '("val")
+  "Isabelle keywords for declarations"
+  :group 'isa-syntax
+  :type '(repeat string))
+
+(defcustom isa-keywords-defn
+  '("bind_thm")
+  "Isabelle keywords for definitions"
+  :group 'isa-syntax
+  :type '(repeat string))
+
+;; isa-keywords-goal is used to manage undo actions
+(defcustom isa-keywords-goal
+  '("goal" "goalw" "goalw_cterm" "Goal")
+  "Isabelle commands to begin an interactive proof"
+  :group 'isa-syntax
+  :type '(repeat string))
+
+(defcustom isa-keywords-save
+  '("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
+(defcustom isa-keywords-commands
+  '("by" "goal")
+  "Isabelle command keywords"
+  :group 'isa-syntax
+  :type '(repeat string))
+
+;; 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"))
+
+(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 Isabelle script")
+
+(defvar isa-tacticals '("REPEAT" "THEN" "ORELSE" "TRY"))
+
+;; ----- regular expressions
+
+;; this should come from isa-ml-compiler stuff.
+(defcustom isa-error-regexp 
+  "^.*Error:"
+  "A regexp indicating that Isabelle has identified an error."
+  :type 'string
+  :group 'isa-syntax)
+
+(defvar isa-id proof-id)
+
+(defvar isa-ids (proof-ids isa-id))
+
+(defun isa-abstr-regexp (paren char)
+    (concat paren "\\s-*\\(" isa-ids "\\)\\s-*" char))
+
+(defvar isa-font-lock-terms
+  (list
+   ;; lambda binders
+   (list (isa-abstr-regexp "\\[" ":") 1 'font-lock-declaration-name-face)
+
+   ;; Pi binders
+   (list (isa-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face)
+   
+   ;; Kinds
+   (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\(("
+		   isa-id ")\\)?") 'font-lock-type-face))
+  "*Font-lock table for Isa terms.")
+
+(defconst isa-save-command-regexp
+  (concat "^" (ids-to-regexp isa-keywords-save)))
+(defconst isa-save-with-hole-regexp
+  (concat "\\(" (ids-to-regexp isa-keywords-save)
+	  "\\)\\s-+\\(" isa-id "\\)\\s-*\."))
+(defconst isa-goal-command-regexp
+  (concat "^" (ids-to-regexp isa-keywords-goal)))
+(defconst isa-goal-with-hole-regexp
+  (concat "\\(" (ids-to-regexp isa-keywords-goal)
+	  "\\)\\s-+\\(" isa-id "\\)\\s-*:"))
+(defconst isa-decl-with-hole-regexp
+  (concat "\\(" (ids-to-regexp isa-keywords-decl)
+	  "\\)\\s-+\\(" isa-ids "\\)\\s-*:"))
+(defconst isa-defn-with-hole-regexp
+  (concat "\\(" (ids-to-regexp isa-keywords-defn)
+	  "\\)\\s-+\\(" isa-id "\\)\\s-*[:[]"))
+
+(defvar isa-font-lock-keywords-1
+   (append
+    isa-font-lock-terms
+    (list
+     (cons (ids-to-regexp isa-keywords) 'font-lock-keyword-face)
+     (cons (ids-to-regexp isa-tacticals) 'font-lock-tacticals-name-face)
+
+     (list isa-goal-with-hole-regexp 2 'font-lock-function-name-face)
+     (list isa-decl-with-hole-regexp 2 'font-lock-declaration-name-face)
+     (list isa-defn-with-hole-regexp 2 'font-lock-function-name-face)
+     (list isa-save-with-hole-regexp 2 'font-lock-function-name-face))))
+
+(provide 'isa-syntax)
diff --git a/isa/isa.el b/isa/isa.el
new file mode 100644
index 00000000..1fa429bd
--- /dev/null
+++ b/isa/isa.el
@@ -0,0 +1,366 @@
+;; isa.el Major mode for Isabelle proof assistant
+;; Copyright (C) 1994-1998 LFCS Edinburgh. 
+;; Author: David Aspinall
+
+;; $Id$
+;;
+
+
+(require 'isa-syntax)
+(require 'outline)
+(require 'proof)
+
+
+;;;
+;;; ======== User settings for Isabelle ========
+;;;
+
+(defgroup isabelle-settings nil
+  "Customization of Isabelle specifics for proof mode."
+  :group 'proof)
+  
+(defcustom isa-prog-name "/usr/lib/Isabelle98/bin/isabelle"
+  "*Name of program to run Isabelle."
+  :type 'file
+  :group 'isabelle-settings)
+
+(defcustom isa-thy-file-tags-table "/usr/lib/Isabelle98/src/TAGS.thy"
+  "*Name of theory file tags table for Isabelle."
+  :type 'file
+  :group 'isabelle-settings)
+
+(defcustom isa-ML-file-tags-table  "/usr/lib/Isabelle98/src/TAGS.ML"
+  "*Name of ML file tags table for Isabelle."
+  :type 'file
+  :group 'isabelle-settings)
+
+(defcustom isa-indent 2
+  "*Indentation degree in proof scripts.
+Utterly irrelevant for Isabelle because normal proof scripts have
+no regular or easily discernable structure."
+  :type 'number
+  :group 'isabelle-settings)
+
+(defcustom isa-www-home-page
+  ;; "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html"
+  "http://www.dcs.ed.ac.uk/home/isabelle"
+  "URL of home page for Isabelle."
+  :type 'string
+  :group 'isabelle-settings)
+  
+  
+  
+
+;;;
+;;; ======== Configuration of generic modes ========
+;;;
+
+(defvar isa-mode-config-table
+  '(;; general
+    (proof-assistant		"Isabelle")
+    (proof-www-home-page	isa-www-home-page)
+    ;; 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 ; could be version 
+     "print \" 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		isa-goal-regexp)    ; 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.")
+
+
+;; ===== outline mode
+
+;;; FIXME: test and add more things here
+(defvar isa-outline-regexp
+  (ids-to-regexp '("goal" "Goal" "prove_goal"))
+  "Outline regexp for Isabelle ML files")
+
+;;; End of a command needs parsing to find, so this is approximate.
+(defvar isa-outline-heading-end-regexp ";[ \t\n]*")
+
+(defconst isa-goal-regexp "^[ \t]*[0-9]+\\. "
+  "Regexp to match subgoal headings.
+Used by proof mode to parse proofstate output, and also
+to set outline heading regexp.")
+  
+;; 
+(defvar isa-shell-outline-regexp isa-goal-regexp)
+(defvar isa-shell-outline-heading-end-regexp isa-goal-regexp)
+
+;;; ---- end-outline
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   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))
+
+(define-derived-mode isa-mode proof-mode
+   "isa" "Isabelle Mode"
+   (isa-mode-config))
+
+(define-derived-mode isa-pbp-mode pbp-mode
+  "pbp" "Proof-by-pointing support for Isabelle"
+  (isa-pbp-mode-config))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Code that's Isabelle specific                                  ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+;; 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))
+	     (isa-goal-command-p
+	      (span-property (prev-span span 'type) 'cmd)))
+	(concat "choplev 0" proof-terminal-string)
+      (while span
+	(setq str (span-property span 'cmd))
+	(cond ((eq (span-property span 'type) 'vanilla)
+	       (or (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 (string-match isa-not-undoable-commands-regexp str))
+		      (setq i 0)
+		      (while (< i (length str))
+			(if (= (aref str i) proof-terminal-char)
+			    (setq ct (+ 1 ct)))
+			(setq i (+ 1 i))))
+		     (t nil))))
+	(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-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)))
+
+       ((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))
+	     (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")))
+
+(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."
+  (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)
+  nil)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Indentation                                                    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;;
+;; 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
+   ((null stack) 0)
+   ((null (car (car stack)))
+    (nth 1 (car stack)))
+   (t (save-excursion
+	(goto-char (nth 1 (car stack)))
+	(+ isa-indent (current-column))))))
+
+(defun isa-parse-indent (c 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))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Configuring proof and pbp mode and setting up various utilities  ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun isa-init-syntax-table ()
+  "Set appropriate values for syntax table in current buffer."
+  (modify-syntax-entry ?\$ ".")
+  (modify-syntax-entry ?\/ ".")
+  (modify-syntax-entry ?\\ ".")
+  (modify-syntax-entry ?+  ".")
+  (modify-syntax-entry ?-  ".")
+  (modify-syntax-entry ?=  ".")
+  (modify-syntax-entry ?%  ".")
+  (modify-syntax-entry ?<  ".")
+  (modify-syntax-entry ?>  ".")
+  (modify-syntax-entry ?\& ".")
+  (modify-syntax-entry ?_  "_")
+  (modify-syntax-entry ?\' "_")
+  (modify-syntax-entry ?\| ".")
+  (modify-syntax-entry ?\* ". 23")
+  (modify-syntax-entry ?\( "()1")
+  (modify-syntax-entry ?\) ")(4"))
+
+(defun isa-mode-config ()
+  (mapcar (lambda (symval) (apply 'set symval)) isa-mode-config-table)
+  (isa-init-syntax-table)
+  ;; 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
+  ;; 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 '(("\\.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-pre-shell-start-hook 'isa-pre-shell-start nil t))
+
+
+(defun isa-shell-mode-config ()
+  ;; 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))
+
+(provide 'isa)