initial version of 'isar proof assistant (Isabelle/Isar);

6 files changed, 1089 insertions, 0 deletions

diff --git a/isar/Example.thy b/isar/Example.thy
new file mode 100644
index 00000000..b8b7328b
--- /dev/null
+++ b/isar/Example.thy
@@ -0,0 +1,12 @@
+
+theory Example = Main:;
+
+lemma "A --> B --> A";
+proof;
+  assume A;
+  show "B --> A";
+  proof;
+  qed;
+qed;
+
+end;
diff --git a/isar/ProofGeneral.ML b/isar/ProofGeneral.ML
new file mode 100644
index 00000000..8cf11f2f
--- /dev/null
+++ b/isar/ProofGeneral.ML
@@ -0,0 +1,41 @@
+(* 
+   Isabelle/Isar configuration for Proof General.
+
+   Author:  David Aspinall <da@dcs.ed.ac.uk>
+   Contact: Isabelle maintainer <isabelle@dcs.ed.ac.uk>
+
+   ProofGeneral.ML,v 2.16 1998/11/03 16:29:30 da Exp
+
+MMW: I have temporarily removed the theory loader patches, since it
+kept crashing on me.
+*)
+
+
+(** configure output channels to decorate output **)
+
+(*messages*)
+writeln_fn :=
+  (std_output o suffix "\n" o enclose (oct_char "360") (oct_char "361"));
+warning_fn :=
+  (std_output o suffix "\n" o enclose (oct_char "362") (oct_char "363") o prefix_lines "### ");
+error_fn :=
+  (std_output o suffix "\n" o enclose (oct_char "364") (oct_char "365") o prefix_lines "*** ");
+
+(*prompts*)
+Source.decorate_prompt_fn := (fn s => s ^ oct_char "372");
+
+(*theory / proof state*)
+current_goals_markers :=
+  let
+    val begin_state = oct_char "366";
+    val end_state= oct_char "367";
+    val begin_goal = oct_char "370";
+  in (begin_state, end_state, begin_goal) end;
+
+Toplevel.print_state_fn :=
+  (Library.setmp writeln_fn (std_output o suffix "\n") Toplevel.print_state_default);
+
+
+print_mode := ["ProofGeneral"];
+
+Isar.main();
diff --git a/isar/interface b/isar/interface
new file mode 100644
index 00000000..e294799d
--- /dev/null
+++ b/isar/interface
@@ -0,0 +1,108 @@
+#!/bin/bash
+#
+# $Id$
+#
+# ProofGeneral interface wrapper for Isabelle/Isar.
+
+
+## diagnostics
+
+PRG=$(basename $0)
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [OPTIONS] [FILES ...]"
+  echo
+  echo "  Options are:"
+  echo "    -l NAME      logic image name (default $ISABELLE_LOGIC)"
+  echo "    -p NAME      Emacs program name (default xemacs)"
+  echo "    -u BOOL      use .emacs file (default false)"
+  echo "    -w BOOL      use window system (default true)"
+  echo
+  echo "Starts ProofGeneral for Isabelle/Isar with LOGIC images and theory FILES."
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+PG_HOME=$(cd $(dirname "$0"); cd ..; echo $PWD)
+
+
+# options
+
+LOGIC="$ISABELLE_LOGIC"
+PROGNAME="xemacs"
+INITFILE="false"
+WINDOWSYSTEM="true"
+
+function getoptions()
+{
+  OPTIND=1
+  while getopts "l:p:u:w:" OPT
+  do
+    case "$OPT" in
+      l)
+        LOGIC="$OPTARG"
+        ;;
+      p)
+        PROGNAME="$OPTARG"
+        ;;
+      u)
+        INITFILE="$OPTARG"
+        ;;
+      w)
+        WINDOWSYSTEM="$OPTARG"
+        ;;
+      \?)
+        usage
+        ;;
+    esac
+  done
+}
+
+getoptions $PROOFGENERAL_OPTIONS
+
+getoptions "$@"
+shift $(($OPTIND - 1))
+
+
+# args
+
+FILES="$@"
+shift $#
+
+[ -z "$FILES" ] && FILES="Scratch.thy"
+
+
+## main
+
+ARGS=""
+
+[ "$INITFILE" = false ] && ARGS="$ARGS -q"
+
+if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then
+  ARGS="$ARGS -T Isabelle"
+else
+  ARGS="$ARGS -nw"
+fi
+
+
+ARGS="$ARGS -l $PG_HOME/isar/interface-setup.el -l $PG_HOME/generic/proof-site.el"
+
+for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
+    "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
+do
+  [ -f "$FILE" ] && ARGS="$ARGS -l $FILE"
+done
+
+export PROOFGENERAL_HOME="$PG_HOME/"
+export PROOFGENERAL_LOGIC="$LOGIC"
+exec $PROGNAME $ARGS $FILES
diff --git a/isar/interface-setup.el b/isar/interface-setup.el
new file mode 100644
index 00000000..06a383d1
--- /dev/null
+++ b/isar/interface-setup.el
@@ -0,0 +1,9 @@
+;;
+;; $Id$
+;; 
+
+(customize-set-variable
+ 'isabelle-isar-prog-name
+ (concat (getenv "ISABELLE") " " (getenv "PROOFGENERAL_LOGIC")))
+
+(customize-set-variable 'proof-assistant-table '((isar "Isabelle/Isar" "\\.thy$")))
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
new file mode 100644
index 00000000..0b2dec35
--- /dev/null
+++ b/isar/isar-syntax.el
@@ -0,0 +1,266 @@
+;; isar-syntax.el Syntax expressions for Isabelle/Isar
+;; Copyright (C) 1994-1998 LFCS Edinburgh. 
+;;
+;; Author:      David Aspinall <da@dcs.ed.ac.uk>
+;; Maintainer:  Isabelle maintainer <isabelle@dcs.ed.ac.uk>
+;;
+;; isar-syntax.el,v 2.14 1998/11/03 14:41:54 da Exp
+;;
+
+(require 'proof-syntax)
+
+;;; Proof mode customization: how should it work?
+;;;   Presently we have a bunch of variables in proof.el which are
+;;;   set from a bunch of similarly named variables in <engine>-syntax.el.
+;;;
+;;;   Seems a bit daft: why not just have the customization in
+;;;   one place, and settings hardwired in <engine>-syntax.el.
+;;;
+;;;   That way we can see which settings are part of instantiation of
+;;;   proof.el, and which are part of cusomization for <engine>.
+
+;; ------ customize groups
+
+;(defgroup isar-scripting nil
+;  "Customization of Isabelle/Isar script management"
+;  :group 'external
+;  :group 'languages)
+
+;(defgroup isar-syntax nil
+;  "Customization of Isabelle/Isar's syntax recognition"
+;  :group 'isar-scripting)
+
+;; ----- syntax for font-lock and other features
+
+(defgroup isar-syntax nil
+  "Customization of Isabelle/Isar syntax for proof mode"
+  :group 'isar-settings)
+
+;MMW FIXME This stuff should be generated automatically (and made logic specific).
+;MMW FIXME Tune these categories.
+;MMW FIXME Can I invent new categories?
+
+(defcustom isar-keywords-decl
+  '(
+    "use_thy"
+    "use" 
+    "undos"
+    "undo"
+    "types"
+    "typedecl"
+    "typed_print_translation"
+    "typ"
+    "translations"
+    "top"
+    "token_translation"
+    "title"
+    "thm"
+    "text"
+    "term"
+    "syntax"
+    "subsubsection"
+    "subsection"
+    "setup"
+    "section"
+    "rep_datatype"
+    "redos"
+    "redo"
+    "record"
+    "recdef"
+    "quit"
+    "pwd"
+    "prop"
+    "print_translation"
+    "print_theory"
+    "print_theorems"
+    "print_syntax"
+    "print_methods"
+    "print_facts"
+    "print_binds"
+    "print_attributes"
+    "print_ast_translation"
+    "primrec"
+    "pr"
+    "path"
+    "parse_translation"
+    "parse_ast_translation"
+    "oracle"
+    "nonterminals"
+    "local"
+    "load"
+    "kill"
+    "inductive"
+    "help"
+    "global"
+    "exit"
+    "defaultsort"
+    "datatype"
+    "consts"
+    "commit"
+    "constdefs"
+    "coinductive"
+    "classrel"
+    "classes"
+    "chapter"
+    "cd"
+    "axioms"
+    "axclass"
+    "arities"
+    "ML"
+    )
+  "Isabelle/Isar keywords for declarations."
+  :group 'isar-syntax
+  :type '(repeat string))
+
+(defcustom isar-keywords-defn
+  '(
+    "theory"
+    "theorems"
+    "lemmas"
+    "defs"
+    "context"
+    "axclass"
+    )
+  "Isabelle/Isar keywords for definitions"
+  :group 'isar-syntax
+  :type '(repeat string))
+
+;; isar-keywords-goal is used to manage undo actions
+(defcustom isar-keywords-goal
+  '(
+    "typedef"
+    "theorem"
+    "lemma"
+    "instance"
+    )
+  "Isabelle/Isar commands to begin an interactive proof"
+  :group 'isar-syntax
+  :type '(repeat string))
+
+(defcustom isar-keywords-save
+  '(
+    "qed_with"
+    )
+  "Isabelle/Isar commands finish a top-level proof and store the theorem"
+  :group 'isar-syntax
+  :type '(repeat string))
+
+(defcustom isar-keywords-kill-goal
+  '("kill")
+  "Isabelle/Isar kill command keywords"
+  :group 'isar-syntax
+  :type '(repeat string))
+
+(defcustom isar-keywords-minor
+  '(
+    "and"
+    "as"
+    "binder"
+    "infixl"
+    "infixr"
+    "is"
+    "output"
+    )
+  "Isabelle/Isar minor keywords"
+  :group 'isar-syntax
+  :type '(repeat string))
+
+(defcustom isar-keywords-proof-commands
+  '(
+    "qed"
+    "proof" 
+    "end"
+    "by"
+    ".."
+    "."
+    )
+  "Isabelle/Isar proof command keywords"
+  :group 'isar-syntax
+  :type '(repeat string))
+
+(defcustom isar-keywords-commands
+  '(
+    "up"
+    "then_refine"
+    "then"
+    "show"
+    "refine"
+    "prev"
+    "note"
+    "next"
+    "let"
+    "have"
+    "from"
+    "fix"
+    "begin"
+    "back"
+    "assume"
+    )
+  "Isabelle/Isar command keywords"
+  :group 'isar-syntax
+  :type '(repeat string))
+
+
+;; NB: this means that any adjustments above by customize will
+;; only have effect in next session.
+(defconst isar-keywords
+  (append isar-keywords-goal isar-keywords-save isar-keywords-decl
+	  isar-keywords-defn isar-keywords-commands)
+  "All keywords in a Isabelle/Isar theory")
+
+
+;; ----- regular expressions
+
+(defconst isar-id "\\([A-Za-z][A-Za-z0-9'_]*\\)")
+(defconst isar-idx (concat isar-id "\\(\\.[0-9]+\\)?"))
+
+(defconst isar-ids (proof-ids isar-id "[ \t]*")
+  "Matches a sequence of identifiers separated by whitespace.")
+
+(defconst isar-string "\"\\(\\([^\\\"]\\|\\\\\"\\)*\\)\"")
+
+(defconst isar-string-regexp
+  (concat "\\s-*" isar-string "\\s-*")
+  "Regexp matching Isabelle/Isar strings, with contents bracketed.")
+
+(defvar isar-font-lock-terms
+  (list
+   (cons (concat "\351" isar-id "\350") 'proof-declaration-name-face)    ; class
+   (cons (concat "\352'" isar-id "\350") 'proof-tacticals-name-face)     ; tfree
+   (cons (concat "\353\\?'" isar-idx "\350") 'font-lock-type-face)       ; tvar
+   (cons (concat "\354" isar-id "\350") 'font-lock-function-face)        ; free
+   (cons (concat "\355" isar-id "\350") 'font-lock-keyword-face)         ; bound
+   (cons (concat "\356" isar-idx "\350") 'font-lock-function-face)       ; var
+   )
+  "*Font-lock table for Isabelle terms.")
+
+(defconst isar-save-command-regexp
+  (concat "^" (proof-ids-to-regexp isar-keywords-save)))
+
+(defconst isar-save-with-hole-regexp
+  (concat "\\(" (proof-ids-to-regexp isar-keywords-save) isar-string-regexp "\\)"))
+
+(defcustom isar-goal-command-regexp
+  (proof-ids-to-regexp isar-keywords-goal)
+  "Regular expression used to match a goal."
+  :type 'regexp
+  :group 'isabelle-isar-config)
+
+;; MMW FIXME ??
+(defconst isar-goal-with-hole-regexp
+  (concat "\\("
+	  (proof-ids-to-regexp '("lemma" "theorem"))
+	  "\\)" isar-string-regexp)
+  "Regexp matching goal commands in Isabelle/Isar which name a theorem")
+
+(defvar isar-font-lock-keywords-1
+  (append
+   isar-font-lock-terms
+   (list
+    (cons (proof-ids-to-regexp isar-keywords-proof-commands) 'font-lock-function-name-face)
+    (cons (proof-ids-to-regexp isar-keywords) 'font-lock-keyword-face)
+    (cons (proof-ids-to-regexp isar-keywords-minor) 'font-lock-type-face)
+    (list isar-goal-with-hole-regexp 2 'font-lock-function-name-face)
+    (list isar-save-with-hole-regexp 2 'font-lock-function-name-face))))
+
+(provide 'isar-syntax)
diff --git a/isar/isar.el b/isar/isar.el
new file mode 100644
index 00000000..85d4dde5
--- /dev/null
+++ b/isar/isar.el
@@ -0,0 +1,653 @@
+;; isar.el Major mode for Isabelle proof assistant
+;; Copyright (C) 1994-1998 LFCS Edinburgh. 
+;;
+;; Author:      David Aspinall <da@dcs.ed.ac.uk>
+;; Maintainer:  Isabelle maintainer <isabelle@dcs.ed.ac.uk>
+
+;;
+;; isar.el,v 2.44 1998/11/10 18:08:50 da Exp
+;;
+
+
+;; FIXME: this most be done before loading proof-config, shame.
+(setq proof-tags-support nil) ; no isatags prog, yet.
+
+;; Add Isabelle image onto splash screen
+(customize-set-variable
+ 'proof-splash-extensions
+ '(list
+   nil
+   (proof-splash-display-image "isabelle_transparent" t)))
+
+(require 'proof)
+(require 'isar-syntax)
+
+;; To make byte compiler be quiet.
+;; NASTY: these result in loads when evaluated 
+;; ordinarily (from non-byte compiled code).
+;(eval-when-compile
+;  (require 'proof-script)
+;  (require 'proof-shell)
+;  (require 'outline)
+;  (cond ((fboundp 'make-extent) (require 'span-extent))
+;	((fboundp 'make-overlay) (require 'span-overlay))))
+
+
+
+;;; variable: proof-analyse-using-stack
+;;;    proof-locked-region-empty-p, proof-shell-insert, pbp-mode,
+;;;    proof-mark-buffer-atomic, proof-shell-invisible-command,
+;;;    prev-span, span-property, next-span, proof-unprocessed-begin,
+;;;    proof-config-done, proof-shell-config-done
+
+
+;;;
+;;; ======== User settings for Isabelle/Isar ========
+;;;
+
+;;; proof-site provides us with the cusomization groups
+;;;
+;;; 'isabelle-isar         -  User options for Isabelle/Isar Proof General
+;;; 'isabelle-isar-config  -  Configuration of Isabelle/Isar Proof General
+;;;	   		      (constants, but may be nice to tweak)
+
+(defcustom isabelle-isar-prog-name "isabelle"
+  "*Name of program to run Isabelle/Isar."
+  :type 'file
+  :group 'isabelle-isar)
+
+(defcustom isabelle-isar-indent 2
+  "*Indentation degree in documents"
+  :type 'number
+  :group 'isabelle-isar)
+
+(defcustom isabelle-web-page
+  "http://isabelle.in.tum.de"
+  "URL of web page for Isabelle."
+  :type 'string
+  :group 'isabelle-isar)
+
+;;;
+;;; ======== Configuration of generic modes ========
+;;;
+
+;; ===== outline mode
+
+(defcustom isar-keywords-section
+  '("chapter" "section" "subsection" "subsubsection" "text")
+  "Isabelle/Isar section headings"
+  :group 'isar-syntax
+  :type '(repeat string))
+
+(defcustom isar-outline-regexp
+  (proof-ids-to-regexp (append isar-keywords-goal isar-keywords-section))
+  "Outline regexp for Isabelle/Isar documents"
+  :type 'regexp
+  :group 'isabelle-isar-config)
+
+;;; End of a command needs parsing to find, so this is approximate.
+(defcustom isar-outline-heading-end-regexp ";[ \t\n]*"
+  "Outline heading end regexp for Isabelle/Isar ML files."
+  :type 'regexp
+  :group 'isabelle-isar-config)
+
+;; FIXME: not sure about this one
+(defvar isar-shell-outline-regexp "\370[ \t]*\\([0-9]+\\)\\.")
+(defvar isar-shell-outline-heading-end-regexp "$")
+
+(defun isar-outline-setup ()
+  (if (and window-system (string-match "XEmacs" emacs-version))
+      (progn
+	(custom-set-variables     ;custom value dictatorship!
+	 '(outline-mac-style t))
+	(outl-mouse-minor-mode))
+    (outline-minor-mode)))
+
+;;; ---- end-outline
+
+
+
+;;; NB!  Disadvantage of *not* shadowing variables is that user
+;;; cannot override them.  It might be nice to override some
+;;; variables, which ones?
+
+(defun isar-mode-config-set-variables ()
+  "Configure generic proof scripting mode variables for Isabelle/Isar."
+  (setq
+   proof-assistant-home-page	isabelle-web-page
+   proof-mode-for-script	'isar-proofscript-mode
+   ;; proof script syntax
+   proof-terminal-char		?\;	; ends a proof
+   proof-comment-start		"(*"	; comment in a proof
+   proof-comment-end		"*)"	; 
+   ;; Next few used for func-menu and recognizing goal..save regions in
+   ;; script buffer.
+   proof-save-command-regexp    isar-save-command-regexp
+   proof-goal-command-regexp    isar-goal-command-regexp
+   proof-goal-with-hole-regexp  isar-goal-with-hole-regexp
+   proof-save-with-hole-regexp  isar-save-with-hole-regexp
+   proof-commands-regexp	(proof-ids-to-regexp isar-keywords)
+   ;; proof engine commands (first three for menus, last for undo)
+   proof-prf-string		"pr"
+   proof-goal-command		"lemma \"%s\""
+   proof-save-command		"qed"
+   proof-ctxt-string		"print_theory"
+   proof-help-string		"help"
+   proof-kill-goal-command	"kill"
+   ;; command hooks
+   proof-goal-command-p		'isar-goal-command-p
+   proof-count-undos-fn		'isar-count-undos
+   proof-find-and-forget-fn	'isar-find-and-forget
+   proof-goal-hyp-fn		'isar-goal-hyp
+   proof-state-preserving-p	'isar-state-preserving-p
+   proof-parse-indent		'isar-parse-indent
+   proof-stack-to-indent	'isar-stack-to-indent
+   proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list))
+
+
+(defun isar-shell-mode-config-set-variables ()
+  "Configure generic proof shell mode variables for Isabelle/Isar."
+  (setq
+   proof-shell-first-special-char	?\350
+
+   proof-shell-wakeup-char		?\372
+   proof-shell-annotated-prompt-regexp  "^\\w*[>#] \372"
+
+   ;; This pattern is just for comint.
+   proof-shell-prompt-pattern		"^\\w*[>#] "
+
+   ;; for issuing command, not used to track cwd in any way.
+   proof-shell-cd			"cd \"%s\";"
+   proof-shell-proof-completed-regexp   "FIXME No subgoals!"
+
+   proof-shell-error-regexp		"^\364\\*\\*\\*"
+   proof-shell-interrupt-regexp         "^Interrupt"
+   
+   ;; nothing appropriate for: proof-shell-abort-goal-regexp         ;; MMW FIXME: ??
+
+   ;; matches names of assumptions
+   proof-shell-assumption-regexp	isar-id
+   ;; matches subgoal name
+   ;; FIXME: proof-shell-goal-regexp is *not* used at the generic level!
+   ;;        Perhaps it should be renamed to isar-goal-regexp and be
+   ;;        set somewhere else.  
+   proof-shell-goal-regexp		"\370[ \t]*\\([0-9]+\\)\\."
+
+   proof-shell-start-goals-regexp	"\366"
+   proof-shell-end-goals-regexp		"\367"
+   proof-shell-goal-char	        ?\370
+   ;; initial command configures Isabelle/Isar by hacking print functions.
+   proof-shell-init-cmd
+    (concat "use \"" proof-home-directory "isar/ProofGeneral.ML\";")
+   proof-shell-restart-cmd		"restart"
+   proof-shell-quit-cmd			"quit"
+   
+   proof-shell-eager-annotation-start   "\360\\|\362"
+   proof-shell-eager-annotation-end     "\361\\|\363"
+
+   ;; 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."
+
+   ;; Tested values of proof-shell-eager-annotation-start: 
+   ;; "^\\[opening \\|^###\\|^Reading\\|^Proof General\\|^Not reading"
+   ;; "^---\\|^\\[opening "
+   ;; could be last bracket on end of line, or with ### and ***.
+
+   ;; === ANNOTATIONS  === ones below here are broken
+   proof-shell-result-start	        "\372 Pbp result \373"
+   proof-shell-result-end		"\372 End Pbp result \373"
+   proof-analyse-using-stack		t
+   proof-shell-start-char		?\372
+   proof-shell-end-char			?\373
+   proof-shell-field-char		?\374
+   ;; NEW NEW for multiple files
+   ;; === NEW NEW: multiple file stuff.  move elsewhere later.
+   proof-shell-process-file 
+   (cons
+    ;; Theory loader output and verbose update() output.
+    "Proof General, this file is loaded: \"\\(.*\\)\""
+    (lambda (str)
+      (match-string 1 str)))
+   ;; \\|Not reading \"\\(.*\\)\"
+   ;;    (lambda (str)
+   ;;   (or (match-string 1 str) 
+   ;;	  (match-string 2 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 'isar-shell-compute-new-files-list
+   )
+  (add-hook 'proof-activate-scripting-hook 'isar-shell-hack-use-thy)
+  )
+
+
+;;;
+;;;  use_thy and friends.
+;;;
+;;; Quite tricky to get these right.  By default, Isabelle's
+;;; theory loader glues together theory and ML files whenever
+;;; it can, but that's not what we want here.
+;;;
+;;; So we rely on some hacked versions.
+;;;
+
+(defcustom isar-usethy-notopml-command "" ;;; FIXME "ProofGeneral.use_thy \"%s\";"
+  "Sent to Isabelle/Isar to process theory for this ML file, and all ancestors."
+  :type 'string
+  :group 'isabelle-isar-config)
+
+(defun isar-shell-hack-use-thy ()
+  "Possibly issue  use_thy_no_topml command to Isabelle/Isar.
+If the current buffer has an empty locked region, the interface is
+about to send commands from it to Isabelle/Isar.  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 (and
+       (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?
+       buffer-file-name
+       (file-exists-p 
+	(concat (file-name-sans-extension buffer-file-name) ".thy")))
+      ;; Send a use_thy command if there is a corresponding .thy file.
+      ;; Let Isabelle do the work of checking whether any work needs
+      ;; doing.  Really this should be force_use_thy, too.
+      ;; Wait after sending, so that queue is cleared for further commands.
+      ;; (there would be no harm in letting the queue be extended
+      ;; if it were allowed for).
+      (progn
+	(proof-shell-invisible-command
+	 (format isar-usethy-notopml-command
+		 (file-name-sans-extension buffer-file-name))
+	 t)
+	;; Leave the messages from the use around.
+	(setq proof-shell-erase-response-flag nil))
+    ))
+
+(defun isar-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."
+  ;; This assertion is supposed to test that we only remove
+  ;; what was in the list anyway.  But 
+  ;;(assert (member (file-truename (match-string 1 str))
+  ;;		  proof-included-files-list))
+  (remove (file-truename (match-string 1 str)) 
+	  proof-included-files-list))
+
+;;
+;; Hack for update
+;;
+
+(defcustom isar-update-command "" ;; FIXME "ProofGeneral.update();"
+  "Sent to Isabelle/Isar to re-load theory files as needed and synchronise."
+  :type 'string
+  :group 'isabelle-config)
+  
+(defun isar-update ()
+  "Issue an update command to the Isabelle/Isar process.
+This re-reads any theory files as necessary and resynchronizes
+proof-included-files-list."
+  (interactive)
+  (save-some-buffers)
+  (proof-shell-insert isar-update-command))
+
+  
+
+
+
+;;
+;;   Define the derived modes 
+;;
+(eval-and-compile
+(define-derived-mode isar-shell-mode proof-shell-mode
+   "Isabelle/Isar shell" nil
+   (isar-shell-mode-config)))
+
+(eval-and-compile			; to define vars for byte comp.
+(define-derived-mode isar-pbp-mode pbp-mode
+  "Isabelle/Isar proofstate" nil
+  (isar-pbp-mode-config)))
+
+(eval-and-compile			; to define vars for byte comp.
+(define-derived-mode isar-proofscript-mode proof-mode
+    "Isabelle/Isar script" nil
+    (isar-mode-config)))
+
+(define-key isar-proofscript-mode-map
+  [(control c) (control l)] 'proof-prf)	; keybinding like Isamode
+
+
+(defun isar-mode ()
+  "Mode for Isabelle/Isar interactive documents."
+  (interactive)
+  (cond
+   (;; Hack for splash screen
+    (if (and (boundp 'proof-mode-hook)
+	     (memq 'proof-splash-timeout-waiter proof-mode-hook))
+	(proof-splash-timeout-waiter))
+    ;; Has this theory file already been loaded by Isabelle?
+    ;; Colour it blue if so.  
+    ;; NB: call to file-truename is needed for FSF Emacs which
+    ;; chooses to make buffer-file-truename abbreviate-file-name
+    ;; form of file-truename.
+    (and (member (file-truename buffer-file-truename)
+		 proof-included-files-list)
+	 (proof-mark-buffer-atomic (current-buffer)))
+    )
+   (t 
+    ;; Proof mode does that automatically.
+    (isar-proofscript-mode))))
+
+;; FIXME: could test that the buffer isn't already locked.
+(defun isar-process-thy-file (file)
+  "Process the theory file FILE.  If interactive, use buffer-file-name."
+  (interactive (list buffer-file-name))
+  (save-some-buffers)
+  (proof-shell-invisible-command 
+   (format isar-usethy-notopml-command
+	   (file-name-sans-extension file))))
+
+(defcustom isar-retract-thy-file-command "" ;; MMW FIXME "ML {| ProofGeneral.retract_thy_file \"%s\"; |};"
+  "Sent to Isabelle/Isar to forget theory file and descendants.
+Resulting output from Isabelle/Isar will be parsed by Proof General."
+  :type 'string
+  :group 'isabelle-isar-config)
+
+(defcustom isar-retract-ML-file-command "" ;; MMW FIXME "ML {| ProofGeneral.retract_ML_file \"%s\"\"; |};"
+  "Sent to Isabelle/Isar to forget ML file and descendants.
+Resulting output from Isabelle/Isar will be parsed by Proof General."
+  :type 'string
+  :group 'isabelle-isar-config)
+
+(defcustom isar-retract-ML-files-children-command "" ;; MMW FIXME "ProofGeneral.retract_ML_files_children \"%s\";"
+  "Sent to Isabelle/Isar to forget the descendants of an ML file.
+Resulting output from Isabelle will be parsed by Proof General."
+  :type 'string
+  :group 'isabelle-config)
+
+(defun isar-retract-thy-file (file)
+  "Retract the theory file FILE. If interactive, use buffer-file-name."
+  (interactive (list buffer-file-name))
+  (proof-shell-invisible-command
+   (format isar-retract-thy-file-command
+	   (file-name-sans-extension file))))
+
+
+;; Next bits taken from isar-load.el
+;; isar-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-isar)
+
+(autoload 'thy-mode "thy-mode" 
+	  "Major mode for Isabelle/Isar theory files" t nil)
+
+(autoload 'thy-find-other-file "thy-mode" 
+	    "Find associated .ML or .thy file." t nil)
+
+(defun isar-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 isar-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 isar-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 isar-proofscript-mode-map 
+  [(control c) (control o)] 'thy-find-other-file)
+
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Code that's Isabelle specific                                  ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+;; FIXME: think about the next variable.  I've changed sense from
+;;  LEGO and Coq's treatment.
+(defcustom isar-not-undoable-commands-regexp
+  (proof-ids-to-regexp '("break" "context" "clear_undo" "undo"))
+  "Regular expression matching commands which are *not* undoable."
+  :type 'regexp
+  :group 'isabelle-isar-config)
+
+;; This next function is the important one for undo operations.
+(defun isar-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))
+	     (isar-goal-command-p
+	      (span-property (prev-span span 'type) 'cmd)))
+	(concat "top clear_undo" proof-terminal-string)
+      (while span
+	(setq str (span-property span 'cmd))
+	(cond ((eq (span-property span 'type) 'vanilla)
+	       (or (proof-string-match isar-not-undoable-commands-regexp str)
+		   (setq ct (+ 1 ct))))
+	      ((eq (span-property span 'type) 'pbp)
+	       ;; this case probably redundant for Isabelle, unless
+	       ;; we think of some nice ways of matching non-undoable
+	       ;; commands.
+	       (cond ((not (proof-string-match isar-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 "undos " (int-to-string ct) proof-terminal-string))))
+
+(defun isar-goal-command-p (str)
+  "Decide whether argument is a goal or not"
+  (proof-string-match isar-goal-command-regexp str)) ; this regexp defined in isar-syntax.el
+
+;; Isabelle has no concept of a Linear context, so forgetting back
+;; to the declaration of a particular something makes no real
+;; sense.  Perhaps in the future there will be functions to remove
+;; theorems from theories, but even then all we could do is
+;; forget particular theorems one by one.  So we ought to search
+;; backwards in isar-find-and-forget, rather than forwards as
+;; the old code below does.
+
+(defun isar-find-and-forget (span)
+  "Return a command to be used to forget SPAN."
+  (save-excursion
+    ;; FIXME: bug here: too much gets retracted.
+    ;; See if we are going to part way through a completely processed
+    ;; buffer, in which case it should be removed from 
+    ;; proof-included-files-list along with any other buffers
+    ;; depending on it.  However, even though we send the retraction
+    ;; command to Isabelle we don't want to *completely* unlock
+    ;; the current buffer.  How can this be avoided?
+    (goto-char (point-max))
+    (skip-chars-backward " \t\n") 
+    (if (>= (proof-unprocessed-begin) (point))
+	(format isar-retract-ML-files-children-command 
+		(file-name-sans-extension 
+		 (file-name-nondirectory
+		  (buffer-file-name))))
+      proof-no-command)))
+
+
+;; BEGIN Old code  (taken from Coq.el)
+;(defconst isar-keywords-decl-defn-regexp
+;  (ids-to-regexp (append isar-keywords-decl isar-keywords-defn))
+;  "Declaration and definition regexp.")
+;(defun isar-find-and-forget (span)
+;  (let (str ans)
+;    (while (and span (not ans))
+;      (setq str (span-property span 'cmd))
+;      (cond
+;       ((eq (span-property span 'type) 'comment))       
+
+;       ((eq (span-property span 'type) 'goalsave)
+;	(setq ans (concat isar-forget-id-command
+;			  (span-property span 'name) proof-terminal-string)))
+
+;       ((string-match (concat "\\`\\(" isar-keywords-decl-defn-regexp
+;                              "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str)
+;	(setq ans (concat isar-forget-id-command
+;			  (match-string 2 str) proof-terminal-string)))
+;       ;; If it's not a goal but it contains "Definition" then it's a
+;       ;; declaration
+;       ((and (not (isar-goal-command-p str))
+;	     (string-match
+;	      (concat "Definition\\s-+\\(" proof-id "\\)\\s-*:") str))
+;	(setq ans (concat isar-forget-id-command
+;			  (match-string 2 str) proof-terminal-string))))
+;      (setq span (next-span span 'type)))
+;      (or ans "COMMENT")))
+; END old code 
+
+(defvar isar-current-goal 1
+  "Last goal that emacs looked at.")
+
+;; Parse proofstate output.  Isabelle does not display
+;; named hypotheses in the proofstate output:  they
+;; appear as a list in each subgoal.  Ignore
+;; that aspect for now and just return the
+;; subgoal number.
+;; MMW FIXME: ??
+(defun isar-goal-hyp ()
+  (if (looking-at proof-shell-goal-regexp)
+      (cons 'goal (match-string 1))))
+
+(defun isar-state-preserving-p (cmd)
+  "Non-nil if command preserves the proofstate."
+  (proof-string-match isar-not-undoable-commands-regexp cmd))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Indentation                                                    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; MMW FIXME: take from coq.el?
+;; Sadly this is pretty pointless for Isabelle.
+;; Proof scripts in Isabelle don't really have an easily-observed
+;; block structure  -- a case split can be done by any obscure tactic,
+;; and then solved in a number of steps that bears no relation to the
+;; number of cases!  And the end is certainly not marked in anyway.
+;; 
+(defun isar-stack-to-indent (stack)
+    (cond
+   ((null stack) 0)
+   ((null (car (car stack)))
+    (nth 1 (car stack)))
+   (t (save-excursion
+	(goto-char (nth 1 (car stack)))
+	(+ isabelle-isar-indent (current-column))))))
+
+(defun isar-parse-indent (c stack)
+  "Indentation function for Isabelle.  Does nothing at the moment."
+  stack)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Isa shell startup and exit hooks                               ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun isar-pre-shell-start ()
+  (setq proof-prog-name		isabelle-isar-prog-name)
+  (setq proof-mode-for-shell    'isar-shell-mode)
+  (setq proof-mode-for-pbp	'isar-pbp-mode))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Configuring proof and pbp mode and setting up various utilities  ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun isar-init-syntax-table ()
+  "Set appropriate values for syntax table in current buffer."
+  (modify-syntax-entry ?\$ ".")
+  (modify-syntax-entry ?\/ ".")
+  (modify-syntax-entry ?\\ ".")
+  (modify-syntax-entry ?+  ".")
+  (modify-syntax-entry ?-  ".")
+  (modify-syntax-entry ?=  ".")
+  (modify-syntax-entry ?%  ".")
+  (modify-syntax-entry ?<  ".")
+  (modify-syntax-entry ?>  ".")
+  (modify-syntax-entry ?\& ".")
+  (modify-syntax-entry ?_  "_")
+  (modify-syntax-entry ?\' "_")
+  (modify-syntax-entry ?\| ".")
+  (modify-syntax-entry ?\* ". 23")
+  (modify-syntax-entry ?\( "()1")
+  (modify-syntax-entry ?\) ")(4"))
+
+(defun isar-mode-config ()
+  (isar-mode-config-set-variables)
+  (isar-init-syntax-table)
+  (setq font-lock-keywords isar-font-lock-keywords-1)
+  (proof-config-done)
+  ;; outline
+  ;; FIXME: do we need to call make-local-variable here?
+  (make-local-variable 'outline-regexp)
+  (setq outline-regexp isar-outline-regexp)
+  (make-local-variable 'outline-heading-end-regexp)
+  (setq outline-heading-end-regexp isar-outline-heading-end-regexp)
+  (isar-outline-setup)
+  ;; tags
+  ;  (and (boundp 'tag-table-alist)
+  ;       (setq tag-table-alist
+  ;	     (append '(("\\.ML$"  . isar-ML-file-tags-table)
+  ;		       ("\\.thy$" . thy-file-tags-table))
+  ;		     tag-table-alist)))
+  (setq blink-matching-paren-dont-ignore-comments t))
+
+
+;; MMW FIXME: ??
+;; This hook is added on load because proof shells can
+;; be started from .thy (not in scripting mode) or .ML files.
+(add-hook 'proof-pre-shell-start-hook 'isar-pre-shell-start nil t)
+
+(defun isar-shell-mode-config ()
+  "Configure Proof General proof shell for Isabelle/Isar."
+  (isar-init-syntax-table)
+  (isar-shell-mode-config-set-variables)
+  (proof-shell-config-done)
+  (isar-outline-setup))
+
+;; FIXME: broken, of course, as is all PBP everywhere.
+(defun isar-pbp-mode-config ()
+  (setq pbp-change-goal "Show %s.")
+  (setq pbp-error-regexp proof-shell-error-regexp)
+  (isar-outline-setup))
+
+(provide 'isar)