diff options
-rw-r--r-- | isa/BUGS | 68 | ||||
-rw-r--r-- | isa/Example-Xsym.ML | 20 | ||||
-rw-r--r-- | isa/Example.ML | 18 | ||||
-rw-r--r-- | isa/Example.thy | 20 | ||||
-rw-r--r-- | isa/Example2.ML | 15 | ||||
-rw-r--r-- | isa/README | 32 | ||||
-rw-r--r-- | isa/interface-setup.el | 43 | ||||
-rw-r--r-- | isa/isa-syntax.el | 352 | ||||
-rw-r--r-- | isa/isa.el | 723 | ||||
-rw-r--r-- | isa/isabelle-system.el | 598 | ||||
-rw-r--r-- | isa/thy-mode.el | 1045 | ||||
-rw-r--r-- | isa/todo | 62 | ||||
-rw-r--r-- | isa/x-symbol-isa.el | 21 | ||||
-rw-r--r-- | isa/x-symbol-isabelle.el | 514 |
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) |