Renamed for new subdirectory structure

16 files changed, 9 insertions, 651 deletions

diff --git a/coq-syntax.el b/coq/coq-syntax.el
index b81a93e8..55d68f35 100644
--- a/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -4,6 +4,9 @@
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 
 ;; $Log$
+;; Revision 1.1  1998/09/03 13:51:13  da
+;; Renamed for new subdirectory structure
+;;
 ;; Revision 2.0  1998/08/11 14:59:53  da
 ;; New branch
 ;;
diff --git a/coq.el b/coq/coq.el
index 3a34ab19..3a34ab19 100644
--- a/coq.el
+++ b/coq/coq.el
diff --git a/coqtags b/coq/coqtags
index b6c72c78..b6c72c78 100644
--- a/coqtags
+++ b/coq/coqtags
diff --git a/script-management.texinfo b/doc/script-management.texinfo
index a7232b3c..a7232b3c 100644
--- a/script-management.texinfo
+++ b/doc/script-management.texinfo
diff --git a/pbp.el b/generic/pbp.el
index 23ffdd68..23ffdd68 100644
--- a/pbp.el
+++ b/generic/pbp.el
diff --git a/proof-indent.el b/generic/proof-indent.el
index bb42f462..bb42f462 100644
--- a/proof-indent.el
+++ b/generic/proof-indent.el
diff --git a/proof-syntax.el b/generic/proof-syntax.el
index 5caa8fe3..5caa8fe3 100644
--- a/proof-syntax.el
+++ b/generic/proof-syntax.el
diff --git a/proof.el b/generic/proof.el
index c37f863b..c37f863b 100644
--- a/proof.el
+++ b/generic/proof.el
diff --git a/span-extent.el b/generic/span-extent.el
index b49670b7..6e6183cd 100644
--- a/span-extent.el
+++ b/generic/span-extent.el
@@ -5,6 +5,9 @@
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 
 ;; $Log$
+;; Revision 1.1  1998/09/03 13:51:33  da
+;; Renamed for new subdirectory structure
+;;
 ;; Revision 2.0  1998/08/11 15:00:13  da
 ;; New branch
 ;;
diff --git a/span-overlay.el b/generic/span-overlay.el
index f74350ed..e67ad33c 100644
--- a/span-overlay.el
+++ b/generic/span-overlay.el
@@ -5,6 +5,9 @@
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 
 ;; $Log$
+;; Revision 1.1  1998/09/03 13:51:34  da
+;; Renamed for new subdirectory structure
+;;
 ;; Revision 2.0  1998/08/11 15:00:13  da
 ;; New branch
 ;;
diff --git a/isa-print-functions.ML b/isa-print-functions.ML
deleted file mode 100644
index 3af539a5..00000000
--- a/isa-print-functions.ML
+++ /dev/null
@@ -1,172 +0,0 @@
-(* 
-   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-syntax.el b/isa-syntax.el
deleted file mode 100644
index f7667127..00000000
--- a/isa-syntax.el
+++ /dev/null
@@ -1,138 +0,0 @@
-;; 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.
-
-(defvar isa-keywords-decl
-  '("val")
-  "Isabelle keywords for declarations")
-;  :group 'isa-syntax
-;  :type '(repeat string))
-
-(defvar isa-keywords-defn
-  '("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" "goalw" "goalw_cterm")
-  "Isabelle commands to begin an interactive proof")
-;  :group 'isa-syntax
-;  :type '(repeat string))
-
-(defvar 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
-(defvar isa-keywords-commands
-  '("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"))
-
-(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.
-(defvar isa-error-regexp 
-  "^.*Error:"
-  "A regular expression indicating that the Isa process has identified
-  an error.")
-
-(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.el b/isa.el
deleted file mode 100644
index ccecdfaa..00000000
--- a/isa.el
+++ /dev/null
@@ -1,341 +0,0 @@
-;; 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 ========
-;;;
-
-(defvar isa-prog-name "/usr/lib/Isabelle98/bin/isabelle"
-  "*Name of program to run Isabelle.")
-
-(defvar isa-thy-file-tags-table "/usr/lib/Isabelle98/src/TAGS.thy"
-  "*Name of theory file tags table for Isabelle.")
-
-(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 ; 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		"^[ \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.")
-
-
-;; ===== 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]*")
-
-;; 
-(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 ()
-  (apply 'setq 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)
diff --git a/lego-syntax.el b/lego/lego-syntax.el
index 60ede04f..60ede04f 100644
--- a/lego-syntax.el
+++ b/lego/lego-syntax.el
diff --git a/lego.el b/lego/lego.el
index 30a1e389..30a1e389 100644
--- a/lego.el
+++ b/lego/lego.el
diff --git a/legotags b/lego/legotags
index a3c13eab..a3c13eab 100644
--- a/legotags
+++ b/lego/legotags