Deleted file

14 files changed, 0 insertions, 3531 deletions

diff --git a/isa/BUGS b/isa/BUGS
deleted file mode 100644
index 41f992c3..00000000
--- a/isa/BUGS
+++ /dev/null
@@ -1,68 +0,0 @@
--*- mode:outline -*-
-
-* Isabelle Proof General Bugs
-
-See also ../BUGS for generic bugs.
-
-See also ../isar/BUGS.  Isar is now main the instance for 
-Isabelle PG, the original Isabelle instance less supported.
-
-
-** Issues with tracing mode 
-
-1. Large volumes of output can cause Emacs to hog CPU spending
-all its time processing the output (esp with fontifying and X-symbol
-decoding).   It becomes difficult to use normal editing commands,
-even C-c C-c to interrupt the prover.  Workaround: hitting C-g,
-the Emacs quit key, will interrupt the prover in this state.
-See manual for further description of this.
-
-2. Interrupt response may be lost in large volumes of output, when
-using pty communication.  Symptom is interrupt on C-g, but PG thinks
-the prover is still busy.  Workaround: hit return in the shell buffer,
-or set proof-shell-process-connection-type to nil to use piped
-communication.
-
-** set proof_timing is problematic
-
-It will make the goals display disappear during proof.  This is
-because Proof General only displays goals output that appears *after*
-Isabelle messages, but Isabelle prints the timing message after the
-goals are displayed.
-
-** General difficulty with proof scripts containing ML structures, etc.  
-
-Proof General does not understand full ML syntax(!), so it will be
-confused by structures which contain semi-colons after declarations,
-for example.  Also, it cannot undo function declarations.  See the
-section on ML files in the manual for more details.
-
-** Blocking when processing multiple files, beginning from a .ML file.
-
-Proof General will block the Emacs process when it is waiting for a
-theory file (and it's ancestors) to be read as scripting is turned on.
-To avoid this, assert the theory file rather than the ML file.
-
-** Subsection Interaction with theory database
-
-Isabelle Proof General uses some support from Isabelle to remove and
-reload theories from the theory database.  To maintain consistency,
-Isabelle is rather conservative.  So re-asserting a retracted file will
-often re-load it, even if it has not changed.  (This is because the
-file may have implicit dependencies on things in the global ML
-environment not made apparent by the theory structure).  
-This may lead to seemingly unnecessary repetition of time-consuming
-proofs, so be careful not to retract more than you need!
-
-As of Isabelle 99-1 and Proof General 3.2, there should be much
-less unncessary re-loading of theories; be careful to use Isabelle's
-mechanisms of declaring dependencies in theory file headers.
-
-** Clash with SML mode
-
-Since Isabelle proof scripts are not differentiated from `.ML' files,
-Proof General may compete with `sml-mode' (if you use it) for
-controlling these buffers.  To ensure Proof General wins, load it last.
-
-Workaround: use another extension for real ML files, e.g.  `.sml',
-and disable `.ML' from entering `sml-mode'.
diff --git a/isa/Example-Xsym.ML b/isa/Example-Xsym.ML
deleted file mode 100644
index ed97c291..00000000
--- a/isa/Example-Xsym.ML
+++ /dev/null
@@ -1,20 +0,0 @@
-(*
-    Example proof script for Isabelle Proof General.
-
-    $Id$
-
-    Just a version of Example.ML using XSymbol.
-
-    Also subscripts/superscripts:  A\<^sup>1 \\<or> A\<^sub>2
-    [NB: these can't be used in identifiers or otherwise
-     parsed by Isabelle unless declared as part of a theory's 
-     concrete syntax, see docs or examples in HOL/IMP.]
-*)    
-
-Goal "A \\<and> B \\<longrightarrow> B \\<and> A";
-by (rtac impI 1);
-by (etac conjE 1);
-by (rtac conjI 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "and_comms";
diff --git a/isa/Example.ML b/isa/Example.ML
deleted file mode 100644
index 57733a48..00000000
--- a/isa/Example.ML
+++ /dev/null
@@ -1,18 +0,0 @@
-(*  -*- isa -*-
-
-    Example proof script for Isabelle Proof General.
-
-    $Id$
-
-    The line at the top of this comment forces 
-    Proof General's classic Isabelle mode
-    (instead of Isar: you can't use both at once).
-*)
-
-Goal "A & B --> B & A";
-  by (rtac impI 1);
-  by (etac conjE 1);
-  by (rtac conjI 1);
-  by (assume_tac 1);
-  by (assume_tac 1);
-qed "and_comms";
diff --git a/isa/Example.thy b/isa/Example.thy
deleted file mode 100644
index ba64d959..00000000
--- a/isa/Example.thy
+++ /dev/null
@@ -1,20 +0,0 @@
-(*  -*- isa -*- 
-
-    Example theory file for Isabelle
-
-    David Aspinall <da@dcs.ed.ac.uk>
-
-    $Id$
-
-    The line at the top of this comment forces 
-    Proof General's classic Isabelle mode;
-    scripting takes place in .ML files.
-
-    NB: this is incompatible with ProofGeneral/Isar which is
-    a separate instance of Proof General.
-
-    See the PG manual for ways to select Isabelle/Classic
-    by default.
-*)
-
-Example = Main
diff --git a/isa/Example2.ML b/isa/Example2.ML
deleted file mode 100644
index ab2fef03..00000000
--- a/isa/Example2.ML
+++ /dev/null
@@ -1,15 +0,0 @@
-(*
-    Example proof script for Isabelle Proof General.
-
-    $Id$
-
-    Same as Example.ML, except using X-Symbol input tokens.
-*)
-
-Goal "A \\<and> B \\<longrightarrow> B \\<and> A";
-  by (rtac impI 1);
-  by (etac conjE 1);
-  by (rtac conjI 1);
-  by (assume_tac 1);
-  by (assume_tac 1);
-qed "and_comms";
diff --git a/isa/README b/isa/README
deleted file mode 100644
index 01490085..00000000
--- a/isa/README
+++ /dev/null
@@ -1,32 +0,0 @@
-Isabelle Proof General 
-
-Written by David Aspinall, later with assistance from
-Markus Wenzel and David von Oheimb.
-
-Status:		   supported 
-Maintainer:	   David Aspinall
-Isabelle versions: Isabelle2003, Isabelle2004
-Isabelle homepage: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
-
-====================================================================
-
-Isabelle Proof General has full support for multiple file scripting,
-with dependencies between theories communicated between Isabelle and
-Proof General.  It has a mode for editing theory files taken from
-Isamode.
-
-There is excellent support for X Symbol, using the Isabelle print mode
-for X Symbol tokens.  Many Isabelle theories have X Symbol syntax
-already defined and it's easy to add to your own theories.
-
-The script `interface' and file 'interface-setup.el' are used to start
-Isabelle Proof General via the 'Isabelle' shell command.  These files
-were provided by Markus Wenzel.
-
-Check the value of isabelle-prog-name.
-
-
-========================================
-
-$Id$
-
diff --git a/isa/interface-setup.el b/isa/interface-setup.el
deleted file mode 100644
index 16c167cc..00000000
--- a/isa/interface-setup.el
+++ /dev/null
@@ -1,43 +0,0 @@
-;; interface-setup.el Interface wrapper for Isabelle Proof General
-;;
-;; This file is free software; you can redistribute it and/or modify
-;; it under the terms of the GNU General Public License as published by
-;; the Free Software Foundation; either version 2, or (at your option)
-;; any later version.
-;;
-;; Author: Markus Wenzel <wenzelm@in.tum.de>
-;;
-;; interface-setup.el,v 7.0 2002/08/29 09:14:03 da Exp
-;;
-
-;;
-;; X-Symbol
-;;
-
-(let ((xsymbol (getenv "PROOFGENERAL_XSYMBOL"))
-      (enable-var (if (equal (getenv "PROOFGENERAL_ASSISTANTS") "isa")
-                      'isa-x-symbol-enable 'isar-x-symbol-enable)))
-
-  ;; avoid confusing warning message
-  (if (not (boundp 'x-symbol-image-converter))     
-      (customize-set-variable 'x-symbol-image-converter nil))
-  
-  ;; tell Proof General about -x option
-  (if (and xsymbol (not (equal xsymbol "")))
-      (customize-set-variable enable-var (equal xsymbol "true"))))
-
-
-;;
-;; Unicode
-;;
-
-(let ((unicode (getenv "PROOFGENERAL_UNICODE")))
-  (if (and unicode (not (equal unicode "")))
-      (customize-set-variable 'proof-shell-unicode (equal unicode "true"))))
-
-;;
-;; Proof General
-;;
-
-(if (not (featurep 'proof-site))
-    (load (concat (getenv "PROOFGENERAL_HOME") "/generic/proof-site.el")))
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
deleted file mode 100644
index 3ed6c53e..00000000
--- a/isa/isa-syntax.el
+++ /dev/null
@@ -1,352 +0,0 @@
-;; isa-syntax.el Syntax expressions for Isabelle
-;;
-;; Copyright (C) 1994-1998 LFCS Edinburgh. 
-;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;; Author:      David Aspinall <David.Aspinall@ed.ac.uk>
-;;
-;; $Id$
-;;
-;;
-(require 'proof-syntax)
-
-;; character syntax
-
-(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 ?.  "w")
-  (modify-syntax-entry ?_  "w")
-  (modify-syntax-entry ?\' "w")
-  (modify-syntax-entry ?\| ".")
-  (modify-syntax-entry ?\* ". 23")
-  (modify-syntax-entry ?\( "()1")
-  (modify-syntax-entry ?\) ")(4"))
-
-(defun isa-init-output-syntax-table ()
-  "Set appropriate values for syntax table for Isabelle output."
-  (isa-init-syntax-table)
-  ;; ignore strings so font-locking works
-  ;; inside them
-  (modify-syntax-entry ?\" " ")
-  (modify-syntax-entry ?\* ".")
-  (modify-syntax-entry ?\( "()")
-  (modify-syntax-entry ?\) ")(")
-  (modify-syntax-entry ?\{ "(}")
-  (modify-syntax-entry ?\} "){"))
-
-;;
-;; Syntax for font-lock and other features
-;;
-
-;; 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:
-;;
-;;   val lemma = result() RS spec RS mp;
-;;
-;; Not recognized as a qed command, and therefore assumed 
-;; to be an undoable tactic command.
-;;
-
-(defgroup isa-syntax nil
-  "Customization of Isabelle syntax for proof mode"
-  :group 'isa-settings)
-
-(defcustom isa-keywords-defn
-  '("bind_thm" "bind_thms")
-  "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" "goal" "goalw" "goalw_cterm" "atomic_goal" "atomic_goalw")
-  "Isabelle commands to begin an interactive proof"
-  :group 'isa-syntax
-  :type '(repeat string))
-
-(defcustom isa-keywords-save
-  '("qed" "qed_spec_mp" "no_qed")
-  ;; Related commands, but having different types, so PG
-  ;; won't bother support them:
-  ;; "uresult" "bind_thm" "store_thm"
-    "Isabelle commands to extract the proved theorem"
-  :group 'isa-syntax
-  :type '(repeat string))
-
-(defcustom isa-keywords-commands
-  '("by" "byev"
-    "ba" "br" "be" "bd" "brs" "bes" "bds"
-    "chop" "choplev" "back" "undo" "ProofGeneral.repeat_undo"
-    "fa" "fr" "fe" "fd" "frs" "fes" "fds"
-    "bw" "bws" "ren"
-    ;; batch proofs
-    "prove_goal" "qed_goal" "prove_goalw" "qed_goalw" "prove_goalw_cterm")
-  "Isabelle command keywords"
-  :group 'isa-syntax
-  :type '(repeat string))
-
-(defcustom isa-keywords-sml
-  '("abstype" "and" "andalso" "as" "case" "datatype" "do" "else" "end"
-    "eqtype" "exception" "fn" "fun" "functor" "handle" "if" "in" "include"
-    "infix" "infixr" "let" "local" "nonfix" "of" "op" "open" "orelse"
-    "raise" "rec" "sharing" "sig" "signature" "struct" "structure" "then"
-    "type" "val" "while" "with" "withtype")
-    "Standard ML keywords that are nice to have coloured."
-  :group 'isa-syntax
-  :type '(repeat string))
-
-(defcustom isa-keyword-symbols
-  '("=" "=>" "|" ";" "," "(" ")" "-" "." "->" ":" "{" "}" "[" "]" "#")
-    "Symbols that are nice to have in bold."
-  :group 'isa-syntax
-  :type '(repeat string))
-
-(defcustom isa-sml-names-keywords
-  '("fun" "val" "structure" "signature" "functor")
-    "Keywords that then define a name."
-  :group 'isa-syntax
-  :type '(repeat string))
-
-(defcustom isa-sml-typenames-keywords
-  '("type" "eqtype" "datatype")
-    "Keywords that define a type, this is only terminated by a '=' or '\n'."
-  :group 'isa-syntax
-  :type '(repeat string))
-
-
-;; NB: this means that any adjustments above by customize will
-;; only have effect in next session.
-(defconst isa-keywords
-  (append isa-keywords-goal isa-keywords-save
-	  isa-keywords-defn isa-keywords-commands 
-          isa-keywords-sml)
-  "All keywords in a Isabelle script")
-
-(defconst isa-keywords-proof-commands
-  (append isa-keywords-goal isa-keywords-save isa-keywords-commands)
-  "Actual Isabelle proof script commands")
-
-;; The most common Isabelle/Pure tacticals
-(defconst isa-tacticals
-  '("ALLGOALS" "DETERM" "EVERY" "EVERY'" "FIRST" "FIRST'" "FIRSTGOAL"
-    "ORELSE" "ORELSE'" "REPEAT" "REPEAT" "REPEAT1" "REPEAT_FIRST"
-    "REPEAT_SOME" "SELECT_GOAL" "SOMEGOAL" "THEN" "THEN'" "TRY" "TRYALL"))
-
-
-;; ----- regular expressions
-
-(defconst isa-id "\\([A-Za-z][A-Za-z0-9'_]*\\)")
-(defconst isa-idx (concat isa-id "\\(\\.[0-9]+\\)?"))
-
-(defconst isa-ids (proof-ids isa-id "[ \t]*")
-  "Matches a sequence of identifiers separated by whitespace.")
-
-(defconst isa-string "\"\\(\\([^\\\"]\\|\\\\\"\\)*\\)\"")
-
-(defcustom isa-save-command-regexp
-  (proof-regexp-alt
-   (proof-anchor-regexp (proof-ids-to-regexp isa-keywords-save))
-   ;; match val ... = result blah
-   (proof-anchor-regexp
-    (concat
-     (proof-ids-to-regexp '("val")) ".+=\\s-*"
-     "\\(" (proof-ids-to-regexp isa-keywords-save) "\\)")))
-  "Regular expression used to match a qed/result."
-  :type 'regexp
-  :group 'isabelle-config)
-
-
-;; CHECKED
-(defconst isa-save-with-hole-regexp
-  (concat "\\(" (proof-ids-to-regexp isa-keywords-save)
-	  "\\)\\s-+\"\\(" isa-id "\\)\"\\s-*;"))
-
-(defcustom isa-goal-command-regexp
-  (proof-regexp-alt
-   (proof-anchor-regexp (proof-ids-to-regexp isa-keywords-goal))
-   ;; match val ... = goal blah
-   (proof-anchor-regexp
-    (concat
-     (proof-ids-to-regexp '("val")) ".+=\\s-*"
-     "\\(" (proof-ids-to-regexp isa-keywords-goal) "\\)")))
-  "Regular expression used to match a goal."
-  :type 'regexp
-  :group 'isabelle-config)
-
-(defconst isa-string-regexp
-  (concat "\\s-*\"\\(" isa-id "\\)\"\\s-*")
-  "Regexp matching ML strings, with contents bracketed.")
-
-(defconst isa-goal-with-hole-regexp
-  (concat "\\("
-	  ;; Don't bother with "val xxx = prove_goal blah".
-	  (proof-ids-to-regexp '("qed_goal"))
-	  "\\)" isa-string-regexp)
-  "Regexp matching goal commands in Isabelle which name a theorem")
-
-
-(defconst isa-proof-command-regexp
-  (proof-ids-to-regexp isa-keywords-proof-commands)
-  "Regexp to match proof commands, with no extra output (apart from proof state)")
-
-
-;; ----- Isabelle inner syntax hilite
-
-(defface isabelle-class-name-face
-  '((((type x) (class color) (background light))   
-     (:foreground "red"))
-    (((type x) (class color) (background dark))   
-     (:foreground "red3"))
-    (t				
-     (bold t)))
-  "*Face for Isabelle term / type hiliting"
-  :group 'proof-faces)
-
-(defface isabelle-tfree-name-face
-  '((((type x) (class color) (background light))   
-     (:foreground "purple"))
-    (((type x) (class color) (background dark))   
-     (:foreground "purple3"))
-    (t
-     (bold t)))
-  "*Face for Isabelle term / type hiliting"
-  :group 'proof-faces)
-
-(defface isabelle-tvar-name-face
-  '((((type x) (class color) (background light))   
-     (:foreground "purple"))
-    (((type x) (class color) (background dark))   
-     (:foreground "purple3"))
-    (t				
-     (bold t)))
-  "*Face for Isabelle term / type hiliting"
-  :group 'proof-faces)
-
-(defface isabelle-free-name-face
-  '((((type x) (class color) (background light))   
-     (:foreground "blue"))
-    (((type x) (class color) (background dark))   
-     (:foreground "blue3"))
-    (t				
-     (bold t)))
-  "*Face for Isabelle term / type hiliting"
-  :group 'proof-faces)
-
-(defface isabelle-bound-name-face
-  '((((type x) (class color) (background light))   
-     (:foreground "green4"))
-    (((type x) (class color) (background dark))   
-     (:foreground "green"))
-    (t				
-     (bold t)))
-  "*Face for Isabelle term / type hiliting"
-  :group 'proof-faces)
-
-(defface isabelle-var-name-face
-  '((((type x) (class color) (background light))   
-     (:foreground "darkblue"))
-    (((type x) (class color) (background dark))   
-     (:foreground "blue3"))
-    (t				
-     (bold t)))
-  "*Face for Isabelle term / type hiliting"
-  :group 'proof-faces)
-
-;; special face for key symbols, make them bold
-(defface isabelle-sml-symbol-face
-  '((((class color) (background dark)) (:bold t))
-    (((class color) (background light)) (:bold t))
-    (((class grayscale) (background light)) (:bold t))
-    (((class grayscale) (background dark)) (:bold t))
-    (t (:bold t)))
-  "*SML symbol/character highlightling face"
-  :group 'proof-faces)
-
-;; GNU Emacs compatibility for above faces.
-(defconst isabelle-class-name-face 'isabelle-class-name-face)
-(defconst isabelle-tfree-name-face 'isabelle-tfree-name-face)
-(defconst isabelle-tvar-name-face 'isabelle-tvar-name-face)
-(defconst isabelle-free-name-face 'isabelle-free-name-face)
-(defconst isabelle-bound-name-face 'isabelle-bound-name-face)
-(defconst isabelle-var-name-face 'isabelle-var-name-face)
-(defconst isabelle-sml-symbol-face 'isabelle-sml-symbol-face)
-
-;; regexp for finding function/variable/struct/sig/functor names
-(defconst isa-sml-function-var-names-regexp 
-  (concat "\\(" (proof-ids-to-regexp isa-sml-names-keywords) "\\)[\ \t]*\\(" isa-id "\\)"))
-
-;; regexp for finding type names, note that types may be compound, 
-;; thus this needs to be separate from function names
-(defconst isa-sml-type-names-regexp 
-  (concat "\\(" (proof-ids-to-regexp isa-sml-typenames-keywords) "\\)\\([^\n=]*\\)[\n=]"))
-
-;; make stuff to be syntax colourd....
-(defvar isa-font-lock-keywords-1
-  (list
-   (cons (proof-ids-to-regexp isa-keywords) 'font-lock-keyword-face)
-   (cons (regexp-opt isa-keyword-symbols) 'isabelle-sml-symbol-face)
-   (list isa-sml-function-var-names-regexp 2 'font-lock-function-name-face 'append' t)
-   (list isa-sml-type-names-regexp 2 'font-lock-function-name-face 'append' t)
-   (cons (proof-ids-to-regexp isa-tacticals) 'proof-tacticals-name-face)
-   (list isa-goal-with-hole-regexp 2 'font-lock-function-name-face)
-   (list isa-save-with-hole-regexp 2 'font-lock-function-name-face)))
-
-(defvar isa-output-font-lock-keywords-1
-  (list
-   (cons (concat "\351" isa-id "\350") 'isabelle-class-name-face)
-   (cons (concat "\352'" isa-id "\350") 'isabelle-tfree-name-face)
-   (cons (concat "\353\\?'" isa-idx "\350") 'isabelle-tvar-name-face)
-   (cons (concat "\354" isa-id "\350") 'isabelle-free-name-face)
-   (cons (concat "\355" isa-id "\350") 'isabelle-bound-name-face)
-   (cons (concat "\356\\?" isa-idx "\350") 'isabelle-var-name-face)
-   (cons (concat "\357\\?" isa-idx "\350") 'proof-declaration-name-face)
-   )
-  "*Font-lock table for Isabelle terms.")
-
-(defvar isa-goals-font-lock-keywords 
-  (append
-   (list 
-    "^Level [0-9].*"
-    "^No subgoals!$"
-    "^Variables:$"
-    "^Constants:$"
-    "\\s-*[0-9][0-9]?\\. ")
-   isa-output-font-lock-keywords-1)
-  "*Font-lock table for Isabelle goals output.")
-
-
-;; ----- indentation
-
-(defconst isa-indent-any-regexp
-  (proof-regexp-alt (proof-ids-to-regexp isa-keywords) "\\s(" "\\s)"))
-(defconst isa-indent-inner-regexp
-  (proof-regexp-alt "\\s(" "\\s)"))
-(defconst isa-indent-enclose-regexp
-  (proof-ids-to-regexp isa-keywords-save))
-(defconst isa-indent-open-regexp
-  (proof-regexp-alt (proof-ids-to-regexp isa-keywords-goal) "\\s("))
-(defconst isa-indent-close-regexp
-  (proof-regexp-alt (proof-ids-to-regexp isa-keywords-save) "\\s)"))
-
-(provide 'isa-syntax)
diff --git a/isa/isa.el b/isa/isa.el
deleted file mode 100644
index 22b68642..00000000
--- a/isa/isa.el
+++ /dev/null
@@ -1,723 +0,0 @@
-; isa-mode.el	 Emacs support for Isabelle proof assistant
-;; Copyright (C) 1993-2000 LFCS Edinburgh, David Aspinall.
-;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
-;;
-;; $Id$
-;;
-;; -----------------------------------------------------------------
-;;
-;; This file and the rest of Isabelle Proof General contain code taken
-;; from David Aspinall's Isamode system, a personal project undertaken
-;; 1993-1999 as a contribution to the Isabelle community.
-;;
-;; -----------------------------------------------------------------
-
-
-;; In case Isa mode was invoked directly or by -*- isa -*- at
-;; the start of the file, ensure that Isa mode is used from now
-;; on for .thy and .ML files.  
-;; FIXME: be less messy with auto-mode-alist here (remove dups)
-(setq auto-mode-alist 
-      (cons '("\\.ML$\\|\\.thy$" . isa-mode) auto-mode-alist))
-
-(require 'proof)
-(require 'isa-syntax)
-(require 'isabelle-system)
-
-;;;
-;;; ======== User settings for Isabelle ========
-;;;
-
-;;; proof-site provides us with the cusomization groups
-;;;
-;;; 'isabelle         -  User options for Isabelle Proof General
-;;; 'isabelle-config  -  Configuration of Isabelle Proof General
-;;;			 (constants, but may be nice to tweak)
-
-
-;;;
-;;; ======== Configuration of generic modes ========
-;;;
-
-(defcustom isa-outline-regexp
-  (proof-ids-to-regexp '("goal" "Goal" "prove_goal"))
-  "Outline regexp for Isabelle ML files"
-  :type 'regexp
-  :group 'isabelle-config)
-
-;;; End of a command needs parsing to find, so this is approximate.
-(defcustom isa-outline-heading-end-regexp ";[ \t\n]*"
-  "Outline heading end regexp for Isabelle ML files."
-  :type 'regexp
-  :group 'isabelle-config)
-
-(defvar isa-shell-outline-regexp "\370[ \t]*\\([0-9]+\\)\\.")
-(defvar isa-shell-outline-heading-end-regexp "$")
-
-
-(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
-and script mode."
-  (setq
-   proof-assistant-home-page	isabelle-web-page
-   proof-mode-for-script	'isa-proofscript-mode
-   ;; proof script syntax
-   proof-terminal-char		?\;	; ends a proof
-   proof-script-comment-start		"(*"	; comment in a proof
-   proof-script-comment-end		"*)"	; 
-   ;; Next few used for func-menu and recognizing goal..save regions in
-   ;; script buffer.
-   proof-save-command-regexp    isa-save-command-regexp
-   proof-goal-command-regexp    isa-goal-command-regexp
-   proof-goal-with-hole-regexp  isa-goal-with-hole-regexp 
-   proof-save-with-hole-regexp  isa-save-with-hole-regexp
-   ;; Unfortunately the default value of proof-script-next-entity-regexps
-   ;; is no good, because goals with holes in Isabelle are batch
-   ;; commands, and not terminated by saves.  So we omit the forward
-   ;; search from the default value.
-   proof-script-next-entity-regexps
-   (list (proof-regexp-alt
-	  isa-goal-with-hole-regexp
-	  isa-save-with-hole-regexp)
-	 (list isa-goal-with-hole-regexp 2)
-	 (list isa-save-with-hole-regexp 2
-	       'backward isa-goal-command-regexp))
-
-   proof-indent-enclose-offset  (- proof-indent)
-   proof-indent-open-offset     0
-   proof-indent-close-offset    0
-   proof-indent-any-regexp      isa-indent-any-regexp
-   proof-indent-inner-regexp    isa-indent-inner-regexp
-   proof-indent-enclose-regexp  isa-indent-enclose-regexp
-   proof-indent-open-regexp     isa-indent-open-regexp
-   proof-indent-close-regexp    isa-indent-close-regexp
-   
-   ;; proof engine commands
-   proof-showproof-command	"pr();"
-   proof-goal-command		"Goal \"%s\";"
-   proof-save-command		"qed \"%s\";"
-   proof-context-command	"ProofGeneral.show_context();"
-   proof-info-command		"ProofGeneral.help();"
-   proof-kill-goal-command	"ProofGeneral.kill_goal();"
-   proof-find-theorems-command  "ProofGeneral.thms_containing (space_explode \",\" \"%s\");"
-   proof-shell-start-silent-cmd "Goals.disable_pr();"
-   proof-shell-stop-silent-cmd  "Goals.enable_pr();"
-   ;; 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-state-preserving-p	'isa-state-preserving-p
-
-   ;; close goal..save regions eagerly
-   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\";"
-
-   ;; span menu 
-   proof-script-span-context-menu-extensions 'isabelle-create-span-menu
-
-   ;; Parsing error messages.  Bit tricky to allow for
-   ;; multitude of possible error formats Isabelle spits out.
-   ;; Ideally we shouldn't bother parsing errors that appear
-   ;; in the temporary ML files generated while reading
-   ;; theories, but unfortunately the user sometimes needs to 
-   ;; examine them to understand a strange problem...
-   pg-next-error-regexp
-   "\\(error on \\|Error: in '[^']+', \\)line \\([0-9]+\\)\\|The error(s) above occurred"
-   pg-next-error-filename-regexp
-   "\\(Loading theory \"\\|Error: in '\\)\\([^\"']+\\)[\"']"
-   pg-next-error-extract-filename
-   "%s.thy"))
-
-  
-
-
-(defun isa-shell-mode-config-set-variables ()
-  "Configure generic proof shell mode variables for Isabelle."
-  (setq
-   pg-subterm-first-special-char	?\350
-
-   proof-shell-wakeup-char		 ?\372
-   proof-shell-annotated-prompt-regexp   "\\(val it = () : unit\n\\)?> \372"
-
-   ;; This pattern is just for comint
-   proof-shell-prompt-pattern		"^2?[ML-=#>]>? \372?"
-
-   ;; for issuing command, not used to track cwd in any way.
-   proof-shell-cd-cmd			"ThyLoad.add_path \"%s\";"
-
-   ;; Escapes for filenames inside ML strings.
-   ;; We also make a hack for Isabelle, by switching from backslashes
-   ;; to forward slashes if it looks like we're running on Windows.
-   proof-shell-filename-escapes		
-   (if (fboundp 'win32-long-file-name)	; rough test for XEmacs on win32 
-       ;; Patterns to unixfy names.  Avoids a deliberate bomb in Isabelle which
-       ;; barfs at paths with these characters in them.
-       '(("\\\\" . "/") ("\"" . "\\\"") ("^[a-zA-Z]:" . ""))
-     ;; Normal case: quotation for backslash, quote mark.
-     '(("\\\\" . "\\\\") ("\""   . "\\\"")))
-
-   proof-shell-interrupt-regexp         "Interrupt"
-   proof-shell-error-regexp		"^\364\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception-\\( \\|$\\)"
-   
-   ;; matches names of assumptions
-   proof-shell-assumption-regexp	isa-id
-   ;; matches subgoal name
-   ;; FIXME: not used yet.  In future will be used for
-   ;; proof-by-pointing like features.
-   ;; proof-shell-goal-regexp		"\370[ \t]*\\([0-9]+\\)\\."
-
-   proof-shell-start-goals-regexp	"\366"
-   proof-shell-end-goals-regexp		"\367"
-   pg-topterm-char	        ?\370
-
-   proof-shell-proof-completed-regexp	"^No subgoals!"
-
-   ;; initial command configures Isabelle by hacking print functions,
-   ;; restoring settings saved by Proof General, etc.
-
-   proof-shell-pre-sync-init-cmd	"ProofGeneral.init false;"
-   proof-shell-init-cmd		        nil
-
-   proof-shell-restart-cmd		"ProofGeneral.isa_restart();"
-   proof-shell-quit-cmd			"quit();"
-
-   ;; NB: settings below only recognize tracing output in Isabelle2002
-   proof-shell-eager-annotation-start   "\360\\|\362"
-   proof-shell-eager-annotation-start-length 1
-   proof-shell-eager-annotation-end     "\361\\|\363"
-   ;; see isa-pre-shell-start for proof-shell-trace-output-regexp
-
-   ;; Isabelle is learning to talk PGIP...
-   proof-shell-match-pgip-cmd		"<pgip"
-   proof-shell-issue-pgip-cmd		
-	(if isa-supports-pgip 'isabelle-process-pgip nil)
-
-   ;; Some messages delimited by eager annotations
-   proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
-   proof-shell-clear-goals-regexp       "Proof General, please clear the goals buffer."
-   proof-shell-set-elisp-variable-regexp "Proof General, please set the variable \\([^ ]+\\) to: #\\([^#]+\\)#\\."
-
-   ;; Theorem dependencies.   NB: next regex anchored at end with eager annot end
-   proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\361"
-   proof-shell-theorem-dependency-list-split "\" \""
-   proof-shell-show-dependency-cmd "thm %s;"
-   
-   ;; Dirty hack to allow font-locking for output based on hidden
-   ;; annotations, see isa-output-font-lock-keywords-1
-   pg-use-specials-for-fontify t
-
-   ;; === ANNOTATIONS  === ones here are broken
-   proof-shell-result-start	        "\372 Pbp result \373"
-   proof-shell-result-end		"\372 End Pbp result \373"
-   pg-subterm-anns-use-stack		t
-   pg-subterm-start-char		?\372
-   pg-subterm-sep-char			?\373
-   pg-subterm-end-char			?\374
-   pg-after-fontify-output-hook		
-   (if proof-experimental-features 
-       'isabelle-convert-idmarkup-to-subterm 'pg-remove-specials)
-   ;; FIXME: next one doesn't do the right thing, it always returns 'a
-   ;; since variables are out-of-scope.  Better would be to simply
-   ;; print the variable's kind.
-   pg-subterm-help-cmd			"printyp (type_of (read \"%s\"))"
-
-   ;; === MULTIPLE FILE HANDLING ===
-
-   ;; da: this next setting added for PG 3.5.  I think the theory
-   ;; loader changed at some point: originally this setting left as
-   ;; nil would have been okay.
-   proof-cannot-reopen-processed-files  t 
-   proof-shell-process-file 
-   (cons
-    ;; Theory loader output and verbose update() output.
-    "Proof General, this file is loaded: \"\\(.*\\)\""
-    (lambda (str)
-      (match-string 1 str)))
-   ;; This is the output returned by a special command to
-   ;; query Isabelle for outdated files.
-   ;;   proof-shell-clear-included-files-regexp
-   ;;   "Proof General, please clear your record of loaded files."
-   proof-shell-retract-files-regexp
-   "Proof General, you can unlock the file \"\\(.*\\)\""
-   proof-shell-compute-new-files-list 'isa-shell-compute-new-files-list
-   )
-  (add-hook 'proof-activate-scripting-hook 'isa-shell-update-thy 'append)
-  )
-
-
-;;;
-;;; Theory loader operations
-;;;
-
-;; Experiments for background non-blocking loading of theory: this is
-;; 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.
-
-; attempt to trap C-g.  Needs more work so revert to previous
-;(defun isa-update-thy-only (file try wait)
-;  "Tell Isabelle to update current buffer's theory, and all ancestors."
-;  ;; Trap interrupts from C-g during the update
-;  (condition-case err
-;      (proof-shell-invisible-command
-;       (format "ProofGeneral.%supdate_thy_only \"%s\";"
-;	       (if try "try_" "") (file-name-sans-extension file))
-;       wait)
-;    (t (message "Isabelle Proof General: error or interrupt during update theory...")
-;       (if proof-shell-busy
-;	   (proof-interrupt-process))
-;       (sit-for 1)
-;       (proof-deactivate-scripting)
-;       (if (cdr err) ;; quit is just (quit).  
-;	   (error (cdr err))))))
-
-(defun isa-update-thy-only (file try wait)
-  "Tell Isabelle to update current buffer's theory, and all ancestors."
-  ;; First make sure we're in the right directory to take care of
-  ;; relative "files" paths inside theory file.
-  (proof-cd-sync)
-  (proof-shell-invisible-command
-   (proof-format-filename
-    ;; %r parameter means relative (don't expand) path
-    (format "ProofGeneral.%supdate_thy_only \"%%r\";" (if try "try_" ""))
-    (file-name-nondirectory (file-name-sans-extension file)))
-   wait))
-
-(defun isa-shell-update-thy ()
-  "Possibly issue update_thy_only command to Isabelle.
-If the current buffer has an empty locked region, the interface is
-about to send commands from it to Isabelle.  This function sends
-a command to read any theory file corresponding to the current ML file.
-This is a hook function for proof-activate-scripting-hook."
-  (if (proof-locked-region-empty-p)
-       ;; If we switch to this buffer and it *does* have a locked
-       ;; region, we could check that no updates are needed and
-       ;; unlock the whole buffer in case they were.  But that's
-       ;; a bit messy.  Instead we assume that things must be
-       ;; 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.
-	(isa-update-thy-only buffer-file-name t 
-			     ;; whether to block or not
-			     (if (and (boundp 'activated-interactively)
-					activated-interactively)
-				 t ; was nil, but falsely leaves Scripting on! 
-			       t))
-	;; Leave the messages from the update around.
-	(setq pg-response-erase-flag nil))))
-
-(defun isa-remove-file (name files cmp-base)
-  (if (not files) nil
-    (let*
-	((file (car files))
-	 (rest (cdr files))
-	 (same (if cmp-base (string= name (file-name-nondirectory file))
-		 (string= name file))))
-      (if same (isa-remove-file name rest cmp-base)
-	(cons file (isa-remove-file name rest cmp-base))))))
-
-(defun isa-shell-compute-new-files-list (str)
-  "Compute the new list of files read by the proof assistant.
-This is called when Proof General spots output matching
-proof-shell-retract-files-regexp."
-  (let*
-      ((name (match-string 1 str))
-       (base-name (file-name-nondirectory name)))
-    (if (string= name base-name)
-	(isa-remove-file name proof-included-files-list t)
-      (isa-remove-file (file-truename name) proof-included-files-list nil))))
-
-
-;;
-;;   Define the derived modes 
-;;
-(eval-and-compile
-(define-derived-mode isa-shell-mode proof-shell-mode
-   "Isabelle shell" nil
-   (isa-shell-mode-config)))
-
-(eval-and-compile
-(define-derived-mode isa-response-mode proof-response-mode
-  "Isabelle response" nil
-  (isa-response-mode-config)))
-
-(eval-and-compile			; to define vars for byte comp.
-(define-derived-mode isa-goals-mode proof-goals-mode
-  "Isabelle goals" nil
-  (isa-goals-mode-config)))
-
-(eval-and-compile			; to define vars for byte comp.
-(define-derived-mode isa-proofscript-mode proof-mode
-    "Isabelle script" nil
-    (isa-mode-config)))
-
-
-;;
-;; Automatically selecting theory mode or Proof General script mode.
-;;
-
-(defun isa-mode ()
-  "Mode for Isabelle buffers: either isa-proofscript-mode or thy-mode.
-Files with extension .thy will be in thy-mode, otherwise we choose
-isa-proofscript-mode."
-  (interactive)
-  (cond
-   (;; Theory files only if they have the right extension
-    (and (buffer-file-name)
-	 (proof-string-match "\\.thy$" (buffer-file-name)))
-
-    ;; Enter theory mode, but first configure settings for proof
-    ;; script if they haven't been done already.  This is a hack,
-    ;; needed because Proof General assumes that the script mode must
-    ;; have been configured before shell mode can be triggered, which
-    ;; isn't true for Isabelle.  
-    ;; (proof-config-done-related and proof-shell-mode refer to
-    ;; the troublesome settings in question)
-    ;; 3.3 fix: add require proof-script since context menus are 
-    ;; now added for response/goals buffer, which requires proof mode. 
-    (unless proof-terminal-char
-      (require 'proof-script)
-      (proof-menu-define-specific)	
-      (isa-mode-config-set-variables)
-      )
-
-    (thy-mode)
-
-    ;; related mode configuration including locking buffer,
-    ;; fontification, etc.
-    (proof-config-done-related)		
-
-    ;; Hack for splash screen
-    (if (and (boundp 'proof-mode-hook)
-	     (memq 'proof-splash-timeout-waiter proof-mode-hook))
-	(proof-splash-timeout-waiter)
-      ;; Otherwise, user may need welcoming.
-      (proof-splash-message)))
-   (t 
-    (isa-proofscript-mode))))
-
-(eval-after-load 
- "thy-mode"
- ;; Extend theory mode keymap
- '(let ((map thy-mode-map))
-(define-key map "\C-c\C-b" 'isa-process-thy-file)
-(define-key map "\C-c\C-r" 'isa-retract-thy-file)
-(proof-define-keys map proof-universal-keys)))
-
-;; FIXME: could test that the buffer isn't already locked.
-(defun isa-process-thy-file (file)
-  "Process the theory file FILE.  If interactive, use buffer-file-name."
-  (interactive (list buffer-file-name))
-  (save-some-buffers)
-  (isa-update-thy-only file nil nil))
-
-(defcustom isa-retract-thy-file-command "ThyInfo.remove_thy \"%r\";"
-  "Sent to Isabelle to forget theory file and descendants.
-Resulting output from Isabelle will be parsed by Proof General."
-  :type 'string
-  :group 'isabelle-config)
-
-(defun isa-retract-thy-file (file)
-  "Retract the theory file FILE. If interactive, use buffer-file-name.
-To prevent inconsistencies, scripting is deactivated before doing this. 
-So if scripting is active in an ML file which is not completely processed, 
-you will be asked to retract the file or process the remainder of it."
-  (interactive (list buffer-file-name))
-  (proof-deactivate-scripting)
-  (proof-shell-invisible-command
-   (proof-format-filename isa-retract-thy-file-command
-			  (file-name-nondirectory 
-			   (file-name-sans-extension file)))))
-
-
-;; Next bits taken from isa-load.el
-;; isa-load.el,v 3.8 1998/09/01 
-
-(defgroup thy nil
-  "Customization of Isamode's theory editing mode"
-  ;; :link '(info-link "(Isamode)Theory Files")
-  :load 'thy-mode
-  :group 'isabelle)
-
-(autoload 'thy-mode "thy-mode" 
-	  "Major mode for Isabelle theory files" t nil)
-
-(autoload 'thy-find-other-file "thy-mode" 
-	    "Find associated .ML or .thy file." t nil)
-
-(defun isa-splice-separator (sep strings)
-  (let (stringsep)
-    (while strings
-      (setq stringsep (concat stringsep (car strings)))
-      (setq strings (cdr strings))
-      (if strings (setq stringsep 
-			(concat stringsep sep))))
-    stringsep))
-
-(defun isa-file-name-cons-extension (name)
-  "Return cons cell of NAME without final extension and extension"
-  (if (string-match "\\.[^\\.]+$" name)
-      (cons (substring name 0 (match-beginning 0))
-	    (substring name (match-beginning 0)))
-    (cons name "")))
-
-(defun isa-format (alist string)
-  "Format a string by matching regexps in ALIST against STRING"
-  (while alist
-    (while (string-match (car (car alist)) string)
-      (setq string
-	    (concat (substring string 0 (match-beginning 0))
-		    (cdr (car alist))
-		    (substring string (match-end 0)))))
-    (setq alist (cdr alist)))
-  string)
-
-;; Key to switch to theory mode
-(define-key isa-proofscript-mode-map 
-  [(control c) (control o)] 'thy-find-other-file)
-
-
-
-
-;;
-;;  Code that's Isabelle specific
-;;
-
-(defcustom isa-not-undoable-commands-regexp
-  (proof-ids-to-regexp '("undo"))
-  "Regular expression matching commands which are *not* undoable."
-  :type 'regexp
-  :group 'isabelle-config)
-
-;; 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 
-      ((case-fold-search nil)
-       (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 (prev-span span 'type)))
-	(concat "choplev 0" proof-terminal-string)
-      (while span
-	(setq str (span-property span 'cmd))
-	(cond ((eq (span-property span 'type) 'vanilla)
-	       (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 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)
-			    (setq ct (+ 1 ct)))
-			(setq i (+ 1 i))))
-		     (t nil))))
-	(setq span (next-span span 'type)))
-      (concat "ProofGeneral.repeat_undo " 
-	      (int-to-string ct) proof-terminal-string))))
-
-(defun isa-goal-command-p (span)
-  "Decide whether argument is a goal or not"
-  (proof-string-match isa-goal-command-regexp  ; this regexp defined in isa-syntax.el
-		      (or (span-property span 'cmd) ""))) 
-
-;; 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.  So we ought to search
-;; backwards in isa-find-and-forget, rather than forwards as
-;; 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-state-preserving-p (cmd)
-  "Non-nil if command preserves the proofstate."
-  (not (proof-string-match isa-not-undoable-commands-regexp cmd)))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Isa shell startup and exit hooks                               ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun isa-pre-shell-start ()
-  (setq proof-prog-name		(isabelle-command-line))
-  (setq proof-mode-for-shell    'isa-shell-mode)
-  (setq proof-mode-for-goals	'isa-goals-mode)
-  (setq proof-mode-for-response 'isa-response-mode)
-  (setq proof-shell-trace-output-regexp "\375"))
-
-(defun isa-mode-config ()
-  (isa-mode-config-set-variables)
-  (isa-init-syntax-table)
-  (setq font-lock-keywords isa-font-lock-keywords-1)
-  (setq comment-quote-nested nil) ;; we can cope with nested comments
-  (proof-config-done)
-  ;; 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$" . thy-file-tags-table))
-  ;		     tag-table-alist)))
-  (setq blink-matching-paren-dont-ignore-comments t))
-
-
-;; These hooks are added on load because proof shells can
-;; be started from .thy (not in scripting mode) or .ML files.
-;; 3.4: pre-shell-start-hook was a local hook, but then caused
-;; new probs in E21 with not setting in correct buffer for shell(?)
-(add-hook 'proof-pre-shell-start-hook 'isa-pre-shell-start); nil t
-(add-hook 'proof-shell-insert-hook 'isa-preprocessing)
-
-(defun isa-shell-mode-config ()
-  "Configure Proof General proof shell for Isabelle."
-  (isa-init-output-syntax-table)
-  (setq font-lock-keywords isa-output-font-lock-keywords-1)
-  (isa-shell-mode-config-set-variables)
-  (proof-shell-config-done))
-
-(defun isa-response-mode-config ()
-  (setq font-lock-keywords isa-output-font-lock-keywords-1)
-  (isa-init-output-syntax-table)
-  (proof-response-config-done))
-
-(defun isa-goals-mode-config ()
-  ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO.
-  (setq pg-goals-change-goal "Show %s.")	
-  (setq pg-goals-error-regexp proof-shell-error-regexp)
-  (isa-init-output-syntax-table)
-  (setq font-lock-keywords isa-goals-font-lock-keywords)
-  (proof-goals-config-done))
-
-(defun isa-preprocessing ()  ;dynamic scoping of `string'
-  "Handle ^VERBATIM marker -- acts on variable STRING by dynamic scoping"
-  (if (proof-string-match isabelle-verbatim-regexp string)
-      (setq string (match-string 1 string))))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Completion table for Isabelle identifiers
-;;
-;; Ideally this could be set automatically from the running process,
-;; and maybe a default value could be dumped by Isabelle when it is
-;; built.
-
-(defpgdefault completion-table
-  '("quit" 
-    "cd" "use" "use_thy" "time_use" "time_use_thy"
-    "Pretty.setdepth" "Pretty.setmargin" "print_depth"
-    "show_hyps" "show_types" "show_sorts"
-    "print_exn"
-    "goal" "goalw" "goalw_cterm" "premises"
-    "by" "byev" 
-    "result" "uresult"
-    "chop" "choplev" "back" "undo"
-    "pr" "prlev" "goals_limit"
-    "proof_timing"
-    "prove_goal" "prove_goalw" "prove_goalw_cterm"
-    "push_proof" "pop_proof" "rotate_proof"
-    "save_proof" "restore_proof"
-    "read" "prin" "printyp"
-    "topthm" "getgoal" "gethyps"
-    "filter_goal" "compat_goal"
-
-    ;; short cuts - should these be included?
-    "ba" "br" "be" "bd" "brs" "bes" "bds"
-    "fs" "fr" "fe" "fd" "frs" "fes" "fds"
-    "bw" "bws" "ren"
-
-    "resolve_tac" "eresolve_tac" "dresolve_tac" "forward_tac"
-    "assume_tac" "eq_assume_tac"
-    "match_tac" "ematch_tac" "dmatch_tac"
-    "res_inst_tac" "eres_inst_tac" "dres_inst_tac" "forw_inst_tac"
-    "rewrite_goals_tac" "rewrite_tac" "fold_goals_tac"
-    "fold_goals_tac" "fold_tac"
-    "cut_facts_tac" "subgoal_tac"
-
-    ;; short cuts - should these be included?
-    "rtac" "etac" "dtac" "atac" "ares_tac" "rewtac"
-
-    ;; In general, I think rules should appear in rule tables, not here.
-    "asm_rl" "cut_rl"  
-
-    "flexflex_tac" "rename_tac" "rename_last_tac"
-    "Logic.set_rename_prefix" "Logic.auto_rename"
-
-    "compose_tac"
-
-    "biresolve_tac" "bimatch_tac" "subgoals_of_brl" "lessb"
-    "head_string" "insert_thm" "delete_thm" "compat_resolve_tac"
-
-    "could_unify" "filter_thms" "filt_resolve_tac"
-
-    ;; probably shouldn't be included:
-    "tapply" "Tactic" "PRIMITIVE" "STATE" "SUBGOAL"
-
-    "pause_tac" "print_tac"
-
-    "THEN" "ORELSE" "APPEND" "INTLEAVE"
-    "EVERY" "FIRST" "TRY" "REPEAT_DETERM" "REPEAT" "REPEAT1"
-    "trace_REPEAT"
-    "all_tac" "no_tac"
-    "FILTER" "CHANGED" "DEPTH_FIRST" "DEPTH_SOLVE"
-    "DEPTH_SOLVE_1" "trace_DEPTH_FIRST"
-    "BREADTH_FIRST" "BEST_FIRST" "THEN_BEST_FIRST"
-    "trace_BEST_FIRST"
-    "COND" "IF_UNSOLVED" "DETERM" 
-    
-    "SELECT_GOAL" "METAHYPS"
-
-    "ALLGOALS" "TRYALL" "SOMEGOAL" "FIRSTGOAL"
-    "REPEAT_SOME" "REPEAT_FIRST" "trace_goalno_tac"
-
-    ;; include primed versions of tacticals?
-
-    "EVERY1" "FIRST1"
-
-    "prth" "prths" "prthq"
-    "RSN" "RLN" "RL"
-
-    ;; simplifier
-    
-    "addsimps" "addeqcongs" "delsimps"
-    "setsolver" "setloop" "setmksimps" "setsubgoaler"
-    "empty_ss" "merge_ss" "prems_of_ss" "rep_ss"
-    "simp_tac" "asm_full_simp_tac" "asm_simp_tac"
-
-    ;; classical prover
-
-    "empty_cs" 
-    "addDs" "addEs" "addIs" "addSDs" "addSEs" "addSIs" 
-    "print_cs" 
-    "rep_claset" "best_tac" "chain_tac" "contr_tac" "eq_mp_tac"
-    "fast_tac" "joinrules" "mp_tac" "safe_tac" "safe_step_tac" 
-    "slow_best_tac" "slow_tac" "step_tac" "swapify" 
-    "swap_res_tac" "inst_step_tac" 
-    
-    ;; that's it for now!
-    ))
-
-(provide 'isa)
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
deleted file mode 100644
index 631e8908..00000000
--- a/isa/isabelle-system.el
+++ /dev/null
@@ -1,598 +0,0 @@
-;; isabelle-system.el Interface with Isabelle system
-;;
-;; Copyright (C) 2000 LFCS Edinburgh, David Aspinall. 
-;;
-;; Author:      David Aspinall <da@dcs.ed.ac.uk>
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
-;;
-;; $Id$
-;;
-;; Most of this code is taken from the final version of Isamode.
-;; --------------------------------------------------------------
-;;
-
-(require 'proof)			; for proof-assistant-symbol, etc.
-(require 'proof-syntax)			; for proof-string-match
-
-(defconst isa-running-isar 
-  (eq proof-assistant-symbol 'isar))
-
-;; If we're using Isabelle/Isar then the isabelle custom
-;; group won't have been defined yet.
-(if isa-running-isar
-(defgroup isabelle nil
-  "Customization of user options for Isabelle and Isabelle/Isar Proof General"
-  :group 'proof-general))
-
-(defcustom isabelle-web-page
-  "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/"
-  ;; "http://isabelle.in.tum.de"
-  ;; "http://www.dcs.ed.ac.uk/home/isabelle"
-  "URL of web page for Isabelle."
-  :type 'string
-  :group 'isabelle)
-
-
-;;; ================ Extract Isabelle settings ================
-
-(defcustom isa-isatool-command
-  (or (getenv "ISATOOL") 
-      (proof-locate-executable "isatool")
-      ;; FIXME: use same mechanism as isabelle-program-name below.
-      (let ((possibilities
-	     (list
-	      (concat (getenv "HOME") "/Isabelle/bin/isatool")
-	      "/usr/share/Isabelle/bin/isatool"
-	      "/usr/local/bin/isatool"
-	      "/usr/local/Isabelle/bin/isatool"
-	      "/usr/bin/isatool"
-	      "/opt/bin/isatool"
-	      "/opt/Isabelle/bin/isatool")))
-	(while (and possibilities
-		    (not (file-executable-p
-			  (car possibilities))))
-	  (setq possibilities (cdr possibilities)))
-	(car-safe possibilities))
-      "path_to_isatool_is_unknown")
-  "Command to invoke Isabelle tool 'isatool'.
-XEmacs should be able to find `isatool' if it is on the PATH when
-started.  Then several standard locations are attempted.
-Otherwise you should set this, using a full path name here for reliable 
-working."
-  :type 'file
-  :group 'isabelle)
-
-(defvar isatool-not-found nil
-  "Non-nil if user has been prompted for `isatool' already and it wasn't found.")
-
-(defun isa-set-isatool-command ()
-  "Make sure isa-isatool-command points to a valid executable.
-If it does not, prompt the user for the proper setting.
-If it appears we're running on win32 or FSF Emacs, we allow this to
-remain unverified.
-Returns non-nil if isa-isatool-command is surely an executable
-with full path."
-  (interactive)
-  (unless (or isatool-not-found (file-executable-p isa-isatool-command))
-    (setq isa-isatool-command
-	  (read-file-name
-	   "Please give the full path to `isatool' (RET if you don't have it): "
-	   nil nil nil))
-    (if (not (file-executable-p isa-isatool-command))
-	(progn
-	  (setq isatool-not-found t)
-	  (beep)
-	  (warn "Proof General: isatool command not found; some menus will be incomplete and Isabelle may not run correctly.  Please check your Isabelle installation."))))
-  (file-executable-p isa-isatool-command))
-
-(defun isa-shell-command-to-string (command)
-  "Like shell-command-to-string except the last character is stripped."
-  (let ((s (shell-command-to-string command)))
-    (if (equal (length s) 0) s
-      (substring s 0 -1))))
-
-(defun isa-getenv (envvar &optional default)
-  "Extract an environment variable setting using the `isatool' program.
-If the isatool command is not available, try using elisp's getenv
-to extract the value from Emacs' environment.
-If there is no setting for the variable, DEFAULT will be returned"
-  (isa-set-isatool-command)
-  (if (file-executable-p isa-isatool-command)
-      (let ((setting (isa-shell-command-to-string
-		      (concat isa-isatool-command
-			      " getenv -b " envvar))))
-	(if (string-equal setting "")
-	    default
-	  setting))
-    (or (getenv envvar) default)))
-
-;;;
-;;; ======= Interaction with System using Isabelle tools =======
-;;;
-
-(defcustom isabelle-program-name 
-  (if (fboundp 'proof-running-on-win32)	
-      "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\"
-    (proof-locate-executable "isabelle" t
-			     '("/usr/local/Isabelle/bin/"
-			       "/opt/Isabelle/bin/"
-			       "/usr/Isabelle/bin/"
-			       "/usr/share/Isabelle/bin/")))
-  "*Default name of program to run Isabelle.
-
-The default value except when running under Windows is \"isabelle\",
-which will get expanded using PATH if possible, or in a number
-of standard locations (/usr/local/Isabelle/, /opt/Isabelle, etc). 
-
-The default value when running under Windows is:
-
-  C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\
-
-This expects SML/NJ in C:\\sml and Isabelle images in C:\Isabelle.  
-The logic image name is tagged onto the end.  
-
-NB: The Isabelle settings mechanism or the environment variable
-ISABELLE will always override this setting."
-  :type 'file
-  :group 'isabelle)
-
-(defvar isabelle-prog-name isabelle-program-name
-  "Set from `isabelle-program-name', has name of logic appended sometimes.")
-
-(defun isabelle-command-line ()
-  "Make proper command line for running Isabelle"
-  (let*
-      ;; The ISABELLE and PROOFGENERAL_LOGIC values (as set when run
-      ;; under the interface wrapper script) indicate that we should
-      ;; determine the proper command line from the current Isabelle
-      ;; settings environment.
-      ((isabelle (or
-		  (getenv "ISABELLE")	; overrides default, may be updated
-		  isabelle-program-name ; calculated earlier
-		  "isabelle"))		; to be really sure
-       (isabelle-opts (getenv "ISABELLE_OPTIONS"))
-       (opts (concat
-	      (if isa-running-isar " -PI" "")
-	      (if (and proof-shell-unicode isa-running-isar) " -m PGASCII" "")
-	      (if (and isabelle-opts (not (equal isabelle-opts "")))
-		  (concat " " isabelle-opts) "")))
-       (logic (or isabelle-chosen-logic
-		  (getenv "PROOFGENERAL_LOGIC")))
-       (logicarg (if (and logic (not (equal logic "")))
-		     (concat " " logic) "")))
-    (concat isabelle opts logicarg)))
-
-
-(defun isabelle-choose-logic (logic)
-  "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
-  (interactive 
-   (list (completing-read 
-	  "Use logic: "
-	  (mapcar 'list (cons "Default" 
-			      isabelle-logics-available)))))
-  ;; a little bit obnoxious maybe (but maybe what naive user would expect)
-  ;; (customize-save-variable 'isabelle-chosen-logic logic)
-  (if (proof-shell-live-buffer)
-      (error "Can't change logic while Isabelle is running, please exit process first!"))
-  (customize-set-variable 'isabelle-chosen-logic 
-			  (unless (string-equal logic "Default") logic))
-  (setq isabelle-prog-name (isabelle-command-line))
-  (setq proof-prog-name isabelle-prog-name)
-  ;; Settings are potentially different between logics, and
-  ;; so are Isar keywords.  Set these to nil so they get
-  ;; automatically re-initialised.  
-  ;; FIXME: Isar keywords change not handled yet.
-  (setq proof-assistant-settings nil)
-  (setq proof-menu-settings nil))
-
-(defun isa-tool-list-logics ()
-  "Generate a list of available object logics."
-  (if (isa-set-isatool-command)
-      (delete "" (split-string 
-		  (isa-shell-command-to-string
-		   (concat isa-isatool-command " findlogics")) "[ \t]"))))
-
-(defun isa-view-doc (docname)
-  "View Isabelle document DOCNAME, using Isabelle tools."
-  (if (isa-set-isatool-command)
-      (apply 'start-process
-	     "isa-view-doc" nil
-	     (list isa-isatool-command "doc" docname))))
-
-(defvar isabelle-version-string 'unset)
-
-(defun isa-version ()
-  "Try to retrieve a version value for Isabelle."
-  (unless (stringp isabelle-version-string)
-    (setq isabelle-version-string
-	  (if (isa-set-isatool-command)
-	      (isa-shell-command-to-string
-	       ;; This may return the string "Unknown Isabelle tool:
-	       ;; version", but that's fine.
-	       (concat isa-isatool-command " version"))
-	    "Unknown")))
-  isabelle-version-string)
-
-;; We're going to need to know this pretty soon, so let's do it now.
-(defconst isa-supports-pgip 
-  ;; PGIP-aware Isabelle versions are also aware of their own version
-  (not (string-match "^Unknown" (isa-version)))
-  "Whether the currently configured version of Isabelle supports PGIP.")
-
-      
-
-
-(defun isa-tool-list-docs ()
-  "Generate a list of documentation files available, with descriptions.
-This function returns a list of lists of the form
- ((DOCNAME DESCRIPTION) ....)
-of Isabelle document names and descriptions.  When DOCNAME is
-passed to isa-tool-doc-command, DOCNAME will be viewed."
-  (if (isa-set-isatool-command)
-      (let ((docs (isa-shell-command-to-string
-		   (concat isa-isatool-command " doc"))))
-	(unless (string-equal docs "")
-	  (mapcan
-	   (function (lambda (docdes)
-		       (if (proof-string-match "^[ \t]+\\(\\S-+\\)[ \t]+" docdes)
-			   (list (list 
-				  (substring docdes (match-beginning 1) (match-end 1))
-				  (substring docdes (match-end 0)))))))
-	   (split-string docs "\n"))))))
-
-(defun isa-quit (save)
-  "Quit / save the Isabelle session.
-Called with one argument: t to save database, nil otherwise."
-  (if (not save)
-      (isa-insert-ret "quit();"))
-  (comint-send-eof))
-
-(defconst isabelle-verbatim-regexp "\\`\^VERBATIM: \\(\\(.\\|\n\\)*\\)\\'"
-  "Regexp matching internal marker for verbatim command output")
-
-(defun isabelle-verbatim (str)
-  "Mark internal command for verbatim output"
-  (concat "\^VERBATIM: " str))
-
-;;; Set proof-shell-pre-interrupt-hook for PolyML 3.
-(if (and
-     (not proof-shell-pre-interrupt-hook)
-     ;; (Older versions of Isabelle reported PolyML for PolyML 3).
-     (proof-string-match-safe "\\`polyml" (isa-getenv "ML_SYSTEM"))
-     (not (proof-string-match-safe "\\`polyml-4" (isa-getenv "ML_SYSTEM"))))
-    (add-hook
-     'proof-shell-pre-interrupt-hook
-     (lambda () (proof-shell-insert (isabelle-verbatim "f") nil))))
-
-;;; ==========  Utility functions ==========
-
-(defcustom isabelle-refresh-logics t
-  "*Whether to refresh the list of logics during an interactive session.
-If non-nil, then `isatool findlogics' will be used to regenerate
-the `isabelle-logics-available' setting.  If this tool does not work
-for you, you should disable this behaviour."
-  :type 'boolean
-  :group 'isabelle)
-
-(defcustom isabelle-logics-available (isa-tool-list-logics)
-  "*List of logics available to use with Isabelle.
-If the `isatool' program is available, this is automatically
-generated with the lisp form `(isa-tool-list-logics)'."
-  :type (list 'string)
-  :group 'isabelle)
-
-;; FIXME: document this one
-(defcustom isabelle-chosen-logic nil
-  "*Choice of logic to use with Isabelle.
-If non-nil, will be added into isabelle-prog-name as default value.
-
-NB: you have saved a new logic image, it may not appear in the choices
-until Proof General is restarted."
-  :type (append
-	 (list 'choice)
-	 (mapcar (lambda (str) (list 'const str)) isabelle-logics-available)
-	 (list '(string :tag "Choose another")
-	       '(const :tag "Unset (use default)" nil)))
-  :group 'isabelle)
-
-(defconst isabelle-docs-menu 
-  (let ((vc '(lambda (docdes)
-	       (vector (car (cdr docdes))
-		       (list 'isa-view-doc (car docdes)) t))))
-    (list (cons "Isabelle documentation" (mapcar vc (isa-tool-list-docs)))))
-  "Isabelle documentation menu.  Constructed when PG is loaded.")
-
-
-;; PG 3.5: logics menu is now refreshed automatically.  Rather
-;; a big effort for such a small effect.
-(defun isabelle-logics-menu-calculate ()
-  (setq isabelle-logics-menu-entries
-	(cons "Logics"
-	      (append
-	       '(["Default" 
-		  (isabelle-choose-logic nil)
-		  :active (not (proof-shell-live-buffer))
-		  :style radio
-		  :selected (not isabelle-chosen-logic)])
-	       (mapcar (lambda (l) 
-		   (vector l (list 'isabelle-choose-logic l)
-			   :active '(not (proof-shell-live-buffer))
-			   :style 'radio
-			   :selected (list 'equal 'isabelle-chosen-logic l)))
-		       isabelle-logics-available)))))
-
-(defvar isabelle-time-to-refresh-logics t
-  "Non-nil if we should refresh the logics list")
-
-(defun isabelle-logics-menu-refresh ()
-  "Refresh isabelle-logics-menu-entries, returning new entries."
-  (interactive)
-  (if (and isabelle-refresh-logics
-	   (or isabelle-time-to-refresh-logics (interactive-p)))
-      (progn
-	(setq isabelle-logics-available (isa-tool-list-logics))
-	(isabelle-logics-menu-calculate)
-	(if proof-running-on-Emacs21 
-	    ;; update the menu manually
-	    (easy-menu-add-item proof-assistant-menu nil 
-				isabelle-logics-menu-entries))
-	(setq isabelle-time-to-refresh-logics nil) ;; just done it, don't repeat!
-	(run-with-timer 2 nil ;; short delay to avoid doing this too often
-			(lambda () (setq isabelle-time-to-refresh-logics t))))))
-
-;; Function for XEmacs only
-(defun isabelle-logics-menu-filter (&optional ignored)
-  (isabelle-logics-menu-refresh)
-  (cdr isabelle-logics-menu-entries))
-
-;; Functions for GNU Emacs only to update logics menu
-(if proof-running-on-Emacs21
-(defun isabelle-menu-bar-update-logics ()
-  ;; standard check we're being invoked
-  (and (current-local-map)
-       (keymapp (lookup-key (current-local-map) 
- 			    (vector 'menu-bar (intern proof-assistant))))
-       (isabelle-logics-menu-refresh))))
-
-(if proof-running-on-Emacs21
-    (add-hook 'menu-bar-update-hook 'isabelle-menu-bar-update-logics))
-
-
-(defvar isabelle-logics-menu-entries (isabelle-logics-menu-calculate))
-
-(defvar isabelle-logics-menu 
-   (if proof-running-on-XEmacs
-       (cons (car isabelle-logics-menu-entries)
-	     (list :filter 'isabelle-logics-menu-filter)) ;; generates menu on click
-     isabelle-logics-menu-entries)
-  "Isabelle logics menu.  Calculated when Proof General is loaded.")
-
-;; Added in PG 3.4: load isar-keywords file.
-;; This roughly follows the method given in the interface script.
-;; It could be used to add an elisp command at the bottom of
-;; a theory file, if we sorted out the load order a bit, or
-;; added a facility to reconfigure.
-;; TODO: also add something to spill out a keywords file?
-(defun isabelle-load-isar-keywords (&optional kw)
-  (interactive "sLoad isar keywords: ")
-  (let ((userhome  (isa-getenv "ISABELLE_HOME_USER"))
-	(isahome   (isa-getenv "ISABELLE_HOME"))
-	(isarkwel  "%s/etc/isar-keywords-%s.el")
-	(isarel    "%s/etc/isar-keywords.el")
-	(ifrdble   (lambda (f) (if (file-readable-p f) f))))
-    (load-file
-     (or
-      (and kw (funcall ifrdble (format isarkwel userhome kw)))
-      (and kw (funcall ifrdble (format isarkwel isahome kw)))
-      (funcall ifrdble (format isarel userhome))
-      (funcall ifrdble (format isarel isahome))
-      (locate-library "isar-keywords")))))
-
-
-;;; ========== Mirroring Proof General options in Isabelle process ========
-
-;; NB: use of defpacustom here gives  separate customizable
-;; options for Isabelle and Isabelle/Isar.
-
-;; In latest release of Isabelle, these are set automatically via PGIP
-;; sent from Isabelle.
-
-;; BEGIN backwards compatibility 
-(cond 
- ((not isa-supports-pgip)
-(defpacustom show-types  nil
-  "Whether to show types in Isabelle."
-  :type 'boolean
-  :setting "show_types:=%b;")
-
-(defpacustom show-sorts  nil
-  "Whether to show sorts in Isabelle."
-  :type 'boolean
-  :setting "show_sorts:=%b;")
-
-(defpacustom show-consts  nil
-  "Whether to show types of consts in Isabelle goals."
-  :type 'boolean
-  :setting "show_consts:=%b;")
-
-(defpacustom long-names  nil
-  "Whether to show fully qualified names in Isabelle."
-  :type 'boolean
-  :setting "long_names:=%b;")
-
-(defpacustom eta-contract  t
-  "Whether to print terms eta-contracted in Isabelle."
-  :type 'boolean
-  :setting "Syntax.eta_contract:=%b;")
-
-(defpacustom trace-simplifier  nil
-  "Whether to trace the Simplifier in Isabelle."
-  :type 'boolean
-  :setting "trace_simp:=%b;")
-
-(defpacustom trace-rules  nil
-  "Whether to trace the standard rules in Isabelle."
-  :type 'boolean
-  :setting "trace_rules:=%b;")
-
-(defpacustom quick-and-dirty  t
-  "Whether to take a few short cuts occasionally."
-  :type 'boolean
-  :setting "quick_and_dirty:=%b;")
-
-(defpacustom full-proofs  nil
-  "Whether to record full proof objects internally."
-  :type 'boolean
-  :setting "ProofGeneral.full_proofs %b;")
-
-(defpacustom global-timing  nil
-  "Whether to enable timing in Isabelle."
-  :type 'boolean
-  :setting "Library.timing:=%b;")
-
-(if proof-experimental-features
-(defpacustom theorem-dependencies nil
-  "Whether to track theorem dependencies within Proof General."
-  :type 'boolean
-  :setting ("change print_mode (insert (op =) \"thm_deps\");" .
-	    "change print_mode (remove (op =) \"thm_deps\");")))
-
-(defpacustom goals-limit  10
-  "Setting for maximum number of goals printed in Isabelle."
-  :type 'integer
-  :setting "goals_limit:=%i;")
-
-(defpacustom prems-limit  10
-  "Setting for maximum number of premises printed in Isabelle/Isar."
-  :type 'integer
-  :setting "ProofContext.prems_limit:=%i;")
-
-(defpacustom print-depth  10
-  "Setting for the ML print depth in Isabelle."
-  :type 'integer
-  :setting "print_depth %i;")))
-;; END backwards compatibility 
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Generic Isabelle menu for Isabelle and Isabelle/Isar
-;;
-
-(defpgdefault menu-entries
-  (append
-   (if isa-running-isar
-       nil
-     (list ["Switch to theory" thy-find-other-file t]))
-   (list isabelle-logics-menu)))
-
-(defpgdefault help-menu-entries isabelle-docs-menu)
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; X-Symbol language configuration, and adding to completion table
-;;
-
-(defpgdefault x-symbol-language 'isabelle)
-
-
-(eval-after-load "x-symbol-isabelle"
- ;; Add x-symbol tokens to isa-completion-table and rebuild
- ;; internal completion table if completion is already active
-'(progn
-   (defpgdefault completion-table
-     (append (proof-ass completion-table)
-	     (mapcar (lambda (xsym) (nth 2 xsym))
-		     x-symbol-isabelle-table)))
-   (setq proof-xsym-font-lock-keywords
-	 x-symbol-isabelle-font-lock-keywords)
-   (if (featurep 'completion)
-       (proof-add-completions))))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Subterm markup -- faking it
-;;
-
-(defun isabelle-convert-idmarkup-to-subterm ()
-  "Convert identifier markup to subterm markup.
-This is a hook setting for `pg-after-fontify-output-hook' to
-enable identifiers to be highlighted.  (To disable that behaviour,
-the function `pg-remove-specials' can be used instead)."
-  ;; NB: the order of doing this is crucial: it must happen after
-  ;; fontifying (since replaces chars used for fontifying), but before
-  ;; X-Sym decoding (since some chars used for fontifying may clash
-  ;; with X-Sym character codes: luckily those codes don't seem to
-  ;; cause problems for subterm markup).
-  ;; Future version of this should use PGML output in Isabelle2002.
-  (goto-char (point-min))
-  (while (proof-re-search-forward "[\351-\357]" nil t)
-    (replace-match "\372\200\373" nil t))
-  (goto-char (point-min))
-  (while (proof-re-search-forward "\350" nil t)
-    (replace-match "\374" nil t)))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Context-senstive in-span menu additions 
-;;
-
-(defun isabelle-create-span-menu (span idiom name)
-  (if (string-equal idiom "proof")
-      (let ((thm (span-property span 'name)))
-	(list (vector 
-	       "Visualise dependencies" 
-	       `(proof-shell-invisible-command 
-		 ,(format (if isa-running-isar 
-			      "thm_deps %s;" "thm_deps [%s];") thm))
-	       (not (string-equal thm proof-unnamed-theorem-name)))))))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; XML as an SML string: add escapes for quotes
-;;
-
-(defun isabelle-xml-sml-escapes (xmlstring)
-  (replace-regexp-in-string "\"" "\\\"" xmlstring t t))
-
-(defun isabelle-process-pgip (xmlstring)
-  "Return an Isabelle or Isabelle/Isar command to process PGIP in XMLSTRING."
-  (if isa-supports-pgip
-      (let ((mlcmd (format "ProofGeneral.process_pgip(\"%s\");"
-			   (isabelle-xml-sml-escapes xmlstring))))
-	(if (eq proof-assistant-symbol 'isar)
-	    (isar-markup-ml mlcmd)
-	  mlcmd))
-    "")) ;; Empty string in case called with non PGIP-aware Isabelle.
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Understanding syntax configuration (really should be PGIP, but...)
-;;
-;; [PRESENTLY UNUSED; WORK IN PROGRESS]
-
-(defun isabelle-parse-syntax-dump (buf)
-  (save-excursion
-    (let (consts start lim)
-      (set-buffer buf)
-      (goto-char (point-min))
-      (if (re-search-forward "consts:" nil t)
-	  (progn
-	    (setq start (point))
-	    (setq lim (re-search-forward "parse_ast_translation:" nil t))
-	    (goto-char start)
-	    (while (re-search-forward "\"\\([^\"]*\\)\"" lim t)
-	      (if (< 0 (length (match-string 1)))
-		  (setq consts (cons (match-string 1) consts))))))
-      consts)))
-
-
-(provide 'isabelle-system)
-;; End of isabelle-system.el
diff --git a/isa/thy-mode.el b/isa/thy-mode.el
deleted file mode 100644
index 2eef0988..00000000
--- a/isa/thy-mode.el
+++ /dev/null
@@ -1,1045 +0,0 @@
-;; thy-mode.el - Mode for Isabelle theory files.
-;;
-;; Copyright (C) 1998 LFCS Edinburgh. 
-;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
-;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; Taken from Isamode, version: 3.6 1998/09/02 11:40:45
-;;
-;; $Id$
-;;
-;; NAMESPACE management: all functions and variables declared
-;; in this file begin with thy-
-
-(require 'proof-site)
-(require 'proof-syntax)
-(require 'isa)
-
-;; In case thy mode was invoked directly or by -*- thy -*- at
-;; the start of the file, ensure that isa mode is used from now
-;; on for .thy files.
-;; FIXME: be less messy with auto-mode-alist here (remove dups)
-(setq auto-mode-alist
-      (cons '("\\.thy$" . isa-mode) auto-mode-alist))
-
-;;; ========== Theory File Mode User Options ==========
-
-(defcustom thy-heading-indent 0
-  "Indentation for section headings."
-  :type  'integer
-  :group 'thy)
-
-(defcustom thy-indent-level 2
-  "*Indentation level for Isabelle theory files.  An integer."
-  :type  'integer
-  :group 'thy)
-
-(defcustom thy-indent-strings t
-  "If non-nil, indent inside strings.
-You may wish to disable indenting inside strings if your logic uses
-any of the usual bracket characters in unusual ways."
-  :type 'boolean
-  :group 'thy)
-
-(defcustom thy-use-sml-mode nil
-  "*If non-nil, invoke sml-mode inside \"ML\" section of theory files.
-This option is left-over from Isamode.  Really, it would be more
-useful if the script editing mode of Proof General itself could be based 
-on sml-mode, but at the moment there is no way to do this."
-  :type 'boolean
-  :group 'thy)
-
-
-;;; ======  Theory and ML file templates =========================    
-
-(defcustom thy-sections
-  ;; NB: preceding white space in templates deleted by indentation alg.
-  ;;     top must come first.
-  '(("top" .     thy-insert-header)
-    ("classes" . thy-insert-class)
-    ("default" . thy-insert-default-sort) ; is "default" obsolete?
-    ("defaultsort" . thy-insert-default-sort)
-    ("types"   . thy-insert-type) 
-    ("typedecl")
-    ("arities" . thy-insert-arity)
-    ;; =================================
-    ;; These only make sense for HOL.
-    ;; Ideally we should parameterise these parts on the theory.
-    ("datatype") ("typedef")
-    ("inductive") ("coninductive")
-    ("intrs") ("monos")
-    ("primrec") ("recdef")
-    ("rep_datatype") ("distinct") ("induct")
-    ;; ==============================
-    ("consts"  . thy-insert-const)
-    ("translations" . "\"\"\t==\t\"\"")
-    ("axclass")
-    ("syntax")
-    ("instance")
-    ("rules"   . thy-insert-rule)
-    ("defs"    . thy-insert-rule)
-    ("axioms"    . thy-insert-rule)
-    ("use")
-    ("theory")
-    ("files")
-    ("constdefs")
-    ("oracle")
-    ("local")
-    ("locale")
-    ("nonterminals")
-    ("setup")
-    ("global")
-    ("end")
-    ("ML"))
-  "Names of theory file sections and their templates.
-Each item in the list is a pair of a section name and a template.
-A template is either a string to insert or a function. Useful functions are:
-  thy-insert-header, thy-insert-class, thy-insert-default-sort,
-  thy-insert-const, thy-insert-rule.
-The nil template does nothing.
-You can add extra sections to theory files by extending this variable."
-  :type '(repeat
-	  (cons string
-	       (choice function
-		       string
-		       (const :tag "no template" nil))))
-  :group 'thy)
-
-(defcustom thy-id-header
-  "(* 
-    File:	 %f
-    Theory Name: %t
-    Logic Image: %l
-*)\n\n"
-  "*Identification header for .thy and .ML files.
-Format characters: %f replaced by filename, %t by theory name,
-and %l by the logic image name this file should be read in."
-  :group 'thy
-  :type 'string)
-
-(defcustom thy-template
-"%t  =  %p +\n
-classes\n
-default\n
-types\n
-arities\n
-consts\n
-translations\n
-rules\n
-end\n
-ML\n"
-"Template for theory files.
-Contains a default selection of sections in a traditional order.
-You can use the following format characters:
-
-`%t' --- replaced by theory name.
-
-`%p' --- replaced by names of parents, separated by `+' characters."
- :group 'thy
- :type 'string)
-
-
-
-;;; ========== Code ==========
-
-(defvar thy-mode-map nil)
-
-(defvar thy-mode-syntax-table nil)		; Shared below.
-
-(if thy-mode-syntax-table	
-    nil		
-  ;; This is like sml-mode, except:
-  ;;   .   is a word constituent (not punctuation).  (bad for comments?)
-  ;;   "   is a paired delimiter
-  (setq thy-mode-syntax-table (make-syntax-table))
-  (modify-syntax-entry ?\( "()1 " thy-mode-syntax-table)
-  (modify-syntax-entry ?\) ")(4 " thy-mode-syntax-table)
-  (modify-syntax-entry ?\\ "\\   " thy-mode-syntax-table)
-  (modify-syntax-entry ?*  ". 23" thy-mode-syntax-table)
-  (modify-syntax-entry ?_  "w   " thy-mode-syntax-table)
-  (modify-syntax-entry ?\' "w   " thy-mode-syntax-table)
-;  it's annoying to match with quotes from previous strings,
-;  so this has been removed. 
-;  (modify-syntax-entry ?\" "$   " thy-mode-syntax-table)
-  (modify-syntax-entry ?.  "w   " thy-mode-syntax-table))
-
-(or thy-mode-map
-    (let ((map (make-sparse-keymap)))
-      (define-key map [(control up)] 'thy-goto-prev-section)
-      (define-key map [(control down)] 'thy-goto-next-section)
-      (define-key map "\C-c\C-n" 'thy-goto-next-section)
-      (define-key map "\C-c\C-p" 'thy-goto-prev-section)
-      (define-key map "\C-c\C-m" 'thy-minor-sml-mode)
-      (define-key map "\C-c\C-t" 'thy-insert-template)
-      ;; Disabled for Proof General
-      ;;(define-key map "\C-c\C-u" 'thy-use-file)
-      ;;(define-key map "\C-c\C-l" 'thy-raise-windows)
-      (define-key map "\C-c\C-o" 'thy-find-other-file)
-      (define-key map "\C-M" 'newline-and-indent)
-      (define-key map "\C-k" 'thy-kill-line)
-      (setq thy-mode-map map)))
-
-(defun thy-add-menus (&optional file)
-  "Add Proof General and Isabelle menu to current menu bar."
-  (require 'proof-script)		; Later: proof-menu, autoloaded
-  (easy-menu-define thy-mode-pg-menu
-		    thy-mode-map
-		    "PG Menu for Isabelle Proof General"
-		    (cons proof-general-name
-			  (append
-			   (list
-			   ;; A couple from the toolbar that make sense here
-			   ;; (also in proof-universal-keys)
-			    ["Issue command" proof-minibuffer-cmd t]
-			    ["Interrupt prover" proof-interrupt-process t])
-			   (list proof-buffer-menu)
-			   (list proof-help-menu))))
-  (easy-menu-define thy-mode-isa-menu
-		    thy-mode-map
-		    "Menu for Isabelle Proof General, theory file mode."
-		    (cons "Theory"
-			  (list
-			   ["Next Section" thy-goto-next-section t]
-			   ["Prev Section" thy-goto-prev-section t]
-			   ["Insert Template" thy-insert-template t]
-			   ["Process Theory" isa-process-thy-file
-			    :active (proof-locked-region-empty-p)]
-			   ["Retract Theory" isa-retract-thy-file
-			    :active (proof-locked-region-full-p)]
-			   ["Next Error" proof-next-error t]
-			   ["Switch to Script" thy-find-other-file t])))
-  (easy-menu-add thy-mode-pg-menu thy-mode-map)
-  (easy-menu-add thy-mode-isa-menu thy-mode-map)
-  
-  (if file
-     (progn (easy-menu-remove thy-mode-deps-menu)
-	    (proof-thy-menu-define-deps file)
-	    (easy-menu-add thy-mode-deps-menu thy-mode-map))))
-
-
-(defun thy-mode (&optional nomessage)
-  "Major mode for editing Isabelle theory files.
-\\<thy-mode-map>
-\\[thy-goto-next-section]\t Skips to the next section.
-\\[thy-goto-prev-section]\t Skips to the previous section.
-
-\\[indent-for-tab-command]\t Indents the current line.
-
-\\[thy-insert-template]\t Inserts a template for the file or current section.
-
-If thy-use-sml-mode is non-nil, \\<thy-mode-map>\\[thy-minor-sml-mode] \
-invokes sml-mode as a minor mode 
-in the ML section.  This is done automatically by \
-\\[indent-for-tab-command].
-
-The style of indentation for theory files is controlled by these variables:
-  thy-heading-indent 
-  thy-indent-level
-  thy-indent-strings
-- see individual variable documentation for details.
-
-Here is the full list of theory mode key bindings:
-\\{thy-mode-map}"
-  (interactive)
-  (kill-all-local-variables)
-  (setq major-mode 'thy-mode)
-  (setq mode-name "Theory")
-  (use-local-map thy-mode-map)
-  (thy-add-menus)
-
-  (set-syntax-table thy-mode-syntax-table)
-  (make-local-variable 'indent-line-function)
-  (setq indent-line-function 'thy-indent-line)
-  (make-local-variable 'comment-start)			; Following lines as in sml-mode
-  (setq comment-start "(* ")				; .
-  (make-local-variable 'comment-end)			; .
-  (setq comment-end " *)")				; .
-  (setq comment-start-skip "(\\*+[ \t]?")		; .
-  (setq font-lock-keywords
-	thy-mode-font-lock-keywords)
-
-  ;; Toolbar: needs alteration for non-scripting mode!
-  ;;  (if (featurep 'proof-toolbar)
-  ;; (proof-toolbar-setup))
-  ;;
-			  
-
-  (run-hooks 'thy-mode-hook)
-  (force-mode-line-update)
-  (if (null nomessage)
-      (message
-       (substitute-command-keys 
-	"Isabelle theory-file mode.   Use \\[thy-insert-template] to insert templates; \\[describe-mode] for help.")))
-  )
-
-(defun thy-mode-quiet ()
-  (interactive)
-  (thy-mode t))
-
-
-
-
-;;; "use" and "use_thy" with theory files ========================
-
-;;; FIXME: Isabelle has been improved, so the following code could
-;;; be cleaned up.  Also set variable to allow automatic starting
-;;; of process by reading logic image.
-
-;;; NB: this is a mess at the moment because of the theory file
-;;; naming conventions.  Really we need to parse the theory/ML
-;;; file - yuk!!
-;;; The next version of Isabelle will be more consistent.
-
-;(defun thy-use-file (&optional force-use_thy)
-;  "Send the file of the current buffer to an Isabelle buffer with use_thy or use."
-;  (interactive "P")
-;  (let ((fname (buffer-file-name)))
-;    (if fname
-;	(isa-query-save (current-buffer))
-;      (setq fname
-;	    (or (buffer-file-name)
-;		(read-file-name "Use file: " nil nil t))))
-;    (let*
-;	((has-thy-extn   (string-match "\\.thy$" fname))   ; o/w assume ML.
-;	 (tname          (if has-thy-extn 
-;			     (substring fname 0 -4); cos use_thy is daft!
-;			   fname))
-;	 (use            (if (or has-thy-extn force-use_thy)
-;			     "use_thy"
-;			   "use"))
-;	 (use-thy-string (concat use " \"" tname "\";"))
-;	 (logic (isa-guess-root)))
-;      (thy-send-string logic use-thy-string))))
-
-;(defun thy-use-region (beg end)
-;  "Send the region to an Isabelle buffer, with use"
-;  (interactive "r")
-;  (write-region beg end thy-use-tempname nil 'nomessage)
-;  (let* ((use-thy-string (concat "use \"" thy-use-tempname "\";"))
-;	 (logic (isa-guess-root)))
-;    (thy-send-string logic use-thy-string)))
-
-;(defun thy-copy-region (beg end &optional isa-buffer)
-;  "Copy the region to an Isabelle buffer."
-;  (interactive "r")
-;  (let ((text (buffer-substring beg end))
-;	(logic (isa-guess-root)))
-;    (save-excursion
-;      (thy-send-string logic text))))
-
-;(defun thy-use-line (&optional isabuffer)
-;  "Send the current interactive ML line to an Isabelle buffer.
-;Advance to the next line."
-;  (interactive)
-;  (isa-apply-to-interactive-line 'thy-copy-region))
-
-;(defun thy-send-string (logic text &optional hide)
-;  "Send TEXT to a buffer running LOGIC.
-;If LOGIC is nil, pick the first Isabelle buffer."
-;  (require 'isa-mode)
-;  (setq logic nil) ;;; #### HACK! This all needs changing for single-session.
-;  (let ((cur-frm (selected-frame)))	; Preserve selected frame.
-;    (if logic				; switch to Isabelle buffer, without
-;	(isabelle-session logic)	; raising the frame.
-;					; (NB: this fails if was renamed).
-;      (set-buffer
-;       (or (car-safe (isa-find-buffers-in-mode 'isa-mode))
-;	   (error "Can't find an Isabelle buffer"))))
-;    (if hide
-;	(isa-send-string
-;	 (get-buffer-process (current-buffer))
-;	 text)
-;      (isa-insert-ret text))     ; send use command
-;    (select-frame cur-frm)))
-
-(defun thy-proofgeneral-send-string (logic text &optional hide)
-  ;; FIXME -- new function!
-  )
-
-;(defun thy-raise-windows ()
-;  "Raise windows/frames associated with Isabelle session."
-;  (interactive)
-;  (isa-select-buffer isa-session-buffer t)
-;  (let ((raise t))
-;    (mapcar 'isa-display-if-active   
-;	    isa-associated-buffers)))
-
-
-;(defun thy-guess-logic-in-use ()
-;  (if (featurep 'isa-mode)
-;      (let* ((buf (car-safe (isa-find-buffers-in-mode 'isa-mode)))
-;	     (log (and buf
-;		       (save-excursion
-;			 (set-buffer buf)
-;			 isa-logic-name))))
-;	log)
-;    nil))
-
-
-;(defvar thy-use-tempname ".region.ML"
-;  "*Name of temporary file to hold region dring thy-use-region.")
-
-
-;(defconst thy-logic-image-regexp
-;  "[lL][oO][gG][iI][cC] [iI][mM][aA][gG][eE]:[ \t]*\"?\\([^ \t\n\"]+\\)\"?[ \t]*$"
-;  "Regexp for locating name of logic image file in a .thy or .ML file.")
-
-;(defvar isa-logic-parents
-;  ;; I can't be bothered to write all of them in here,
-;  ;; and anyway they're ambiguous.  Use "Logic image:"
-;  ;; instead.  (Or find a way of getting emacs to track
-;  ;; theory structure...)
-;  '(("List" . "HOL") ("Prod" . "HOL") ("Nat" . "HOL")
-;    ("Ord" . "HOL") ("Set" ."HOL") ("Sexp" . "HOL")
-;    ("Univ" . "HOL") ("WF" . "HOL") ("Sum" . "HOL")
-;    ("IFOL" . "FOL"))
-;  "*An alist of parents of theories that live in logic files.")
-
-;(defun isa-guess-root ()
-;  "Guess the root logic of the .thy or .ML file in current buffer.
-;Choice based on first name found by:
-;  (i) special text: \"Logic Image: <name>\" toward start of file
-; (ii) guess work based on parent in THY = <parent> if a .thy file."
-;  (save-excursion
-;    (goto-char (point-min))
-;    (cond
-;     ((re-search-forward thy-logic-image-regexp 500 t)
-;      (buffer-substring (match-beginning 1) (match-end 1)))
-;     ((and (string-match "\\.thy$" (or (buffer-file-name) ""))
-;	   (re-search-forward 
-;	    "\\w+[ \t\n]*=[ \t\n]*\\(\\w+\\)[ \t\n]*\\+") 500 t)
-;      ;; Something looks like a parent theory:
-;      ;; 		MyThy = HOL + ...
-;      (let ((child
-;	     (buffer-substring (match-beginning 1) (match-end 1))))
-;	    (or (cdr-safe (assoc child isa-logic-parents))
-;		child))))))
-
-;(defun isa-query-save (buffer)
-;  (and (buffer-modified-p buffer)
-;       (y-or-n-p (concat "Save file "
-;			 (buffer-file-name buffer)
-;			 "? "))
-;       (save-excursion (set-buffer buffer) (save-buffer))))
-
-
-
-
-;;; Interfacing with sml-mode ========================
-
-;; extending sml-mode. This only works if you visit the theory file 
-;; (or start Isabelle mode) first.
-;; This is probably fairly close to The Right Thing...
-
-(defun isa-sml-hook ()
-  "Hook to customize sml-mode for use with Isabelle."
-  ;(isa-menus)				; Add Isabelle main menu
-  ;; NB: these keydefs will affect other sml-mode buffers too!
-  (define-key sml-mode-map "\C-c\C-o" 'thy-find-other-file)
-  ; Disabled for proof general 
-  ;(define-key sml-mode-map "\C-c\C-u" 'thy-use-file)
-  ;(define-key sml-mode-map "\C-c\C-r" 'thy-use-region)
-  ;(define-key sml-mode-map "\C-c\C-l" 'thy-use-line)
-  ;; listener minor mode removed: \C-c\C-c freed up
-  (define-key sml-mode-map "\C-c\C-t" 'thy-insert-id-header))
-
-(add-hook 'sml-mode-hook 'isa-sml-hook)
-
-(defun isa-sml-mode ()
-  "Invoke sml-mode after installing Isabelle hook."
-  (interactive)
-  (and (fboundp 'sml-mode) (sml-mode)))
-
-(defcustom isa-ml-file-extension ".ML"
-  "*File name extension to use for ML files."
-  :type 'string
-  :group 'isabelle)
-
-(defun thy-find-other-file (&optional samewindow)
-  "Find associated .ML or .thy file.
-Finds and switch to the associated ML file (when editing a theory file)
-or theory file (when editing an ML file).  
-If SAMEWINDOW is non-nil (interactively, with an optional argument)
-the other file replaces the one in the current window."
-  (interactive "p")
-  (and 
-   (buffer-file-name)
-   (let* ((fname     (buffer-file-name))
-	  (thyfile   (string-match "\\.thy$" fname))
-	  (mlfile    (string-match
-		      (concat (regexp-quote isa-ml-file-extension) "$") fname))
-	  (basename  (file-name-sans-extension fname))
-	  (findfn    (if samewindow 'find-file else 'find-file-other-window)))
-     (cond (thyfile
-	    (funcall findfn (concat basename isa-ml-file-extension)))
-	   (mlfile
-	    (funcall findfn (concat basename ".thy")))))))
-  
-
-;;; "minor" sml-mode inside theory files ==========
-
-(defvar thy-minor-sml-mode-map nil)
-
-(defun thy-install-sml-mode ()
-  (progn
-    (require 'sml-mode)
-    (setq thy-minor-sml-mode-map (copy-keymap sml-mode-map))
-    ;; Bind TAB to what it should be in sml-mode.
-    (define-key thy-minor-sml-mode-map "\t" 'indent-for-tab-command)
-    (define-key thy-minor-sml-mode-map "\C-c\C-m" 'thy-mode-quiet)
-    (define-key thy-minor-sml-mode-map "\C-c\C-t" 'thy-insert-template)))
-
-(defun thy-minor-sml-mode ()
-  "Invoke sml-mode as if a minor mode inside a theory file.
-This has no effect if thy-use-sml-mode is nil."
-  (interactive)
-  (if thy-use-sml-mode
-      (progn
-	(if (not (boundp 'sml-mode)) 
-	    (thy-install-sml-mode))
-	(kill-all-local-variables)
-	(sml-mode)					; Switch to sml-mode
-	(setq major-mode 'thy-mode)
-	(setq mode-name "Theory Sml")			; looks like it's a minor-mode.
-	(use-local-map thy-minor-sml-mode-map)	; special map has \C-c\C-c binding.
-	(make-local-variable 'indent-line-function)
-	(setq indent-line-function 'thy-do-sml-indent)
-	(force-mode-line-update)
-	(message "Use C-c C-c to exit SML mode."))))
-
-(defun thy-do-sml-indent ()
-  "Run sml-indent-line in an Isabelle theory file, provided inside ML section.
-If not, will turn off simulated minor mode and run thy-indent-line."
-  (interactive)
-  (if (string= (thy-current-section) "ML")		; NB: Assumes that TAB key was 
-      (sml-indent-line)					; bound to sml-indent-line.
-    (thy-mode t)					; (at least, it is now!).
-    (thy-indent-line)))
-
-
-(defun thy-insert-name (name)
-  "Insert NAME -- as a string if there are non-alphabetic characters in NAME."
-  (if (string-match "[a-zA-Z]+" name)
-      (insert name)
-    (insert "\"" name "\"")))
-
-(defun thy-insert-class (name supers)
-  (interactive 
-   (list
-    (isa-read-id "Class name: ")
-    (isa-read-idlist "Super classes %s: ")))
-  (insert name)
-  (if supers (insert "\t< " (isa-splice-separator ", " supers)))
-  (indent-according-to-mode)
-  (forward-line 1))
-
-(defun thy-insert-default-sort (sort)
-  (interactive
-   (list
-    (isa-read-id "Default sort: ")))
-  (insert sort)
-  (indent-according-to-mode)
-  (thy-goto-next-section))
-
-(defun thy-insert-type (name no-of-args)
-  (interactive
-   (list
-    (isa-read-id  "Type name: ")
-    (isa-read-num "Number of arguments: ")))
-  ;; make type variables for arguments. Daft things for >26!
-  (cond 
-   ((zerop no-of-args))
-   ((= 1 no-of-args)  
-    (insert "'a "))
-   (t 
-    (insert "(")
-    (let ((i 0))
-      (while (< i no-of-args)
-	(if (> i 0) (insert ","))
-	(insert "'" (+ ?a i))
-	(setq i (1+ i))))
-    (insert ") ")))
-  (thy-insert-name name)
-  (indent-according-to-mode)
-  ;; forward line, although use may wish to add infix.
-  (forward-line 1))
-
-(defun thy-insert-arity (name param-sorts result-class)
-  (interactive
-   (list
-    (isa-read-id "Type name: ")
-    (isa-read-idlist "Parameter sorts %s: ")
-    (isa-read-id "Result class: ")))
-  (insert name " :: ")
-  (if param-sorts 
-      (insert "(" (isa-splice-separator ", " param-sorts) ") "))
-  (insert result-class)
-  (indent-according-to-mode)
-  (forward-line 1))
-
-(defun thy-insert-const (name type)
-  ;; only does a single constant, no lists.
-  (interactive
-   (let* ((thename  (isa-read-id "Constant name: "))
-	  (thetype  (isa-read-string (format "Type of `%s' : " thename))))
-     (list thename thetype)))
-  (thy-insert-name name)
-  (insert " ::\t \"" type "\"\t\t")
-  (indent-according-to-mode)
-  ;; no forward line in case user adds mixfix
-  )
-  
-(defun thy-insert-rule (name)
-  (interactive 
-   (list
-    (isa-read-id "Axiom name: ")))
-  (end-of-line 1)
-  (insert name "\t\"\"")
-  (backward-char)
-  (indent-according-to-mode))
-
-(defun thy-insert-template ()
-  "Insert a syntax template according to the current section"
-  (interactive)
-  (thy-check-mode)
-  (let* ((sect (thy-current-section))
-	 (tmpl (cdr-safe (assoc sect thy-sections))))
-    ;; Ensure point is at start of an empty line.
-    (beginning-of-line)
-    (skip-chars-forward "\t ")
-    (if (looking-at sect) 
-	(progn 
-	  (forward-line 1) 
-	  (skip-chars-forward "\t ")))
-    (if (looking-at "$")
-	nil
-      (beginning-of-line)
-      (newline)
-      (forward-line -1))
-    (cond ((stringp tmpl)
-	   (insert tmpl)
-	   (indent-according-to-mode))
-	  ((null tmpl))		; nil is a symbol!
-	  ((symbolp tmpl)
-	   (call-interactively tmpl)))))
-
-;;; === Functions for reading from the minibuffer.
-;;;
-
-; These could be improved, e.g. to enforce syntax for identifiers.
-; Unfortunately, Xemacs, and now Emacs too, lack a 
-; read-no-blanks-input function!
-
-(defun isa-read-idlist (prompt &optional init)
-  "Read a list of identifiers from the minibuffer."
-  (let ((items init) item)
-    (while (not (string= ""
-			 (setq item (read-string 
-				       (format prompt (or items ""))))))
-      (setq items (nconc items (list item))))
-    items))
-
-(defun isa-read-id (prompt &optional init)
-  "Read an identifier from the minibuffer."
-  ;; don't allow empty input
-  (let ((result ""))
-    (while (string= result "")
-      (setq result (read-string prompt init)))
-    result))
-
-(defun isa-read-string (prompt &optional init)
-  "Read a non-empty string from the minibuffer"
-  ;; don't allow empty input
-  (let ((result ""))
-    (while (string= result "")
-      (setq result (read-string prompt init)))
-    result))
-
-(defun isa-read-num (prompt)
-  "Read a number from the minibuffer."
-  (read-number prompt t))
-
-;(defun thy-read-thy-name ()
-;  (let* ((default  (car 
-;		    (isa-file-name-cons-extension
-;		     (file-name-nondirectory 
-;		      (abbreviate-file-name (buffer-file-name)))))))
-;    default))
-
-(defun thy-read-thy-name ()
-  (let* ((default  (car 
-		    (isa-file-name-cons-extension
-		     (file-name-nondirectory 
-		      (abbreviate-file-name (buffer-file-name))))))
-	 (name     (read-string 
-		    (format "Name of theory [default %s]: " default))))
-    (if (string= name "") default name)))
-
-(defun thy-read-logic-image ()
-  (let*	((defimage "Pure")
-	   ;; (or (thy-guess-logic-in-use)
-	   ;; "Pure"))
-	   
-	 (logic    (read-string
-		    (format "Name of logic image to use [default %s]: "
-			    defimage))))
-    (if (string= logic "") defimage logic)))
-
-(defun thy-insert-header (name logic parents)
-  "Insert a theory file header, for LOGIC, theory NAME with PARENTS"
-  (interactive 
-   (list
-    (thy-read-thy-name)
-    (thy-read-logic-image)
-    (isa-read-idlist "Parent theory %s: ")))
-  (let* ((parentplus (isa-splice-separator 
-		      " + " 
-		      (or parents (list (or logic "Pure")))))
-	 (formalist (list
-		       (cons "%t" name)
-		       (cons "%p" parentplus))))
-    (thy-insert-id-header name logic)
-    (insert (isa-format formalist thy-template)))
-  (goto-char (point-min))
-  (thy-goto-next-section))
-
-(defun thy-insert-id-header (name logic)
-  "Insert an identification header, for theory NAME logic image LOGIC."
-  (interactive
-   (list
-    (thy-read-thy-name)
-    (thy-read-logic-image)))
-  (let* ((formalist (list
-		     (cons "%f" (buffer-file-name))
-		     (cons "%t" name)
-		     (cons "%l" logic))))
-    (insert (isa-format formalist thy-id-header))))
-
-(defun thy-check-mode ()
-  (if (not (eq major-mode 'thy-mode))
-      (error "Not in Theory mode.")))
-  
-
-(defconst thy-headings-regexp
-  (concat
-   "^\\s-*\\("
-   (substring (apply 'concat (mapcar 
-			      '(lambda (pair)
-				 (concat "\\|" (car pair)))
-			      (cdr thy-sections))) 2)
-   "\\)[ \t]*")
-  "Regular expression matching headings in theory files.")
-
-(defvar thy-mode-font-lock-keywords
-  (list				
-   (list (proof-ids-to-regexp
-	  (append '("infixl" "infixr" "binder") 
-		  (mapcar 'car (cdr thy-sections))))
-	 0 'font-lock-keyword-face)
-   ;; FIXME: needs more work.  Get symbols in quotes, etc, etc.
-   (list "\\s-*\\(\\w+\\)\\s-*\\(::?\\)"
-	 2 'font-lock-preprocessor-face)
-   (list "\\s-*\\(\\w+\\)\\s-*::?"
-	 1 'font-lock-variable-name-face)
-   (list "\".*\"\\s-*\\(::?\\)"
-	 1 'font-lock-preprocessor-face)
-   (list "\"\\(.*\\)\"\\s-*\\(::?\\)"
-	 1 'font-lock-variable-name-face))
-;   (list "^\\s-*\\(\\w*\\)\\s-*\\(::\\)"
-;	 1 'font-lock-function-name-face
-;	 2 'font-lock-preprocessor-face))
-  "Font lock keywords for thy-mode.")
-
-;;; movement between sections ===================================    
-
-(defun thy-goto-next-section (&optional count noerror)
-  "Goto the next (or COUNT'th next) section of a theory file.
-Negative value for count means previous sections.
-If NOERROR is non-nil, failed search will not be signalled."
-  (interactive "p")
-  (condition-case nil
-      ;; string matching would probably be good enough
-      (cond ((and count (< count 0))
-	     (let ((oldp (point)))
-	       (beginning-of-line)
-	       (thy-goto-top-of-section)
-	       ;; not quite right here - should go to top
-	       ;; of file, like top of section does.
-	       (if (equal (point) oldp)
-		   (progn
-		     (re-search-backward thy-headings-regexp 
-					 nil nil (1+ (- count)))
-		     (forward-line 1))))
-	     t)
-	    (t
-	     (re-search-forward thy-headings-regexp nil nil count)
-	     (forward-line 1)
-	     t))
-    ;; could just move to top or bottom if this happens, instead
-    ;; of giving this error.
-    (search-failed (if noerror nil
-		     (error "No more headings")))))
-
-(defun thy-goto-prev-section (&optional count noerror)
-  "Goto the previous section (or COUNT'th previous) of a theory file.
-Negative value for count means following sections.
-If NOERROR is non-nil, failed search will not be signalled."
-  (interactive)
-  (thy-goto-next-section (if count (- count) -1) noerror))
-
-(defun thy-goto-top-of-section ()
-  "Goto the top of the current section"
-  (interactive)
-  (if (re-search-backward thy-headings-regexp nil t)
-      (forward-line 1)
-    (goto-char (point-min))))
-
-(defun thy-current-section ()
-  "Return the current section of the theory file, as a string.
-\"top\" indicates no section."
-  (save-excursion
-    (let* ((gotsect (re-search-backward thy-headings-regexp nil t))
-	   (start   (if gotsect
-			(progn
-			  (skip-chars-forward " \t")
-			  (point)))))
-      (if (not start)
-	  "top"
-	(skip-chars-forward "a-zA-z")
-	(buffer-substring start (point))))))
-
-
-
-;;; kill line ==================================================
-
-(defun thy-kill-line (&optional arg)
-  "As kill-line, except in a string will kill continuation backslashes also.
-Coalesces multiple lined strings by leaving single spaces."
-  (interactive "P")
-  (let ((str           (thy-string-start))
-	(kill-start    (point))
-	following-slash)
-    (if (not str)
-	;; Usual kill line if not inside a string.
-	(kill-line arg)
-      (if arg
-	  (forward-line (prefix-numeric-value arg))
-	(if (eobp)
-	    (signal 'end-of-buffer nil)))
-      (setq kill-start (point))
-      (if (thy-string-start str)		; if still inside a string
-	  (cond 
-	   ((looking-at "[ \t]*$")	; at end of line bar whitespace
-	    (skip-chars-backward 
-	     " \t"
-	     (save-excursion (beginning-of-line) (1+ (point))))
-	    (backward-char)
-	    (if (looking-at "\\\\")	; preceding backslash
-		(progn
-		  (skip-chars-backward " \t")
-		  (setq following-slash t)
-		  (setq kill-start (min (point) kill-start)))
-	      (goto-char kill-start))
-	    (forward-line 1))
-	   ((looking-at "[ \t]*\\\\[ \t]*$") ; before final backslash
-	    (setq following-slash t)
-	    (forward-line 1))
-	   ((looking-at "\\\\[ \t]*\\\\[ \t]*$") ; an empty line!
-	    (forward-line 1))
-	   ((looking-at ".*\\(\\\\\\)[ \t]*$")	; want to leave backslash
-	    (goto-char (match-beginning 1)))
-	   ((and kill-whole-line (bolp))
-	    (forward-line 1))
-	   (t
-	    (end-of-line))))
-      (if (and following-slash 
-	       (looking-at "[ \t]*\\\\"))	; delete following slash if
-	  (goto-char (1+ (match-end 0)))) ; there's one
-      (kill-region kill-start (point))	; do kill
-      (if following-slash
-	  ;; did do just-one-space, but it's not nice to delete backwards
-	  ;; too
-	  (delete-region (point)
-			 (save-excursion
-			   (skip-chars-forward " \t")
-			   (point)))))))
-
-
-;;; INDENTATION ==================================================
-  
-;;; Could do with thy-correct-string function,
-;;; which does roughly the same as indent-region.
-;;; Then we could have an electric " that did this!
-
-;;; Could perhaps have used fill-prefix to deal with backslash
-;;; indenting, rather than lengthy code below?
-
-(defun thy-indent-line ()
-  "Indent the current line in an Isabelle theory file.
-If in the ML section, this switches into a simulated minor sml-mode."
-  (let ((sect (thy-current-section)))
-    (cond 
-     ((and thy-use-sml-mode (string= sect "ML"))
-      (progn				               ; In "ML" section,
-	(thy-minor-sml-mode)	               ; switch to sml mode.
-	(sml-indent-line)))
-
-     (t   (let ((indent   (thy-calculate-indentation sect)))
-	    (save-excursion
-	      (beginning-of-line)
-	      (let ((beg (point)))
-		(skip-chars-forward "\t ")
-		(delete-region beg (point)))
-	      (indent-to indent))
-	    (if (< (current-column) 
-		   (current-indentation))	
-		(skip-chars-forward "\t ")))))))
-
-;; Better Emacs major modes achieve a kind of "transparency" to
-;; the user, where special indentation,etc. happens under your feet, but
-;; in a useful way that you soon get accustomed to.  Worse modes
-;; cause frustration and repetitive re-editing of automatic indentation.
-;; I hope I've achieved something in the first category...
-
-(defun thy-calculate-indentation (sect)
-  "Calculate the indentation for the current line.
-SECT should be the string name of the current section."
-  (save-excursion
-    (beginning-of-line)
-    (or (thy-long-comment-string-indentation)
-	(if (looking-at "\\s-*$")
-	    ;; Empty lines use indentation for section.
-	    (thy-indentation-for sect)
-	  (if (looking-at thy-headings-regexp)
-	      thy-heading-indent
-	    (progn
-	      (skip-chars-forward "\t ")
-	      (cond
-	       ;; A comment?
-	       ((looking-at "(\\*")         
-		(thy-indentation-for sect))
-	       ;; Anything else, use indentation for section
-	       (t (thy-indentation-for sect)))))))))
-
-(defun thy-long-comment-string-indentation ()
-  "Calculate the indentation if inside multi-line comment or string.
-Also indent string contents."
-  (let* ((comstr (thy-comment-or-string-start))
-	 (bolpos (save-excursion
-		   (beginning-of-line)
-		   (point)))
-	 (multi  (and comstr 
-		      (< comstr bolpos))))
-    (if (not multi)
-	nil		
-      (save-excursion
-	(beginning-of-line)
-	(cond
-
-	 ;; Inside a comment?
-	 ((char-equal (char-after comstr) ?\( )
-	  (forward-line -1)
-	  (if (looking-at "[\t ]*(\\*")
-	      (+ 3 (current-indentation))
-	    (current-indentation)))
-	 
-	 ;; Otherwise, a string.
-	 ;; Enforce correct backslashing on continuing
-	 ;; line and return cons of backslash indentation
-	 ;; and string contents indentation for continued
-	 ;; line.
-	 (t
-	  (let ((quote-col (save-excursion (goto-char comstr) 
-					   (current-column))))
-	     (if thy-indent-strings
-		(thy-string-indentation comstr)
-	      ;; just to right of matching " 
-	      (+ quote-col 1)))))))))
-
-(defun thy-string-indentation (start)
-  ;; Guess indentation for text inside a string
-  (let* ((startcol  (save-excursion (goto-char start) (current-column)))
-	 (pps-state (parse-partial-sexp (1+ start) (point)))
-	 (par-depth (car pps-state)))
-	 (cond (;; If not in nested expression, startcol+1
-		(zerop par-depth)
-		(1+ startcol))
-	       (;; If in a nested expression, use position of opening bracket
-		(natnump par-depth)
-		(save-excursion
-		  (goto-char (nth 1 pps-state))
-		  (+ (current-column)
-		     (cond ((looking-at "\\[|") 3)
-			   (t 1)))))
-	       (;; Give error for too many closing parens
-		t
-		(error "Mismatched parentheses")))))
-
-(defun thy-indentation-for (sect)
-  "Return the indentation for section SECT"
-  (if (string-equal sect "top")
-      thy-heading-indent
-    thy-indent-level))
-
-(defun thy-string-start (&optional min)
-  "Return position of start of string if inside one, nil otherwise."
-  (let ((comstr (thy-comment-or-string-start)))
-    (if (and comstr
-	     (save-excursion
-	       (goto-char comstr)
-	       (looking-at "\"")))
-	comstr)))
-
-;;; Is this parsing still too slow?  (better way? e.g., try setting
-;;; variable "char" and examining it, rather than finding current
-;;; state first - fewer branches in non-interesting cases, perhaps.
-;;; NB: it won't understand escape sequences in strings, such as \"
-
-(defun thy-comment-or-string-start (&optional min)
-  "Find if point is in a comment or string, starting parse from MIN.
-Returns the position of the comment or string start or nil.
-If MIN is nil, starts from top of current section.
-
-Doesn't understand nested comments."
-  (or min
-      (setq min
-	    (save-excursion
-	      (thy-goto-top-of-section) (point))))
-  (if (<= (point) min)
-      nil
-    (let ((pos   (point))
-	  (incomdepth 0)
-	  incom instring)  ; char
-      (goto-char min)
-      (while (< (point) pos)
-	;; When inside a string, only look for its end
-	(if instring
-	    (if (eq (char-after (point)) ?\") ; looking-at "\""
-		(setq instring nil))
-	  ;; If inside a comment, look for a comment end
-	  (if (> 0 incomdepth)	
-	      (if (and			; looking-at "\\*)"
-		   (eq (char-after (point)) ?\*)
-		   (eq (char-after (1+ (point))) ?\)))
-		  (setq incomdepth (1- incomdepth)))
-	    ;; If inside neither comment nor string, look for 
-	    ;; a string start.
-	    (if (eq (char-after (point)) ?\") ; looking-at "\""
-		(setq instring (point))))
-	  ;; Look for a comment start (unless inside a string)
-	  (if (and
-	       (eq (char-after (point)) ?\()
-	       (eq (char-after (1+ (point))) ?\*))
-	      (progn
-		(if (= 0 incomdepth)	; record start of main comment
-		    (setq incom (point))) ; only
-		(setq incomdepth (1+ incomdepth)))))
-	(forward-char))
-      (if (> 0 incomdepth) incom instring))))
-
-
-
-
-(provide 'thy-mode)
-
-;;; end of thy-mode.el
diff --git a/isa/todo b/isa/todo
deleted file mode 100644
index e4964429..00000000
--- a/isa/todo
+++ /dev/null
@@ -1,62 +0,0 @@
--*- mode:outline -*-
-
-* Things to do for Isabelle
-
-See also ../todo for generic things to do, priority codes.
-
-See also ../isar/todo.  Isar is now main instance for PG, this
-instance less supported.
-
-
-** X Isabelle PG: Non-blocking for .thy loading from .ML files.
-
-** D Isabelle: I think show_sorts -> show_types, how can we reflect this ?
-
-** D Fix mode naming for Isabelle 
-     (might like isa-proofscript-mode -> isa-mode;
-      but this conflicts with entry mechanism for thy/isa mode).
-
-** D Might be nice to unify menus a little more, e.g. add Isabelle for .thy
-
-   But several of the ops there are not relevant for theory files.
-   Well, favourites at least.  What we have at the moment is verging
-   GUI-atrocity: one shouldn't have menus of the same name with
-   different entries, but should rather use greyed out.
-
-** C Improvements to Isabelle that would be nice for Proof General:
-
-   -- ability to remove theorem from theorem database, issued
-   when undoing qed
-
-
-** C X-Symbol support for theory files: bugs at the moment, because
-  of duplicate calls to proof-x-symbol-mode and mess with
-  font-lock initialization.  Problem with current version:
-  visit a.thy, b.thy then turn on xsym.  Broken in b.thy.
-  Seems okay visiting new buffers after that.
-  Must also check interaction with xsym-isa-latex stuff
-  may be broken by removal of mode hook settings.
-  [DvO reports okay].
-  (May need to split extra modes into two parts?)
-
-** B auto-adjust Pretty.setmargin when window is resized.  Use
-  generic code once it's implemented.
-
-** D Implement completion for Isabelle using tables generated by
-  the running process.  Ideally context sensitive.
-  Would be a nice addition. (1 week)
-
-** D Add useful specific commands for Isabelle.  Many could
-  be added.  Would be better to merge in Isamode's menus.
-  (however, probably 2 week's work to bring together Isamode 
-   and proof.el, making some of Isamode generic)
-
-** D Switching to other file with C-c C-o could be more savy
-  with file names and extensions (use some standard function?)
-
-** X Write perl scripts to generate TAGS file for ML and thy files.
-  (60h, any volunteers?) (hard);
-
-** X Manage multiple proofs, perhaps by automatically inserting
-  push_proof() and pop_proof() commands into the proof script.
-  But would lead to unholy mess for script management! (hard!)
diff --git a/isa/x-symbol-isa.el b/isa/x-symbol-isa.el
deleted file mode 100644
index f5934f52..00000000
--- a/isa/x-symbol-isa.el
+++ /dev/null
@@ -1,21 +0,0 @@
-;; Canonical file for token language file for PG/isar.
-
-(require 'x-symbol-isabelle)
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; x-symbol support for Isabelle PG, provided by David von Oheimb.
-;;
-;; The following settings configure the generic PG package.
-;; The token language "Isabelle Symbols" is in file x-symbol-isabelle.el
-;;
-
-(setq proof-xsym-extra-modes '(thy-mode)
-      proof-xsym-activate-command
-      "change print_mode (insert (op =) \"xsymbols\");"
-      proof-xsym-deactivate-command
-      "change print_mode (remove (op =) \"xsymbols\");")
-
-
-
-(provide 'x-symbol-isa)
diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el
deleted file mode 100644
index 58233920..00000000
--- a/isa/x-symbol-isabelle.el
+++ /dev/null
@@ -1,514 +0,0 @@
-;; x-symbol-isabelle.el   
-;;	Token language "Isabelle Symbols" for package x-symbol
-;;
-;;  ID:         $Id$
-;;  Author:     David von Oheimb
-;;              Updates by Markus Wenzel, Christoph Wedler, David Aspinall.
-;;  Copyright   1998 Technische Universitaet Muenchen
-;;  License     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;;
-;; NB: Part of Proof General distribution.
-;;
-;; This file accounts for differences between Isabelle and 
-;; Isabelle/Isar support of X-Symbol tokens, namely:
-;;
-;; Isabelle:       \\<foo>   (inside ML strings)
-;; Isabelle/Isar:  \<foo>
-;;
-
-(defvar x-symbol-isabelle-required-fonts nil)
-
-;;;===========================================================================
-;;;  General language accesses, see `x-symbol-language-access-alist'
-;;;===========================================================================
-
-;; NB da: these next two are also set in proof-x-symbol.el, but
-;; it would be handy to be able to use this file away from PG.  
-(defvar x-symbol-isabelle-name "Isabelle Symbol")
-(defvar x-symbol-isabelle-modeline-name "isa")
-
-(defcustom x-symbol-isabelle-header-groups-alist nil
-   "*If non-nil, used in isasym specific grid/menu.
-See `x-symbol-header-groups-alist'."
-  :group 'x-symbol-isabelle
-  :group 'x-symbol-input-init
-  :type 'x-symbol-headers)
-
-(defcustom x-symbol-isabelle-electric-ignore 
-  "[:'][A-Za-z]\\|<=\\|\\[\\[\\|\\]\\]\\|~="
-  "*Additional Isabelle version of `x-symbol-electric-ignore'."
-  :group 'x-symbol-isabelle
-  :group 'x-symbol-input-control
-  :type 'x-symbol-function-or-regexp)
-
-
-(defvar x-symbol-isabelle-required-fonts nil
-  "List of features providing fonts for language `isabelle'.")
-
-(defvar x-symbol-isabelle-extra-menu-items nil
-  "Extra menu entries for language `isabelle'.")
-
-
-(defvar x-symbol-isabelle-token-grammar
-  '(x-symbol-make-grammar
-    :encode-spec (((t . "\\\\")))
-    :decode-regexp "\\\\+<[A-Za-z]+>"
-    :input-spec nil
-    :token-list x-symbol-isabelle-token-list))
-
-(defun x-symbol-isabelle-token-list (tokens)
-  (mapcar (lambda (x) (cons x t)) tokens))
-
-(defvar x-symbol-isabelle-user-table nil
-  "User table defining Isabelle commands, used in `x-symbol-isabelle-table'.")
-
-(defvar x-symbol-isabelle-generated-data nil
-  "Internal.")
-
-
-;;;===========================================================================
-;;;  No image support
-;;;===========================================================================
-
-(defvar x-symbol-isabelle-master-directory  'ignore)
-(defvar x-symbol-isabelle-image-searchpath '("./"))
-(defvar x-symbol-isabelle-image-cached-dirs '("images/" "pictures/"))
-(defvar x-symbol-isabelle-image-file-truename-alist nil)
-(defvar x-symbol-isabelle-image-keywords nil)
-
-
-;;;===========================================================================
-;;  super- and subscripts
-;;;===========================================================================
-
-;; one char: \<^sup>, \<^sub>, \<^isub>, and \<^isup>
-;; spanning: \<^bsup>...\<^esup> and \<^bsub>..\<^esub>
-
-(defcustom x-symbol-isabelle-subscript-matcher 'x-symbol-isabelle-subscript-matcher
-  "Function matching super-/subscripts for language `isa'.
-See language access `x-symbol-LANG-subscript-matcher'."
-  :group 'x-symbol-isabelle
-  :type 'function)
-
-(defcustom x-symbol-isabelle-font-lock-regexp "\\\\<\\^[ib]?su[bp]>"
-  "Regexp matching the start tag of Isabelle super- and subscripts."
-  :group 'x-symbol-isabelle
-  :type 'regexp)
-
-(defcustom x-symbol-isabelle-font-lock-limit-regexp "\n\\|\\\\<\\^[be]su[bp]>"
-  "Regexp matching the end of line and the start and end tags of Isabelle
-spanning super- and subscripts."
-  :group 'x-symbol-isabelle
-  :type 'regexp)
-
-(defcustom x-symbol-isabelle-font-lock-contents-regexp "."
-  "*Regexp matching the spanning super- and subscript contents.
-This regexp should match the text between the opening and closing super-
-or subscript tag."
-  :group 'x-symbol-isabelle  
-  :type 'regexp)
-
-
-;; the [\350-\357].\350\\|\^A[A-H].\^AA part is there to enable single
-;; char sub/super scripts with coloured Isabelle output.
-(defcustom x-symbol-isabelle-single-char-regexp 
-  "[\350-\357].\350\\|\^A[A-H].\^AA\\|[^\\]\\|\\\\\\\\?<[A-Za-z0-9_']+>"
-  "Return regexp matching \<ident> or c for some char c."
-  :group 'x-symbol-isabelle
-  :type 'regexp)
-
-(defun x-symbol-isabelle-subscript-matcher (limit)  
-  (block nil
-    (let (open-beg open-end close-end close-beg script-type)
-      (while (re-search-forward x-symbol-isabelle-font-lock-regexp limit t)
-        (setq open-beg (match-beginning 0)
-              open-end (match-end 0)
-              script-type (if (eq (char-after (- open-end 2)) ?b)
-                              'x-symbol-sub-face
-                           'x-symbol-sup-face))
-        (if (eq (char-after (- open-end 5)) ?b) ; if is spanning sup-/subscript
-            (let ((depth 1)) ; level of nesting
-              (while (and (not (eq depth 0))
-                          (re-search-forward x-symbol-isabelle-font-lock-limit-regexp
-                                             limit 'limit))
-                (setq close-beg (match-beginning 0)
-                      close-end (match-end 0))
-                (if (eq (char-after (- close-end 1)) ?\n) ; if eol
-                    (setq depth 0)
-                  (if (eq (char-after (- close-end 5)) ?b) ; if end of span
-                      (setq depth (+ depth 1))
-                    (setq depth (- depth 1)))))
-              (when (eq depth 0)
-                (when
-                    (save-excursion
-                      (goto-char open-end)
-                      (re-search-forward x-symbol-isabelle-font-lock-contents-regexp
-                                         close-beg t))
-                  (store-match-data (list open-beg close-end
-                                          open-beg open-end
-                                          open-end close-beg
-                                          close-beg close-end))
-                  (return script-type)))
-              (goto-char close-beg))
-          (when (re-search-forward x-symbol-isabelle-single-char-regexp
-                                   limit 'limit)
-            (setq close-end (match-end 0))
-            (store-match-data (list open-beg close-end
-                                    open-beg open-end
-                                    open-end close-end))
-            (return script-type))
-      )))))
-   
-(defun isabelle-match-subscript (limit)
-  (if (proof-ass x-symbol-enable)
-      (setq x-symbol-isabelle-subscript-type
-            (funcall x-symbol-isabelle-subscript-matcher limit))))
-
-;; these are used for Isabelle output only. x-symbol does its own
-;; setup of font-lock-keywords for the theory buffer
-;; (x-symbol-isabelle-font-lock-keywords does not belong to language
-;; access any more)
-(defvar x-symbol-isabelle-font-lock-keywords
-  '((isabelle-match-subscript
-     (1 x-symbol-invisible-face t)
-     (2 (progn x-symbol-isabelle-subscript-type) prepend)
-     (3 x-symbol-invisible-face t t)))
-  "Isabelle font-lock keywords for super- and subscripts.")
-
-(defvar x-symbol-isabelle-font-lock-allowed-faces t)
-
-
-;;;===========================================================================
-;;;  Charsym Info
-;;;===========================================================================
-
-(defcustom x-symbol-isabelle-class-alist
-  '((VALID "Isabelle Symbol" (x-symbol-info-face))
-    (INVALID "no Isabelle Symbol" (red x-symbol-info-face)))
-  "Alist for Isabelle's token classes displayed by info in echo area.
-See `x-symbol-language-access-alist' for details."
-  :group 'x-symbol-texi
-  :group 'x-symbol-info-strings
-;;  :set 'x-symbol-set-cache-variable   [causes compile error]
-  :type 'x-symbol-class-info)
-
-
-(defcustom x-symbol-isabelle-class-face-alist nil
-  "Alist for Isabelle's color scheme in TeXinfo's grid and info.
-See `x-symbol-language-access-alist' for details."
-  :group 'x-symbol-isabelle
-  :group 'x-symbol-input-init
-  :group 'x-symbol-info-general
-;;  :set 'x-symbol-set-cache-variable   [causes compile error]
-  :type 'x-symbol-class-faces)
-
-
-
-;;;===========================================================================
-;;;  The tables
-;;;===========================================================================
-
-(defvar x-symbol-isabelle-case-insensitive nil)
-(defvar x-symbol-isabelle-token-shape nil)
-(defvar x-symbol-isabelle-input-token-ignore nil)
-(defvar x-symbol-isabelle-token-list 'identity)
-
-(defvar x-symbol-isabelle-symbol-table      ; symbols (isabelle font)
-  '((visiblespace "\\<spacespace>")
-    (Gamma "\\<Gamma>")
-    (Delta "\\<Delta>")
-    (Theta "\\<Theta>")
-    (Lambda "\\<Lambda>")
-    (Pi "\\<Pi>")
-    (Sigma "\\<Sigma>")
-    (Phi "\\<Phi>")
-    (Psi "\\<Psi>")
-    (Omega "\\<Omega>")
-    (alpha "\\<alpha>")
-    (beta "\\<beta>")
-    (gamma "\\<gamma>")
-    (delta "\\<delta>")
-    (epsilon1 "\\<epsilon>")
-    (zeta "\\<zeta>")
-    (eta "\\<eta>")
-    (theta "\\<theta>")
-    (kappa1 "\\<kappa>")
-    (lambda "\\<lambda>")
-    (mu "\\<mu>")
-    (nu "\\<nu>")
-    (xi "\\<xi>")
-    (pi "\\<pi>")
-    (rho1 "\\<rho>")
-    (sigma "\\<sigma>")
-    (tau "\\<tau>")
-    (phi1 "\\<phi>")
-    (chi "\\<chi>")
-    (psi "\\<psi>")
-    (omega "\\<omega>")
-    (notsign "\\<not>")
-    (logicaland "\\<and>")
-    (logicalor "\\<or>")
-    (universal1 "\\<forall>")
-    (existential1 "\\<exists>")
-    (epsilon "\\<some>")
-    (biglogicaland "\\<And>")
-    (ceilingleft "\\<lceil>")
-    (ceilingright "\\<rceil>")
-    (floorleft "\\<lfloor>")
-    (floorright "\\<rfloor>")
-    (bardash "\\<turnstile>")
-    (bardashdbl "\\<Turnstile>")
-    (semanticsleft "\\<lbrakk>")
-    (semanticsright "\\<rbrakk>")
-    (periodcentered "\\<cdot>")
-    (element "\\<in>")
-    (reflexsubset "\\<subseteq>")
-    (intersection "\\<inter>")
-    (union "\\<union>")
-    (bigintersection "\\<Inter>")
-    (bigunion "\\<Union>")
-    (sqintersection "\\<sqinter>")
-    (squnion "\\<squnion>")
-    (bigsqintersection "\\<Sqinter>")
-    (bigsqunion "\\<Squnion>")
-    (perpendicular "\\<bottom>")
-    (dotequal "\\<doteq>")
-    (wrong "\\<wrong>")
-    (equivalence "\\<equiv>")
-    (notequal "\\<noteq>")
-    (propersqsubset "\\<sqsubset>")
-    (reflexsqsubset "\\<sqsubseteq>")
-    (properprec "\\<prec>")
-    (reflexprec "\\<preceq>")
-    (propersucc "\\<succ>")
-    (approxequal "\\<approx>")
-    (similar "\\<sim>")
-    (simequal "\\<simeq>")
-    (lessequal "\\<le>")
-    (coloncolon "\\<Colon>")
-    (arrowleft "\\<leftarrow>")
-    (endash "\\<midarrow>")
-    (arrowright "\\<rightarrow>")
-    (arrowdblleft "\\<Leftarrow>")
-;   (nil "\\<Midarrow>")
-    (arrowdblright "\\<Rightarrow>")
-    (frown "\\<frown>")
-    (mapsto "\\<mapsto>")
-    (leadsto "\\<leadsto>")
-    (arrowup "\\<up>")
-    (arrowdown "\\<down>")
-    (notelement "\\<notin>")
-    (multiply "\\<times>")
-    (circleplus "\\<oplus>")
-    (circleminus "\\<ominus>")
-    (circlemultiply "\\<otimes>")
-    (circleslash "\\<oslash>")
-    (propersubset "\\<subset>")
-    (infinity "\\<infinity>")
-    (box "\\<box>")
-    (lozenge1 "\\<diamond>")
-    (circ "\\<circ>")
-    (bullet "\\<bullet>")
-    (bardbl "\\<parallel>")
-    (radical "\\<surd>")
-    (copyright "\\<copyright>")))
-
-(defvar x-symbol-isabelle-xsymbol-table    ; xsymbols
-  '((Xi "\\<Xi>")
-    (Upsilon1 "\\<Upsilon>")
-    (iota "\\<iota>")
-    (upsilon "\\<upsilon>")
-    (plusminus "\\<plusminus>")
-    (division "\\<div>")
-    (longarrowright "\\<longrightarrow>")
-    (longarrowleft "\\<longleftarrow>")
-    (longarrowboth "\\<longleftrightarrow>")
-    (longarrowdblright "\\<Longrightarrow>")
-    (longarrowdblleft "\\<Longleftarrow>")
-    (longarrowdblboth "\\<Longleftrightarrow>")
-    (brokenbar "\\<bar>")
-    (hyphen "\\<hyphen>")
-    (macron "\\<inverse>")
-    (exclamdown "\\<exclamdown>")
-    (questiondown "\\<questiondown>")
-    (guillemotleft "\\<guillemotleft>")
-    (guillemotright "\\<guillemotright>")
-    (degree "\\<degree>")
-    (onesuperior "\\<onesuperior>")
-    (onequarter "\\<onequarter>")
-    (twosuperior "\\<twosuperior>")
-    (onehalf "\\<onehalf>")
-    (threesuperior "\\<threesuperior>")
-    (threequarters "\\<threequarters>")
-    (paragraph "\\<paragraph>")
-    (registered "\\<registered>")
-    (ordfeminine "\\<ordfeminine>")
-    (masculine "\\<ordmasculine>")
-    (section "\\<section>")
-    (sterling "\\<pounds>")
-    (yen "\\<yen>")
-    (cent "\\<cent>")
-    (currency "\\<currency>")
-    (braceleft2 "\\<lbrace>")
-    (braceright2 "\\<rbrace>")
-    (top "\\<top>")
-    (congruent "\\<cong>")
-    (club "\\<clubsuit>")
-    (diamond "\\<diamondsuit>")
-    (heart "\\<heartsuit>")
-    (spade "\\<spadesuit>")
-    (arrowboth "\\<leftrightarrow>")
-    (greaterequal "\\<ge>")
-    (proportional "\\<propto>")
-    (partialdiff "\\<partial>")
-    (ellipsis "\\<dots>")
-    (aleph "\\<aleph>")
-    (Ifraktur "\\<Im>")
-    (Rfraktur "\\<Re>")
-    (weierstrass "\\<wp>")
-    (emptyset "\\<emptyset>")
-    (angle "\\<angle>")
-    (gradient "\\<nabla>")
-    (product "\\<Prod>")
-    (arrowdblboth "\\<Leftrightarrow>")
-    (arrowdblup "\\<Up>")
-    (arrowdbldown "\\<Down>")
-    (angleleft "\\<langle>")
-    (angleright "\\<rangle>")
-    (summation "\\<Sum>")
-    (integral "\\<integral>")
-    (circleintegral "\\<ointegral>")
-    (dagger "\\<dagger>")
-    (sharp "\\<sharp>")
-    (star "\\<star>")
-    (smltriangleright "\\<triangleright>")
-    (triangleleft "\\<lhd>")
-    (triangle "\\<triangle>")
-    (triangleright "\\<rhd>")
-    (trianglelefteq "\\<unlhd>")
-    (trianglerighteq "\\<unrhd>")
-    (smltriangleleft "\\<triangleleft>")
-    (natural "\\<natural>")
-    (flat "\\<flat>")
-    (amalg "\\<amalg>")
-    (Mho "\\<mho>")
-    (arrowupdown "\\<updown>")
-    (longmapsto "\\<longmapsto>")
-    (arrowdblupdown "\\<Updown>")
-    (hookleftarrow "\\<hookleftarrow>")
-    (hookrightarrow "\\<hookrightarrow>")
-    (rightleftharpoons "\\<rightleftharpoons>")
-    (leftharpoondown "\\<leftharpoondown>")
-    (rightharpoondown "\\<rightharpoondown>")
-    (leftharpoonup "\\<leftharpoonup>")
-    (rightharpoonup "\\<rightharpoonup>")
-    (asym "\\<asymp>")
-    (minusplus "\\<minusplus>")
-    (bowtie "\\<bowtie>")
-    (centraldots "\\<cdots>")
-    (circledot "\\<odot>")
-    (propersuperset "\\<supset>")
-    (reflexsuperset "\\<supseteq>")
-    (propersqsuperset "\\<sqsupset>")
-    (reflexsqsuperset "\\<sqsupseteq>")
-    (lessless "\\<lless>")
-    (greatergreater "\\<ggreater>")
-    (unionplus "\\<uplus>")
-    (backslash3 "\\<setminus>")
-    (smile "\\<smile>")
-    (reflexsucc "\\<succeq>")
-    (dashbar "\\<stileturn>")
-    (biglogicalor "\\<Or>")
-    (bigunionplus "\\<Uplus>")
-    (daggerdbl "\\<ddagger>")
-    (bigbowtie "\\<Join>")
-    (booleans "\\<bool>")
-    (complexnums "\\<complex>")
-    (natnums "\\<nat>")
-    (rationalnums "\\<rat>")
-    (realnums "\\<real>")
-    (integers "\\<int>")
-    (lesssim "\\<lesssim>")
-    (greatersim "\\<greatersim>")
-    (lessapprox "\\<lessapprox>")
-    (greaterapprox "\\<greaterapprox>")
-    (definedas "\\<triangleq>")
-    (cataleft "\\<lparr>")
-    (cataright "\\<rparr>")
-    (bigcircledot "\\<Odot>")
-    (bigcirclemultiply "\\<Otimes>")
-    (bigcircleplus "\\<Oplus>")
-    (coproduct "\\<Coprod>")
-    (cedilla "\\<cedilla>")
-    (diaeresis "\\<dieresis>")
-    (acute "\\<acute>")
-    (hungarumlaut "\\<hungarumlaut>")
-    (lozenge "\\<lozenge>")
-    (smllozenge "\\<struct>")
-    (dotlessi "\\<index>")
-    (euro "\\<euro>")
-    (zero1 "\\<zero>")
-    (one1 "\\<one>")
-    (two1 "\\<two>")
-    (three1 "\\<three>")
-    (four1 "\\<four>")
-    (five1 "\\<five>")
-    (six1 "\\<six>")
-    (seven1 "\\<seven>")
-    (eight1 "\\<eight>")
-    (nine1 "\\<nine>")
-    ))
-
-(defun x-symbol-isabelle-prepare-table (table)
-  "Account for differences in symbols between Isabelle/Isar and Isabelle."
-  (let*
-      ((is-isar (eq proof-assistant-symbol 'isar))
-       (prfx1 (if is-isar "" "\\"))
-       (prfx2 (if is-isar "\\" "")))
-    (mapcar (lambda (entry)
-              (list (car entry) nil
-		    (concat prfx1 (cadr entry)) 
-		    (concat prfx2 (cadr entry))))
-            table)))
-
-(defvar x-symbol-isabelle-table
-  (x-symbol-isabelle-prepare-table
-   (append
-    x-symbol-isabelle-user-table
-    x-symbol-isabelle-symbol-table
-    x-symbol-isabelle-xsymbol-table)))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; User-level settings for X-Symbol 
-;;
-;; this is MODE-ON CODING 8BITS UNIQUE SUBSCRIPTS IMAGE
-(defcustom x-symbol-isabelle-auto-style
-  '((proof-ass x-symbol-enable)	 ; MODE-ON: whether to turn on interactively
-    nil   ;; x-symbol-coding
-    'null ;; x-symbol-8bits	   [NEVER want it; null disables search]
-    nil   ;; x-symbol-unique
-    t     ;; x-symbol-subscripts
-    nil)  ;; x-symbol-image
-  "Variable used to document a language access.
-See documentation of `x-symbol-auto-style'."
-  :group 'x-symbol-isabelle
-  :group 'x-symbol-mode
-  :type 'x-symbol-auto-style)
-
-;; FIXME da: is this needed?
-(defcustom x-symbol-isabelle-auto-coding-alist nil
-  "*Alist used to determine the file coding of ISABELLE buffers.
-Used in the default value of `x-symbol-auto-mode-alist'.  See
-variable `x-symbol-auto-coding-alist' for details."
-  :group 'x-symbol-isabelle
-  :group 'x-symbol-mode
-  :type 'x-symbol-auto-coding)
-
-
-     
-
-(provide 'x-symbol-isabelle)