diff options
Diffstat (limited to 'isa')
| -rw-r--r-- | isa/BUGS | 50 | ||||
| -rw-r--r-- | isa/Example-Xsym.ML | 15 | ||||
| -rw-r--r-- | isa/Example.ML | 13 | ||||
| -rw-r--r-- | isa/Example.thy | 10 | ||||
| -rw-r--r-- | isa/Example2.ML | 15 | ||||
| -rw-r--r-- | isa/README | 33 | ||||
| -rw-r--r-- | isa/depends.ML | 100 | ||||
| -rw-r--r-- | isa/interface | 236 | ||||
| -rw-r--r-- | isa/interface-setup.el | 48 | ||||
| -rw-r--r-- | isa/isa-syntax.el | 304 | ||||
| -rw-r--r-- | isa/isa.el | 765 | ||||
| -rw-r--r-- | isa/isabelle-system.el | 382 | ||||
| -rw-r--r-- | isa/thy-mode.el | 1047 | ||||
| -rw-r--r-- | isa/todo | 84 | ||||
| -rw-r--r-- | isa/x-symbol-isabelle.el | 410 |
15 files changed, 3512 insertions, 0 deletions
diff --git a/isa/BUGS b/isa/BUGS new file mode 100644 index 00000000..068e7fa9 --- /dev/null +++ b/isa/BUGS @@ -0,0 +1,50 @@ +-*- mode:outline -*- + +* Isabelle Proof General Bugs + +See also ../BUGS for generic bugs. + + +** 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 new file mode 100644 index 00000000..d566a850 --- /dev/null +++ b/isa/Example-Xsym.ML @@ -0,0 +1,15 @@ +(* + Example proof script for Isabelle Proof General. + + $Id$ + + Just a version of Example.ML using XSymbol +*) + +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 new file mode 100644 index 00000000..720e3a47 --- /dev/null +++ b/isa/Example.ML @@ -0,0 +1,13 @@ +(* + Example proof script for Isabelle Proof General. + + $Id$ +*) + +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 new file mode 100644 index 00000000..252a5a4c --- /dev/null +++ b/isa/Example.thy @@ -0,0 +1,10 @@ +(* + Example theory file for Isabelle + + David Aspinall <da@dcs.ed.ac.uk> + + $Id$ + +*) + +Example = Main diff --git a/isa/Example2.ML b/isa/Example2.ML new file mode 100644 index 00000000..ab2fef03 --- /dev/null +++ b/isa/Example2.ML @@ -0,0 +1,15 @@ +(* + 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 new file mode 100644 index 00000000..8207071a --- /dev/null +++ b/isa/README @@ -0,0 +1,33 @@ +Isabelle Proof General + +Written by David Aspinall, later with assistance from +Markus Wenzel and David von Oheimb. + +Status: supported +Maintainer: David Aspinall +Isabelle versions: Isabelle99-1, Isabelle99-2, Isabelle2002 +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 proper 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. + +There is no support for proof by pointing yet, and no tags program. + +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/depends.ML b/isa/depends.ML new file mode 100644 index 00000000..65e2b91f --- /dev/null +++ b/isa/depends.ML @@ -0,0 +1,100 @@ +(* depends.ML + + Experimental code for communicating theorem dependencies from Isabelle + to Proof General. + + This code is taken from thm_deps.ML in Isabelle 99-2. It's incompatible + with other Isabelle versions. + + It is duplicated almost verbatim because what we need is + hardwired to a call on the browser tool. +*) + + +fun depends_enable () = Thm.keep_derivs := ThmDeriv; +fun depends_disable () = Thm.keep_derivs := MinDeriv; + + + +fun is_internal (name, tags) = name = "" orelse Drule.has_internal tags; + +fun is_thm_axm (Theorem x) = not (is_internal x) + | is_thm_axm (Axiom x) = not (is_internal x) + | is_thm_axm _ = false; + +fun get_name (Theorem (s, _)) = s + | get_name (Axiom (s, _)) = s + | get_name _ = ""; + +fun make_deps_graph ((gra, parents), Join (ta, ders)) = + let + val name = get_name ta; + in + if is_thm_axm ta then + if is_none (Symtab.lookup (gra, name)) then + let + val (gra', parents') = foldl make_deps_graph ((gra, []), ders); + val prefx = #1 (Library.split_last (NameSpace.unpack name)); + val session = + (case prefx of + (x :: _) => + (case ThyInfo.lookup_theory x of + Some thy => + let val name = #name (Present.get_info thy) + in if name = "" then [] else [name] end + | None => []) + | _ => ["global"]); + in + (Symtab.update ((name, + {name = Sign.base_name name, ID = name, + dir = space_implode "/" (session @ prefx), + unfold = false, path = "", parents = parents'}), gra'), name ins parents) + end + else (gra, name ins parents) + else + foldl make_deps_graph ((gra, parents), ders) + end; + +fun thm_deps thms = + let + val _ = writeln "Generating graph ..."; + val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), + map (#2 o #der o Thm.rep_thm) thms)))); + val path = File.tmp_path (Path.unpack "theorems.graph"); + val _ = Present.write_graph gra path; + val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &"); + in () end; + +fun new_thm_deps thms = + let + val header = "Proof General, the theorem dependencies are: \""; + val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), + map (#2 o #der o Thm.rep_thm) thms)))); + val deps = sort_strings (foldl (op union) ([],(map #parents gra))) + val msg = header ^ (space_implode " " deps) ^ "\"" + in priority msg end; + +val old_qed = qed; +fun qed name = + let val _ = old_qed name + val proved_thm = thm name + in new_thm_deps [proved_thm] end; + +val old_qed_goal = qed_goal; +fun qed_goal name thy goal tacsf = + let val _ = old_qed_goal name thy goal tacsf + val proved_thm = thm name + in new_thm_deps [proved_thm] end; + +val old_qed_goalw = qed_goalw; +fun qed_goalw name thy rews goal tacsf = + let val _ = old_qed_goalw name thy rews goal tacsf + val proved_thm = thm name + in new_thm_deps [proved_thm] end; + +(* FIXME: this one only in HOL?? *) +val old_qed_spec_mp = qed_spec_mp; +fun qed_spec_mp name = + let val _ = old_qed_spec_mp name + val proved_thm = thm name + in new_thm_deps [proved_thm] end; diff --git a/isa/interface b/isa/interface new file mode 100644 index 00000000..46c78a58 --- /dev/null +++ b/isa/interface @@ -0,0 +1,236 @@ +#!/usr/bin/env bash +# +# $Id$ +# +# Proof General interface wrapper for Isabelle. + + +## self references + +THIS=$(cd "$(dirname "$0")"; pwd) +SUPER=$(cd "$THIS/.."; pwd) +KIND=$(basename "$(dirname "$0")") + +if [ "$KIND" = isar ]; then + ISAR=true +else + ISAR=false +fi + + +## diagnostics + +usage() +{ + echo + echo "Usage: Isabelle [OPTIONS] [FILES ...]" + echo + echo " Options are:" + echo " -I BOOL use Isabelle/Isar instead of classic Isabelle (default $ISAR)" + echo " -P BOOL actually start Proof General (default true), otherwise" + echo " run plain tty session" + echo " -X BOOL configure the X-Symbol package on startup (default true)" + echo " -g GEOMETRY specify Emacs geometry" + echo " -k NAME use specific isar-keywords for named logic" + echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)" + echo " -m MODE add print mode for output" + echo " -p NAME Emacs program name (default xemacs)" + echo " -u BOOL use personal .emacs file (default true)" + echo " -w BOOL use window system (default true)" + echo " -x BOOL enable the X-Symbol package on startup (default false)" + echo + echo "Starts Proof General for Isabelle with theory and proof FILES" + echo "(default Scratch.thy)." + echo + echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS" + echo + exit 1 +} + +fail() +{ + echo "$1" >&2 + exit 2 +} + + +## process command line + +# options + +ISABELLE_OPTIONS="" +START_PG="true" +GEOMETRY="" +KEYWORDS="" +LOGIC="$ISABELLE_LOGIC" +PROGNAME="xemacs" +INITFILE="true" +WINDOWSYSTEM="true" +XSYMBOL="" +XSYMBOLSETUP=true + +getoptions() +{ + OPTIND=1 + while getopts "I:P:X:g:k:l:m:p:u:w:x:" OPT + do + case "$OPT" in + I) + ISAR="$OPTARG" + ;; + P) + START_PG="$OPTARG" + ;; + X) + XSYMBOLSETUP="$OPTARG" + ;; + g) + GEOMETRY="$OPTARG" + ;; + k) + KEYWORDS="$OPTARG" + ;; + l) + LOGIC="$OPTARG" + ;; + m) + if [ -z "$ISABELLE_OPTIONS" ]; then + ISABELLE_OPTIONS="-m $OPTARG" + else + ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG" + fi + ;; + p) + PROGNAME="$OPTARG" + ;; + u) + INITFILE="$OPTARG" + ;; + w) + WINDOWSYSTEM="$OPTARG" + ;; + x) + XSYMBOL="$OPTARG" + ;; + \?) + usage + ;; + esac + done +} + +getoptions $PROOFGENERAL_OPTIONS + +getoptions "$@" +shift $(($OPTIND - 1)) + +if [ "$ISAR" = true ]; then + KIND=isar + DEFAULT_FILES="Scratch.thy" +else + KIND=isa + DEFAULT_FILES="Scratch.thy Scratch.ML" +fi + + +# args + +if [ "$#" -eq 0 ]; then + FILES="$DEFAULT_FILES" +else + FILES="" + while [ "$#" -gt 0 ]; do + FILES="$FILES '$1'" + shift + done +fi + + +## smart X11 font installation + +function checkfonts () +{ + XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1 + + case "$XLSFONTS" in + xlsfonts:*) + return 1 + ;; + esac + + return 0 +} + +function installfonts () +{ + checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS +} + + +## main + +if [ "$START_PG" = false ]; then + + [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I" + exec "$ISABELLE" $ISABELLE_OPTIONS "$LOGIC" + +else + + ARGS="" + + [ -n "$GEOMETRY" ] && ARGS="$ARGS -geometry '$GEOMETRY'" + + [ "$INITFILE" = false ] && ARGS="$ARGS -q" + + if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then + ARGS="$ARGS -T Isabelle" + [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && installfonts + else + ARGS="$ARGS -nw" + XSYMBOL=false + fi + + [ ! "$XSYMBOLSETUP" = true ] && XSYMBOL_HOME="" + + + ARGS="$ARGS -l '$SUPER/isa/interface-setup.el'" + + if [ -n "$KEYWORDS" ]; then + if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then + ARGS="$ARGS -l '$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el'" + elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then + ARGS="$ARGS -l '$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el'" + else + fail "No isar-keywords file for '$KEYWORDS'" + fi + elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then + ARGS="$ARGS -l '$ISABELLE_HOME_USER/etc/isar-keywords.el'" + elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then + ARGS="$ARGS -l '$ISABELLE_HOME/etc/isar-keywords.el'" + fi + + for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ + "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" + do + [ -f "$FILE" ] && ARGS="$ARGS -l '$FILE'" + done + + case "$LOGIC" in + /*) + ;; + */*) + LOGIC="$PWD/$LOGIC" + ;; + esac + + PROOFGENERAL_HOME="$SUPER" + PROOFGENERAL_ASSISTANTS="$KIND" + PROOFGENERAL_LOGIC="$LOGIC" + PROOFGENERAL_XSYMBOL="$XSYMBOL" + + export PROOFGENERAL_HOME PROOFGENERAL_ASSISTANTS PROOFGENERAL_LOGIC PROOFGENERAL_XSYMBOL + export ISABELLE_OPTIONS + + eval exec "$PROGNAME" "$ARGS" "$FILES" + +fi diff --git a/isa/interface-setup.el b/isa/interface-setup.el new file mode 100644 index 00000000..2ed504cb --- /dev/null +++ b/isa/interface-setup.el @@ -0,0 +1,48 @@ +;; 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> +;; +;; $Id$ +;; + +;;; +;;; X-Symbol +;;; + +(if (string-match "XEmacs" emacs-version) ;current X-Symbol works with XEmacs only! + (let ((xsymbol-home (getenv "XSYMBOL_HOME")) + (xsymbol (getenv "PROOFGENERAL_XSYMBOL")) + (enable-var + (if (equal (getenv "PROOFGENERAL_ASSISTANTS") "isa") + 'isa-x-symbol-enable 'isar-x-symbol-enable))) + ;; setup the x-symbol package, if not already present + (if (and xsymbol-home + (not (equal xsymbol-home "")) + (not (fboundp 'x-symbol-initialize)) + (not (get 'x-symbol 'x-symbol-initialized))) + (progn + (load (expand-file-name "lisp/x-symbol/auto-autoloads" xsymbol-home)) + (push (expand-file-name "lisp/x-symbol" xsymbol-home) load-path) + (if (boundp 'data-directory-list) + (push (expand-file-name "etc/" xsymbol-home) data-directory-list)) + (if (boundp 'Info-directory-list) + (push (expand-file-name "info/" xsymbol-home) Info-directory-list)) + (if (not (boundp 'x-symbol-image-converter)) ;avoid confusing warning message + (customize-set-variable 'x-symbol-image-converter nil)) + (x-symbol-initialize))) + ;; tell Proof General about -x option + (if (and xsymbol (not (equal xsymbol ""))) + (customize-set-variable enable-var (equal xsymbol "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 new file mode 100644 index 00000000..d8697cb8 --- /dev/null +++ b/isa/isa-syntax.el @@ -0,0 +1,304 @@ +;; isa-syntax.el Syntax expressions for Isabelle +;; Copyright (C) 1994-1998 LFCS Edinburgh. +;; +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Maintainer: Proof General maintainer <proofgen@dcs.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-decl + '("val" "fun" "datatype" "signature" "structure") + "Isabelle keywords for declarations. Includes ML keywords to fontify ML files." + :group 'isa-syntax + :type '(repeat string)) + +(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)) + +;; 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-decl + isa-keywords-defn isa-keywords-commands) + "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) + +(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) + + +(defvar isa-font-lock-keywords-1 + (list + (cons (proof-ids-to-regexp isa-keywords) 'font-lock-keyword-face) + (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 new file mode 100644 index 00000000..245c17d0 --- /dev/null +++ b/isa/isa.el @@ -0,0 +1,765 @@ +;; isa-mode.el Emacs support for Isabelle proof assistant +;; Copyright (C) 1993-2000 LFCS Edinburgh, David Aspinall. +;; +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Contact: isa@proofgeneral.org +;; +;; $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. +;; +;; ----------------------------------------------------------------- + + +;; Add Isabelle image onto splash screen +;; +;; (don't use customize-set-variable since it will be saved with options!) +(setq proof-splash-extensions + '(list + nil + (proof-splash-display-image "isabelle_transparent" t))) + +;; 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-comment-start "(*" ; comment in a proof + proof-comment-end "*)" ; + ;; Next few used for func-menu and recognizing goal..save regions in + ;; script buffer. + proof-save-command-regexp 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\";" + + ;; 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... + proof-shell-next-error-regexp + "\\(error on \\|Error: in '[^']+', \\)line \\([0-9]+\\)\\|The error(s) above occurred" + proof-shell-next-error-filename-regexp + "\\(Loading theory \"\\|Error: in '\\)\\([^\"']+\\)[\"']" + proof-shell-next-error-extract-filename + "%s.thy")) + + + +(defun isa-shell-mode-config-set-variables () + "Configure generic proof shell mode variables for Isabelle." + (setq + proof-shell-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" + proof-shell-goal-char ?\370 + + proof-shell-proof-completed-regexp "^No subgoals!" + + ;; initial command configures Isabelle by hacking print functions, + ;; restoring settings saved by Proof General, etc. + + ;; FIXME: temporary hack for almost enabling/disabling printing. + ;; Also for setting default values. + proof-shell-pre-sync-init-cmd "ProofGeneral.init false;" + proof-shell-init-cmd (proof-assistant-settings-cmd) + + proof-shell-restart-cmd "ProofGeneral.isa_restart();" + proof-shell-quit-cmd "quit();" + + ;; NB: the settings below will only recognize tracing output in + ;; Isabelle 2001. + 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 + + ;; 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: #\\([^#]+\\)#\\." + proof-shell-theorem-dependency-list-regexp "Proof General, the theorem dependencies are: \"\\([^\"]*\\)\"" + + ;; Dirty hack to allow font-locking for output based on hidden + ;; annotations, see isa-output-font-lock-keywords-1 + proof-shell-leave-annotations-in-output t + + ;; === ANNOTATIONS === ones here are broken + proof-shell-result-start "\372 Pbp result \373" + proof-shell-result-end "\372 End Pbp result \373" + proof-analyse-using-stack t + proof-shell-start-char ?\372 + proof-shell-end-char ?\373 + proof-shell-field-char ?\374 + + ;; === MULTIPLE FILE HANDLING === + 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 proof-shell-erase-response-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 + (span-property (prev-span span 'type) 'cmd))) + (concat "choplev 0" proof-terminal-string) + (while span + (setq str (span-property span 'cmd)) + (cond ((eq (span-property span 'type) 'vanilla) + (or (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 (str) + "Decide whether argument is a goal or not" + (proof-string-match isa-goal-command-regexp str)) ; this regexp defined in isa-syntax.el + +;; Isabelle has no concept of a Linear context, so forgetting back +;; to the declaration of a particular something makes no real +;; sense. Perhaps in the future there will be functions to remove +;; theorems from theories, but even then all we could do is +;; forget particular theorems one by one. 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) + (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. +(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 pbp-change-goal "Show %s.") + (setq pbp-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)))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; 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-isa.el +;; + +(setq proof-xsym-extra-modes '(thy-mode) + proof-xsym-activate-command + "print_mode := ([\"xsymbols\",\"symbols\"] @ ! print_mode);" + proof-xsym-deactivate-command + "print_mode := (! print_mode \\\\ [\"xsymbols\",\"symbols\"]);") + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; 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! + )) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Theorem dependencies (experimental) +;; + +(defpacustom theorem-dependencies nil + "Whether to track theorem dependencies within Proof General." + :type 'boolean + ;; when this is built-in (or with a ":=%b" setting). + ;; :setting ("depends_enable()" . "depends_disable()") + :eval (isa-theorem-dependencies-switch)) + +(defvar isa-dependsml-file-loaded nil) + +(add-hook 'proof-shell-kill-function-hooks + (lambda () (setq isa-dependsml-file-loaded nil))) + +(defun isa-load-dependsml-file () + ;; NB: maybe doesn't work if enabled before Isabelle starts. + (if (proof-shell-available-p) + (progn + (proof-shell-invisible-command + (proof-format-filename + "use \"%r\";" + (concat (file-name-directory + (locate-library "isa")) + "depends.ML"))) + (setq isa-dependsml-file-loaded t)))) + +(defun isa-theorem-dependencies-switch () + "Switch on/off theorem dependency tracking. (Experimental feature)." + (if (and isa-theorem-dependencies (not isa-dependsml-file-loaded)) + (isa-load-dependsml-file)) + (proof-shell-invisible-command (if isa-theorem-dependencies + "depends_enable()" + "depends_disable()"))) + + + + + +(provide 'isa) diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el new file mode 100644 index 00000000..01d98767 --- /dev/null +++ b/isa/isabelle-system.el @@ -0,0 +1,382 @@ +;; 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) + +(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") + (let ((possibilities + '("/usr/bin/isatool" + "/usr/share/Isabelle/bin/isatool" + "/usr/local/bin/isatool" + "/usr/local/Isabelle/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) + +(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) + (while (unless proof-running-on-win32 + (not (file-executable-p isa-isatool-command))) + (beep) + (setq isa-isatool-command + (read-file-name + "Please type in the full path to the `isatool' program: " + nil nil t))) + (if (and proof-running-on-win32 + (not (file-executable-p isa-isatool-command))) + (warning "Proof General: isatool command not found; ignored because Win32 system detected.")) + (file-executable-p isa-isatool-command)) + +(defun isa-shell-command-to-string (command) + "Like shell-command-to-string except the last character is stripped." + ;; FIXME: sometimes the command may fail. This will usually cause PG + ;; to break. Bit of an effort to trap errors here, we would need + ;; to provide some advice to shell-command-to-string to retain result + ;; of call to call-process, and raise and error in case it failed. + (substring (shell-command-to-string command) 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)) + "*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. + +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 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." + ;; a little bit obnoxious maybe (but what naive user would expect) + ;; (customize-save-variable 'isabelle-chosen-logic logic) + (customize-set-variable 'isabelle-chosen-logic logic) + (setq isabelle-prog-name (isabelle-command-line)) + (setq proof-prog-name isabelle-prog-name)) + +(defun isa-tool-list-logics () + "Generate a list of available object logics." + (if (isa-set-isatool-command) + (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)))) + +(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 "") + (mapcar + (function (lambda (docdes) + (list + (substring docdes + (proof-string-match "\\(\\S-+\\)[ \t]+" docdes) + (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 "\\`polyml" (isa-getenv "ML_SYSTEM")) + (not (proof-string-match "\\`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-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.") + + +;; It's a hassle to bother trying to reconstruct this +;; dynamically like it was in Isamode, so we don't bother. + +(defconst isabelle-logics-menu + (cons "Logics" + (cons + ["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))) + (isa-tool-list-logics)))) + "Isabelle logics menu. Constructed when PG is loaded.") + + + +;;; ========== Mirroring Proof General options in Isabelle process ======== + +;; NB: use of defpacustom here gives separate customizable +;; options for Isabelle and Isabelle/Isar. + +(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 "Library.error_fn := (fn _ => ()); Library.try (fn () => Context.use_mltext \"ProofGeneral.full_proofs %b;\" false None) ();") +;FIXME should become "ProofGeneral.full_proofs %b;" next time + +(defpacustom global-timing nil + "Whether to enable timing in Isabelle." + :type 'boolean + :setting "Library.timing:=%b;") + +(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;") + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; 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) + +(setq proof-xsym-font-lock-keywords + ;; fontification for tokens themselves (FIXME: broken) + '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face)))) + +(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))) + (if (featurep 'completion) + (proof-add-completions)))) + + + + +(provide 'isabelle-system) +;; End of isabelle-system.el diff --git a/isa/thy-mode.el b/isa/thy-mode.el new file mode 100644 index 00000000..07e0ca54 --- /dev/null +++ b/isa/thy-mode.el @@ -0,0 +1,1047 @@ +;; thy-mode.el - Mode for Isabelle theory files. +;; +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Maintainer: Isabelle maintainer <isabelle@dcs.ed.ac.uk> +;; +;; 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 isa-thy- + +(require 'proof-site) +(require 'proof-syntax) +(require 'isa) + +;;; ========== 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]) + proof-shared-menu + ;; begin UGLY COMPATIBILTY HACK + ;; older/non-existent customize doesn't have + ;; this function. + (if (fboundp 'customize-menu-create) + (list (customize-menu-create 'proof-general) + (customize-menu-create + 'proof-general-internals + "Internals")) + nil) + ;; end UGLY COMPATIBILTY HACK + ))) + (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 new file mode 100644 index 00000000..8e68bc23 --- /dev/null +++ b/isa/todo @@ -0,0 +1,84 @@ +-*- mode:outline -*- + +* Things to do for Isabelle + +See also ../todo for generic things to do, priority codes. + +** 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 Investigate fix for looping rewriting in Isabelle. Continual + and frequent messages from the prover lock out the user. + Is there any easy way of fixing this? + +** 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 weird bug: interrupting Isabelle process (under sml-nj) sometimes + doesn't return, why? (see first half of interrupt error only: + + *** Interrupt. + *** At command "time_use". + + uncaught exception ERROR + raised at: library.ML:1100.35-1100.40 + But not "uncaught exception" part. + What is worse: prompt disappears! But process still seems to be + there underneath. Not sure where this bug comes from. + + Moreover, killing process then hangs Emacs with message + "cleaning up", and get error + (1) (error/warning) Error in process sentinel: (no-catch exited t) + + To see if this is some SML/NJ or Isabelle weirdness, test in + xterm: use "ROOT.ML", interrrupt, use "ROOT.ML" again. + sig 11! (flaky hardware?) + /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2ad09c43 + Not reliably repeatable, but: + ProofGeneral.isa_restart(); + /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2af9e01b + +** 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-isabelle.el b/isa/x-symbol-isabelle.el new file mode 100644 index 00000000..f9938491 --- /dev/null +++ b/isa/x-symbol-isabelle.el @@ -0,0 +1,410 @@ +;; ID: $Id$ +;; Author: David von Oheimb +;; Copyright 1998 Technische Universitaet Muenchen +;; token language "Isabelle Symbols" for package x-symbol +;; +;; NB: Part of Proof General distribution. +;; + +(defvar x-symbol-isabelle-required-fonts nil) + +;; FIXME da: these next two are also set in proof-x-symbol.el, but +;; it's handy to use this file away from PG. In future could +;; fix things so just (require 'proof-x-symbol) would be enough +;; here. +(defvar x-symbol-isabelle-name "Isabelle Symbol") +(defvar x-symbol-isabelle-modeline-name "isa") + +(defvar x-symbol-isabelle-header-groups-alist nil) +;'(("Operator" bigop operator) +; ("Relation" relation) +; ("Arrow, Punctuation" arrow triangle shape +; white line dots punctuation quote parenthesis) +; ("Symbol" symbol currency mathletter setsymbol) +; ("Greek Letter" greek greek1) +; ("Acute, Grave" acute grave)) +; "*If non-nil, used in isasym specific grid/menu." + +(defvar x-symbol-isabelle-class-alist + '((VALID "Isabelle Symbol" (x-symbol-info-face)) + (INVALID "no Isabelle Symbol" (red x-symbol-info-face)))) +(defvar x-symbol-isabelle-class-face-alist nil) +(defvar x-symbol-isabelle-electric-ignore "[:'][A-Za-z]\\|<=\\|\\[\\[\\|\\]\\]\\|~=") + + +;; Bold, super- and subscripts + +(defun x-symbol-isabelle-make-ctrl-regexp (s) + (concat "\\(\\\\?\\\\<\\^" s ">\\)\\(\\\\?\\\\<[A-Za-z][A-Za-z0-9_']*>\\|[^\\]\\)")) + +(defconst x-symbol-isabelle-font-lock-bold-regexp + (x-symbol-isabelle-make-ctrl-regexp "bold") + "Regexp matching bold marker in Isabelle.") + +(defconst x-symbol-isabelle-font-lock-scripts-regexp + (x-symbol-isabelle-make-ctrl-regexp "su[bp]") + "Regexp matching super- and subscript markers in Isabelle.") + +(defun x-symbol-isabelle-match-bold (limit) + ;; checkdoc-params: (limit) + "Match and skip over bold face. +Return nil if `x-symbol-mode' is nil. +Uses `x-symbol-isabelle-font-lock-bold-regexp'." + (and (proof-ass x-symbol-enable) + (or (proof-looking-at x-symbol-isabelle-font-lock-bold-regexp) + (proof-re-search-forward x-symbol-isabelle-font-lock-bold-regexp limit t)))) + +(defun x-symbol-isabelle-match-scripts (limit) + ;; checkdoc-params: (limit) + "Match and skip over super- and subscripts. +Return nil if `x-symbol-mode' is nil. +Uses `x-symbol-isabelle-font-lock-scripts-regexp'." + (and (proof-ass x-symbol-enable) + (or (proof-looking-at x-symbol-isabelle-font-lock-scripts-regexp) + (proof-re-search-forward x-symbol-isabelle-font-lock-scripts-regexp limit t)))) + +(defvar x-symbol-isabelle-font-lock-keywords + '((x-symbol-isabelle-match-bold + (1 x-symbol-invisible-face t) + (2 'underline prepend)) + (x-symbol-isabelle-match-scripts + (1 x-symbol-invisible-face t) + (2 (if (or (eq (char-after (+ 5 (match-beginning 1))) ?b) + (eq (char-after (+ 6 (match-beginning 1))) ?b)) + 'x-symbol-sub-face 'x-symbol-sup-face) prepend))) + "Isabelle font-lock keywords for bold, super- and subscripts.") + + +(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) + +(defvar x-symbol-isabelle-case-insensitive nil) +;(defvar x-symbol-isabelle-token-shape '(?\\ "\\\\\\<[A-Za-z][A-Za-z0-9_']*>\\a'" . "[A-Za-z]")) +(defvar x-symbol-isabelle-token-shape nil) + +(defvar x-symbol-isabelle-exec-specs '(nil ("\\`\\\\<[A-Za-z][A-Za-z0-9_']*>\\'" . + "\\\\<[A-Za-z][A-Za-z0-9_']*>"))) + +(defvar x-symbol-isabelle-input-token-ignore nil) +(defun x-symbol-isabelle-default-token-list (tokens) tokens) + + +(defvar x-symbol-isabelle-token-list 'x-symbol-isabelle-default-token-list) + +(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>") + (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>") + (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) + (let* + ((is-isar (eq proof-assistant-symbol 'isar)) + (prfx1 (if is-isar "" "\\")) + (prfx2 (if is-isar "\\" ""))) + (mapcar (lambda (entry) + (list (car entry) '() (concat prfx1 (cadr entry)) (concat prfx2 (cadr entry)))) + table))) + +(defvar x-symbol-isabelle-table + (x-symbol-isabelle-prepare-table + (append + (if (boundp 'x-symbol-isabelle-user-table) x-symbol-isabelle-user-table nil) + x-symbol-isabelle-symbol-table + x-symbol-isabelle-xsymbol-table))) + +(defvar x-symbol-user-table + (append + (if (boundp 'x-symbol-user-table) x-symbol-user-table nil) + '((bardash 180 (arrow) (direction east . perpendicular) nil (t "|-")) + (bardashdbl 182 (arrow) (direction east) nil (t "|="))))) + + +;;;=========================================================================== +;;; Internal +;;;=========================================================================== + +(defvar x-symbol-isabelle-menu-alist nil + "Internal. Alist used for Isasym specific menu.") +(defvar x-symbol-isabelle-grid-alist nil + "Internal. Alist used for Isasym specific grid.") + +(defvar x-symbol-isabelle-decode-atree nil + "Internal. Atree used by `x-symbol-token-input'.") +(defvar x-symbol-isabelle-decode-alist nil + "Internal. Alist used for decoding of Isasym macros.") +(defvar x-symbol-isabelle-encode-alist nil + "Internal. Alist used for encoding to Isasym macros.") + +(defvar x-symbol-isabelle-nomule-decode-exec nil + "Internal. File name of Isasym decode executable.") +(defvar x-symbol-isabelle-nomule-encode-exec nil + "Internal. File name of Isasym encode executable.") + + + +;;;=========================================================================== +;;; useful key bindings +;;;=========================================================================== + + +;; FIXME: these break some standard bindings, and should only be set +;; for proof shell, script (or minibuffer) modes. + +;(global-set-key [(meta l)] 'x-symbol-INSERT-lambda) + +;(global-set-key [(meta n)] 'x-symbol-INSERT-notsign) +;(global-set-key [(meta a)] 'x-symbol-INSERT-logicaland) +;(global-set-key [(meta o)] 'x-symbol-INSERT-logicalor) +;(global-set-key [(meta f)] 'x-symbol-INSERT-universal1) +;(global-set-key [(meta t)] 'x-symbol-INSERT-existential1) + +;(global-set-key [(meta A)] 'x-symbol-INSERT-biglogicaland) +;(global-set-key [(meta e)] 'x-symbol-INSERT-equivalence) +;(global-set-key [(meta u)] 'x-symbol-INSERT-notequal) +;(global-set-key [(meta m)] 'x-symbol-INSERT-arrowdblright) + +;(global-set-key [(meta i)] 'x-symbol-INSERT-longarrowright) + +(provide 'x-symbol-isabelle) |