diff options
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/BUGS | 21 | ||||
| -rw-r--r-- | isar/Example.thy | 43 | ||||
| -rw-r--r-- | isar/README | 33 | ||||
| -rw-r--r-- | isar/interface | 236 | ||||
| -rw-r--r-- | isar/isar-keywords.el | 403 | ||||
| -rw-r--r-- | isar/isar-syntax.el | 425 | ||||
| -rw-r--r-- | isar/isar.el | 613 | ||||
| -rw-r--r-- | isar/isartags | 86 | ||||
| -rw-r--r-- | isar/todo | 17 |
9 files changed, 1877 insertions, 0 deletions
diff --git a/isar/BUGS b/isar/BUGS new file mode 100644 index 00000000..11564906 --- /dev/null +++ b/isar/BUGS @@ -0,0 +1,21 @@ +-*- mode:outline -*- + +* Isabelle/Isar Proof General Bugs + +See also ../BUGS for generic bugs. + +** Issues with tracing mode + +1. Large volumes of output can cause Emacs to hog CPU spending +all its time processing the output (esp with fontifying and X-symbol +decoding). It becomes difficult to use normal editing commands, +even C-c C-c to interrupt the prover. Workaround: hitting C-g, +the Emacs quit key, will interrupt the prover in this state. +See manual for further description of this. + +2. Interrupt response may be lost in large volumes of output, when +using pty communication. Symptom is interrupt on C-g, but PG thinks +the prover is still busy. Workaround: hit return in the shell buffer, +or set proof-shell-process-connection-type to nil to use piped +communication. + diff --git a/isar/Example.thy b/isar/Example.thy new file mode 100644 index 00000000..fc72c2f7 --- /dev/null +++ b/isar/Example.thy @@ -0,0 +1,43 @@ +(* + Example proof document for Isabelle/Isar Proof General. + + $Id$ +*) + +theory Example = Main: + +text {* Proper proof text -- naive version. *} + +theorem and_comms: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then + show ?thesis .. + qed +qed + + +text {* Proper proof text -- advanced version. *} + +theorem "A & B --> B & A" +proof + assume "A & B" + then obtain B and A .. + then show "B & A" .. +qed + + +text {* Unstructured proof script. *} + +theorem "A & B --> B & A" + apply (rule impI) + apply (erule conjE) + apply (rule conjI) + apply assumption + apply assumption +done + +end diff --git a/isar/README b/isar/README new file mode 100644 index 00000000..7f63c136 --- /dev/null +++ b/isar/README @@ -0,0 +1,33 @@ +Isabelle/Isar Proof General + +Written by Markus Wenzel + +Status: supported +Maintainer: David Aspinall +Isabelle versions: Isabelle99-1, Isabelle99-2, Isabelle2002 +Isabelle homepage: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ +Isar homepage: http://isabelle.in.tum.de/Isar/ + +======================================== + +Isabelle/Isar Proof General has full support for multiple file +scripting, with dependencies between theories communicated between +Isabelle and Proof General. + +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. + +The script `interface' and file 'interface-setup.el' are used +internally to start Isabelle Proof General via the 'Isabelle' shell +command. This is the default way to invoke Proof General from the +Isabelle perspective; it enables Isabelle to provide a consistent +process and file-system environment, including the all-important +isar-keywords.el file. + +Check the value of isabelle-prog-name. + +======================================== + +$Id$ + diff --git a/isar/interface b/isar/interface new file mode 100644 index 00000000..46c78a58 --- /dev/null +++ b/isar/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/isar/isar-keywords.el b/isar/isar-keywords.el new file mode 100644 index 00000000..7a3742bd --- /dev/null +++ b/isar/isar-keywords.el @@ -0,0 +1,403 @@ +;; +;; Keyword classification tables for Isabelle/Isar. +;; This file generated by Isabelle99-2 -- DO NOT EDIT! +;; +;; NB: This version is for Isabelle99. +;; +;; Isabelle2002 is supplied with a different version of this file +;; which should be loaded instead. See also the "-k" option +;; to the Isabelle script. +;; +;; $Id$ +;; + +(defconst isar-keywords-major + '("\\." + "\\.\\." + "ML" + "ML_command" + "ML_setup" + "ProofGeneral\\.context_thy_only" + "ProofGeneral\\.inform_file_processed" + "ProofGeneral\\.inform_file_retracted" + "ProofGeneral\\.kill_proof" + "ProofGeneral\\.restart" + "ProofGeneral\\.try_context_thy_only" + "ProofGeneral\\.undo" + "also" + "apply" + "apply_end" + "arities" + "assume" + "automaton" + "axclass" + "axioms" + "back" + "by" + "cannot_undo" + "case" + "cd" + "chapter" + "classes" + "classrel" + "clear_undos" + "coinductive" + "commit" + "constdefs" + "consts" + "context" + "datatype" + "declare" + "def" + "defaultsort" + "defer" + "defer_recdef" + "defs" + "disable_pr" + "done" + "enable_pr" + "end" + "exit" + "finally" + "fix" + "from" + "global" + "have" + "header" + "hence" + "hide" + "inductive" + "inductive_cases" + "init_toplevel" + "instance" + "judgment" + "kill" + "kill_thy" + "lemma" + "lemmas" + "let" + "local" + "method_setup" + "moreover" + "next" + "nonterminals" + "note" + "obtain" + "oops" + "oracle" + "parse_ast_translation" + "parse_translation" + "pr" + "prefer" + "presume" + "pretty_setmargin" + "primrec" + "print_antiquotations" + "print_ast_translation" + "print_attributes" + "print_binds" + "print_cases" + "print_claset" + "print_commands" + "print_context" + "print_facts" + "print_methods" + "print_simpset" + "print_syntax" + "print_theorems" + "print_theory" + "print_trans_rules" + "print_translation" + "proof" + "prop" + "pwd" + "qed" + "quit" + "recdef" + "recdef_tc" + "record" + "redo" + "remove_thy" + "rep_datatype" + "sect" + "section" + "setup" + "show" + "sorry" + "subsect" + "subsection" + "subsubsect" + "subsubsection" + "syntax" + "term" + "text" + "text_raw" + "then" + "theorem" + "theorems" + "theory" + "thm" + "thm_deps" + "thms_containing" + "thus" + "token_translation" + "touch_all_thys" + "touch_child_thys" + "touch_thy" + "translations" + "txt" + "txt_raw" + "typ" + "typed_print_translation" + "typedecl" + "typedef" + "types" + "ultimately" + "undo" + "undos_proof" + "update_thy" + "update_thy_only" + "use" + "use_thy" + "use_thy_only" + "welcome" + "with" + "{" + "}" + )) + +(defconst isar-keywords-minor + '("actions" + "and" + "binder" + "compose" + "con_defs" + "concl" + "congs" + "distinct" + "files" + "hide_action" + "hints" + "in" + "induction" + "infixl" + "infixr" + "initially" + "inject" + "inputs" + "internals" + "intros" + "is" + "monos" + "output" + "outputs" + "overloaded" + "post" + "pre" + "rename" + "restrict" + "signature" + "states" + "to" + "transitions" + "transrel" + "using" + "where")) + +(defconst isar-keywords-control + '("ProofGeneral\\.context_thy_only" + "ProofGeneral\\.inform_file_processed" + "ProofGeneral\\.inform_file_retracted" + "ProofGeneral\\.kill_proof" + "ProofGeneral\\.restart" + "ProofGeneral\\.try_context_thy_only" + "ProofGeneral\\.undo" + "cannot_undo" + "clear_undos" + "exit" + "init_toplevel" + "kill" + "quit" + "redo" + "undo" + "undos_proof")) + +(defconst isar-keywords-diag + '("ML" + "ML_command" + "cd" + "commit" + "disable_pr" + "enable_pr" + "header" + "kill_thy" + "pr" + "pretty_setmargin" + "print_antiquotations" + "print_attributes" + "print_binds" + "print_cases" + "print_claset" + "print_commands" + "print_context" + "print_facts" + "print_methods" + "print_simpset" + "print_syntax" + "print_theorems" + "print_theory" + "print_trans_rules" + "prop" + "pwd" + "remove_thy" + "term" + "thm" + "thm_deps" + "thms_containing" + "touch_all_thys" + "touch_child_thys" + "touch_thy" + "typ" + "update_thy" + "update_thy_only" + "use" + "use_thy" + "use_thy_only" + "welcome")) + +(defconst isar-keywords-theory-begin + '("theory")) + +(defconst isar-keywords-theory-switch + '("context")) + +(defconst isar-keywords-theory-end + '("end")) + +(defconst isar-keywords-theory-heading + '("chapter" + "section" + "subsection" + "subsubsection")) + +(defconst isar-keywords-theory-decl + '("ML_setup" + "arities" + "automaton" + "axclass" + "axioms" + "classes" + "classrel" + "coinductive" + "constdefs" + "consts" + "datatype" + "defaultsort" + "defer_recdef" + "defs" + "global" + "hide" + "inductive" + "judgment" + "lemmas" + "local" + "method_setup" + "nonterminals" + "oracle" + "parse_ast_translation" + "parse_translation" + "primrec" + "print_ast_translation" + "print_translation" + "recdef" + "record" + "rep_datatype" + "setup" + "syntax" + "text" + "text_raw" + "theorems" + "token_translation" + "translations" + "typed_print_translation" + "typedecl" + "types")) + +(defconst isar-keywords-theory-script + '("declare" + "inductive_cases")) + +(defconst isar-keywords-theory-goal + '("instance" + "lemma" + "recdef_tc" + "theorem" + "typedef")) + +(defconst isar-keywords-qed + '("\\." + "\\.\\." + "by" + "done" + "sorry")) + +(defconst isar-keywords-qed-block + '("qed")) + +(defconst isar-keywords-qed-global + '("oops")) + +(defconst isar-keywords-proof-heading + '("sect" + "subsect" + "subsubsect")) + +(defconst isar-keywords-proof-goal + '("have" + "hence" + "show" + "thus")) + +(defconst isar-keywords-proof-block + '("next" + "proof")) + +(defconst isar-keywords-proof-open + '("{")) + +(defconst isar-keywords-proof-close + '("}")) + +(defconst isar-keywords-proof-chain + '("finally" + "from" + "then" + "ultimately" + "with")) + +(defconst isar-keywords-proof-decl + '("also" + "let" + "moreover" + "note" + "txt" + "txt_raw")) + +(defconst isar-keywords-proof-asm + '("assume" + "case" + "def" + "fix" + "presume")) + +(defconst isar-keywords-proof-asm-goal + '("obtain")) + +(defconst isar-keywords-proof-script + '("apply" + "apply_end" + "back" + "defer" + "prefer")) + +(provide 'isar-keywords) diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el new file mode 100644 index 00000000..849cb243 --- /dev/null +++ b/isar/isar-syntax.el @@ -0,0 +1,425 @@ +;; isar-syntax.el Syntax expressions for Isabelle/Isar +;; Copyright (C) 1994-1998 LFCS Edinburgh. +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Maintainer: Markus Wenzel <wenzelm@in.tum.de> +;; +;; $Id$ +;; + +(require 'proof-syntax) +(require 'isar-keywords) + + +;; ----- character syntax + +(defun isar-init-syntax-table () + "Set appropriate values for syntax table in current buffer." + (modify-syntax-entry ?\$ ".") + (modify-syntax-entry ?\/ ".") + (modify-syntax-entry ?\\ "w") + (modify-syntax-entry ?+ ".") + (modify-syntax-entry ?- ".") + (modify-syntax-entry ?= ".") + (modify-syntax-entry ?% ".") + (modify-syntax-entry ?< "w") + (modify-syntax-entry ?> "w") + (modify-syntax-entry ?\& ".") + (modify-syntax-entry ?. "w") + (modify-syntax-entry ?_ "w") + (modify-syntax-entry ?\' "w") + (modify-syntax-entry ?? "w") + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4") + (cond + (proof-running-on-XEmacs + ;; We classify {* sequences *} as comments, although + ;; they need to be passed as command args as text. + ;; NB: adding a comment sequence b seems to break + ;; buffer-syntactic-context, best to use emulated + ;; version. + (modify-syntax-entry ?\{ "(}5") + (modify-syntax-entry ?\} "){8") + (modify-syntax-entry ?\* ". 2367")) + ;; previous version confuses the two comment sequences, + ;; but works with buffer-syntactic-context. + ;;(modify-syntax-entry ?\{ "(}1") + ;;(modify-syntax-entry ?\} "){4") + ;;(modify-syntax-entry ?\* ". 23")) + (proof-running-on-Emacs21 + (modify-syntax-entry ?\{ "(}1b") + (modify-syntax-entry ?\} "){4b") + (modify-syntax-entry ?\* ". 23n")))) + + +(defun isar-init-output-syntax-table () + "Set appropriate values for syntax table for Isabelle output." + (isar-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 ?\} "){")) + + +;; ----- keyword groups + +(defconst isar-keywords-theory-enclose + (append isar-keywords-theory-begin + isar-keywords-theory-switch + isar-keywords-theory-end)) + +(defconst isar-keywords-theory + (append isar-keywords-theory-heading + isar-keywords-theory-decl + isar-keywords-theory-goal)) + +(defconst isar-keywords-save + (append isar-keywords-qed + isar-keywords-qed-block + isar-keywords-qed-global)) + +(defconst isar-keywords-proof-enclose + (append isar-keywords-proof-block + isar-keywords-proof-open + isar-keywords-proof-close + isar-keywords-qed-block)) + +(defconst isar-keywords-proof + (append isar-keywords-proof-heading + isar-keywords-proof-goal + isar-keywords-proof-chain + isar-keywords-proof-decl + isar-keywords-qed)) + +(defconst isar-keywords-proof-context + (append isar-keywords-proof-asm + isar-keywords-proof-asm-goal)) + +(defconst isar-keywords-local-goal + (append isar-keywords-proof-goal + isar-keywords-proof-asm-goal)) + +(defconst isar-keywords-improper + (append isar-keywords-theory-script + isar-keywords-proof-script + isar-keywords-qed-global)) + +(defconst isar-keywords-outline + isar-keywords-theory-heading) + +(defconst isar-keywords-fume + (append isar-keywords-theory-begin + isar-keywords-theory-heading + isar-keywords-theory-decl + isar-keywords-theory-script + isar-keywords-theory-goal)) + +(defconst isar-keywords-indent-open + (append isar-keywords-theory-goal + isar-keywords-proof-goal + isar-keywords-proof-asm-goal + isar-keywords-proof-open)) + +(defconst isar-keywords-indent-close + (append isar-keywords-save + isar-keywords-proof-close)) + +(defconst isar-keywords-indent-enclose + (append isar-keywords-proof-block + isar-keywords-proof-close + isar-keywords-qed-block)) + + +;; ----- regular expressions + +;; tuned version of proof-ids-to-regexp --- admit single non-word char +;; as well (e.g. { }) +;; FIXME FIXME FIXME +;; DA: this goes wrong for { and } in fact, because plain { and } in +;; `proof-script-command-start-regexp' also match with {* and *}, which +;; should not be considered as commands (breaks new parser). + +(defun isar-ids-to-regexp (l) + "Maps a non-empty list of tokens `l' to a regexp matching any element" + (mapconcat + (lambda (s) (if (proof-string-match "^\\W$" s) + ;; was just s + (cond + ;; FIXME: what we really want here is to match { or } + ;; _except_ when followed/preceded by *, but not to + ;; consider * as part of match. (Exclude punctuation??) + ;; That kind of construct is only allowed for whitespace, + ;; though. + ((string-equal s "{") "{[^\*]") + ((string-equal s "}") "[^\*]}") ;; FIXME wrong + (t s)) ; what else? + (concat "\\<" s "\\>"))) + l "\\|")) + +(defconst isar-long-id-stuff "\\([A-Za-z0-9'_.]+\\)") + +(defconst isar-id "\\([A-Za-z][A-Za-z0-9'_]*\\)") +(defconst isar-idx (concat isar-id "\\(\\.[0-9]+\\)?")) + +(defconst isar-string "\"\\(\\([^\"]\\|\\\\\"\\)*\\)\"") + +(defconst isar-any-command-regexp + (isar-ids-to-regexp isar-keywords-major) + "Regexp matching any Isabelle/Isar command keyword.") + +(defconst isar-name-regexp + (concat "\\s-*\\(" isar-string "\\|" isar-id "\\)\\s-*") + "Regexp matching Isabelle/Isar names, with contents grouped.") + +(defconst isar-tac-regexp + "\\<[A-Za-z][A-Za-z0-9'_]*_tac\\>" + "Regexp matching old-style tactic names") + +(defconst isar-save-command-regexp + (proof-anchor-regexp (isar-ids-to-regexp isar-keywords-save))) + +(defconst isar-global-save-command-regexp + (proof-anchor-regexp (isar-ids-to-regexp isar-keywords-qed-global))) + +(defconst isar-goal-command-regexp + (proof-anchor-regexp (isar-ids-to-regexp isar-keywords-theory-goal))) + +(defconst isar-local-goal-command-regexp + (proof-anchor-regexp (isar-ids-to-regexp isar-keywords-local-goal))) + +(defconst isar-comment-start "(*") +(defconst isar-comment-end "*)") +(defconst isar-comment-start-regexp (regexp-quote isar-comment-start)) +(defconst isar-comment-end-regexp (regexp-quote isar-comment-end)) + +(defconst isar-string-start-regexp "\"\\|{\\*") +(defconst isar-string-end-regexp "\"\\|\\*}") + + +;; antiquotations + +(defconst isar-antiq-regexp + (concat "\\(@{\\([^\"{}]+\\|" isar-string "\\)\\{0,7\\}}\\)") + "Regexp matching Isabelle/Isar antiquoations.") + +(defun isar-match-antiq (limit) + "Match Isabelle/Isar antiquotations." + (or + (and (proof-looking-at-syntactic-context) + (proof-looking-at isar-antiq-regexp)) + (let (done ans) + (while (not done) + (if (proof-re-search-forward isar-antiq-regexp limit t) + (and (proof-looking-at-syntactic-context) + (setq done t) (setq ans t)) + (setq done t))) + ans))) + + +;; ----- 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 isar-font-lock-keywords-1 + (list + (cons (isar-ids-to-regexp isar-keywords-minor) 'font-lock-type-face) + (cons (isar-ids-to-regexp isar-keywords-control) 'proof-error-face) + (cons (isar-ids-to-regexp isar-keywords-diag) 'proof-tacticals-name-face) + (cons (isar-ids-to-regexp isar-keywords-theory-enclose) 'font-lock-preprocessor-face) + (cons (isar-ids-to-regexp isar-keywords-theory) 'font-lock-keyword-face) + (cons (isar-ids-to-regexp isar-keywords-proof-enclose) 'font-lock-preprocessor-face) + (cons (isar-ids-to-regexp isar-keywords-proof) 'font-lock-keyword-face) + (cons (isar-ids-to-regexp isar-keywords-proof-context) 'proof-declaration-name-face) + (cons (isar-ids-to-regexp isar-keywords-improper) 'font-lock-reference-face) + (cons isar-tac-regexp 'font-lock-reference-face) + '(isar-match-antiq (0 'font-lock-variable-name-face prepend)))) + +(defvar isar-output-font-lock-keywords-1 + (list + (cons (concat "\351" isar-long-id-stuff "\350") 'isabelle-class-name-face) + (cons (concat "\352'" isar-id "\350") 'isabelle-tfree-name-face) + (cons (concat "\353\\?'" isar-idx "\350") 'isabelle-tvar-name-face) + (cons (concat "\354" isar-id "\350") 'isabelle-free-name-face) + (cons (concat "\355" isar-id "\350") 'isabelle-bound-name-face) + (cons (concat "\356\\?" isar-idx "\350") 'isabelle-var-name-face) + (cons (concat "\357" isar-id "\350") 'proof-declaration-name-face) + (cons (concat "\357\\?" isar-idx "\350") 'proof-declaration-name-face)) + "*Font-lock table for Isabelle terms.") + +(defvar isar-goals-font-lock-keywords + (append + (list + "^theory " + "^proof (prove):" + "^proof (state):" + "^proof (chain):" + "^goal .+:" + "^picking this:" + "^using this:" + "^this:" + "^term bindings:" + "^facts:" + "^cases:" + "^prems:" + "^fixed variables:" + "^structures:" + "^type constraints:" + "^default sorts:" + "^used type variable names:" + "^[Ff]lex-flex pairs:" + "^[Cc]onstants:" + "^[Vv]ariables:" + "^[Tt]ype variables:" + "^\\s-*[0-9][0-9]?\\. ") + isar-output-font-lock-keywords-1) + "*Font-lock table for Isabelle/Isar output.") + + +;; ----- variations on undo + +(defconst isar-undo "undo;") +(defconst isar-kill "kill;") + +(defun isar-remove (name) + (concat "init_toplevel; kill_thy \"" name "\";")) + +(defun isar-undos (i) + (if (> i 0) (concat "undos_proof " (int-to-string i) ";") + proof-no-command)) + +(defun isar-cannot-undo (cmd) + (concat "cannot_undo \"" cmd "\";")) + + +(defconst isar-undo-fail-regexp + (proof-anchor-regexp + (isar-ids-to-regexp (append isar-keywords-control isar-keywords-theory-end)))) + +(defconst isar-undo-skip-regexp + (proof-anchor-regexp (proof-regexp-alt (isar-ids-to-regexp isar-keywords-diag) ";"))) + +(defconst isar-undo-ignore-regexp + (proof-anchor-regexp "--")) + +(defconst isar-undo-remove-regexp + (concat + (proof-anchor-regexp (isar-ids-to-regexp isar-keywords-theory-begin)) + isar-name-regexp)) + +(defconst isar-undo-kill-regexp + (proof-anchor-regexp (isar-ids-to-regexp isar-keywords-theory-switch))) + + +;; ----- function-menu + +(defconst isar-any-entity-regexp + (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)" + "\\(" isar-name-regexp "[[:=]\\)?")) + +(defconst isar-named-entity-regexp + (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)" + isar-name-regexp "[[:=]")) + +(defconst isar-unnamed-entity-regexp + (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)")) + +(defconst isar-next-entity-regexps + (list isar-any-entity-regexp + (list isar-named-entity-regexp '(1 2)) + (list isar-unnamed-entity-regexp 1))) + + +;; ----- indentation + +(defconst isar-indent-any-regexp + (proof-regexp-alt isar-any-command-regexp "\\s(" "\\s)")) +(defconst isar-indent-inner-regexp + (proof-regexp-alt "[[]()]")) +(defconst isar-indent-enclose-regexp + (proof-regexp-alt (isar-ids-to-regexp isar-keywords-indent-enclose) "\\s)")) +(defconst isar-indent-open-regexp + (proof-regexp-alt (isar-ids-to-regexp isar-keywords-indent-open) "\\s(")) +(defconst isar-indent-close-regexp + (proof-regexp-alt (isar-ids-to-regexp isar-keywords-indent-close) "\\s)")) + + +;; ----- outline mode + +(defconst isar-outline-regexp + (concat "[ \t]*\\(" (isar-ids-to-regexp isar-keywords-outline) "\\)") + "Outline regexp for Isabelle/Isar documents") + +(defconst isar-outline-heading-end-regexp "\n") + + +(provide 'isar-syntax) diff --git a/isar/isar.el b/isar/isar.el new file mode 100644 index 00000000..8902ad49 --- /dev/null +++ b/isar/isar.el @@ -0,0 +1,613 @@ +;; isar.el Major mode for Isabelle/Isar proof assistant +;; Copyright (C) 1994-1998 LFCS Edinburgh. +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author / Maintainer: Markus Wenzel <wenzelm@in.tum.de> +;; +;; $Id$ +;; + +(require 'proof) + +;; +;; Add generic code for Isabelle and Isabelle/Isar +;; +(setq load-path (cons (concat proof-home-directory "isa/") load-path)) +(require 'isabelle-system) + +;; +;; Load syntax +;; +(defcustom isar-keywords-name nil + "Specifies a theory-specific keywords setting to use with Isar. +See -k option for Isabelle interface script." + :type 'string + :group 'isabelle-isar) + +(or (featurep 'isar-keywords) + ;; Pickup isar-keywords file from somewhere appropriate, + ;; giving user chance to set name of file, or based on + ;; name of logic. + (isabelle-load-isar-keywords + (or isar-keywords-name + isabelle-chosen-logic))) +(require 'isar-syntax) + + +;; Completion table for Isabelle/Isar identifiers +(defpgdefault completion-table isar-keywords-major) + +(defcustom isar-web-page + "http://isabelle.in.tum.de/Isar/" + "URL of web page for Isabelle/Isar." + :type 'string + :group 'isabelle-isar) + + +;; Adjust toolbar entries (must be done before proof-toolbar is loaded). + +(if proof-running-on-XEmacs + (setq isar-toolbar-entries + (remassoc 'qed (remassoc 'goal isar-toolbar-entries)))) + + +;;; +;;; theory header +;;; + +(defun isar-detect-header () + "Detect new-style theory header in current buffer" + (let ((header-regexp (isar-ids-to-regexp '("header" "theory"))) + (white-space-regexp "\\(\\s-\\|\n\\)+") + (cmt-end-regexp (regexp-quote proof-script-comment-end)) + (cmt-start-regexp (regexp-quote proof-script-comment-start)) + (found-header nil) forward-amount + (end (point-max)) (cont t) (cmt-level 0)) + (save-excursion + (goto-char (point-min)) + (while (and cont (< (point) end)) + (setq forward-amount 1) + (cond + ;; comments + ((proof-looking-at cmt-start-regexp) + (setq forward-amount (length (match-string 0))) + (incf cmt-level)) + ((proof-looking-at cmt-end-regexp) + (setq forward-amount (length (match-string 0))) + (decf cmt-level)) + ((> cmt-level 0)) + ;; white space + ((proof-looking-at white-space-regexp) + (setq forward-amount (length (match-string 0)))) + ;; theory header + ((proof-looking-at header-regexp) + (setq found-header t) + (setq cont nil)) + ;; bad stuff + (t + (setq cont nil))) + (and cont (forward-char forward-amount))) + found-header))) + + +(defun isar-strip-terminators () + "Remove explicit Isabelle/Isar command terminators `;' from the buffer." + (interactive) + (save-excursion + (goto-char (point-min)) + (while (search-forward ";" (point-max) t) + (if (not (proof-buffer-syntactic-context)) + (progn + (delete-backward-char 1) + (or (proof-looking-at ";\\|\\s-\\|$") + (insert " "))))))) + + +(defun isar-markup-ml (string) + "Return marked up version of ML command STRING for Isar." + (format "ML_command {* %s *};" string)) + + +(defun isar-mode-config-set-variables () + "Configure generic proof scripting mode variables for Isabelle/Isar." + (setq + proof-assistant-home-page isar-web-page + proof-mode-for-script 'isar-mode + ;; proof script syntax + proof-terminal-char ?\; ; forcibly ends a command + proof-script-command-start-regexp + (proof-regexp-alt + ;; FIXME: this gets { and } wrong: they must _not_ appear as {* *} + ;; because that's lexically a kind of comment. + isar-any-command-regexp + (regexp-quote ";")) + proof-script-integral-proofs t + ;; FIXME: use old parser for now to avoid { } problem + proof-script-use-old-parser t + proof-script-comment-start isar-comment-start + proof-script-comment-end isar-comment-end + proof-script-comment-start-regexp isar-comment-start-regexp + proof-script-comment-end-regexp isar-comment-end-regexp + proof-string-start-regexp isar-string-start-regexp + proof-string-end-regexp isar-string-end-regexp + + ;; Next few used for func-menu and recognizing goal..save regions in + ;; script buffer. + proof-save-command-regexp isar-save-command-regexp + proof-goal-command-regexp isar-goal-command-regexp + proof-goal-with-hole-regexp isar-named-entity-regexp ; da + proof-save-with-hole-regexp nil + proof-script-next-entity-regexps isar-next-entity-regexps + + proof-indent-enclose-offset (- proof-indent) + proof-indent-open-offset 0 + proof-indent-close-offset 0 + proof-indent-any-regexp isar-indent-any-regexp +; proof-indent-inner-regexp isar-indent-inner-regexp + proof-indent-enclose-regexp isar-indent-enclose-regexp + proof-indent-open-regexp isar-indent-open-regexp + proof-indent-close-regexp isar-indent-close-regexp + + ;; proof engine commands + proof-showproof-command "pr" + proof-goal-command "lemma \"%s\"" + proof-save-command "qed" + proof-context-command "print_context" + proof-info-command "welcome" + proof-kill-goal-command "ProofGeneral.kill_proof" + proof-find-theorems-command "thms_containing %s" + proof-shell-start-silent-cmd "disable_pr" + proof-shell-stop-silent-cmd "enable_pr" + ;; command hooks + proof-goal-command-p 'isar-goal-command-p + proof-really-save-command-p 'isar-global-save-command-p + proof-count-undos-fn 'isar-count-undos + proof-find-and-forget-fn 'isar-find-and-forget + proof-state-preserving-p 'isar-state-preserving-p + proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list + ;; span menu + proof-script-span-context-menu-extensions 'isabelle-create-span-menu)) + + +(defun isar-shell-mode-config-set-variables () + "Configure generic proof shell mode variables for Isabelle/Isar." + (setq + pg-subterm-first-special-char ?\350 + + proof-shell-wakeup-char ?\372 + proof-shell-annotated-prompt-regexp "^\\w*[>#] \372" + + ;; This pattern is just for comint. + proof-shell-prompt-pattern "^\\w*[>#] " + + ;; for issuing command, not used to track cwd in any way. + proof-shell-cd-cmd (isar-markup-ml "ThyLoad.add_path \"%s\"") + + ;; Escapes for filenames inside ML strings. + ;; We also make a hack for a bug in 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-filename) ; rough test for XEmacs on win32 + ;; Patterns to unixfy names. + ;; Jacques Fleuriot's patch in ML does this too: ("^[a-zA-Z]:" . "") + ;; But I'll risk leaving drive names in, not sure how to replace them. + '(("\\\\" . "/") ("\"" . "\\\"")) + ;; Normal case: quotation for backslash, quote mark. + '(("\\\\" . "\\\\") ("\"" . "\\\""))) + + proof-shell-proof-completed-regexp nil ; n.a. + proof-shell-interrupt-regexp "\364\\*\\*\\* Interrupt" + proof-shell-error-regexp "\364\\*\\*\\*" + proof-shell-abort-goal-regexp nil ; n.a. + + pg-next-error-regexp "\\((line \\([0-9]+\\) of \"[^\"]+\")\\)" + pg-next-error-filename-regexp "\\((line [0-9]+ of \"\\([^\"]+\\)\")\\)" + + ;; matches names of assumptions + proof-shell-assumption-regexp isar-id + ;; matches subgoal name + ;; da: not used at the moment, maybe after 4.0 used for + ;; proof-generic-goal-hyp-fn to get pg-goals-like features. + ;; proof-shell-goal-regexp "\370[ \t]*\\([0-9]+\\)\\." + + proof-shell-start-goals-regexp "\366\n" + proof-shell-end-goals-regexp "\367" + pg-topterm-char ?\370 + + ;; FIXME: next one is needed for backward compatibility. + ;; Would be nice to remove this somehow else, it's only used for + ;; Isar. One way would be to hack the (now obsolete) defpacustom calls. + ;; + ;; proof-assistant-setting-format 'isar-markup-ml + proof-shell-init-cmd '(proof-assistant-settings-cmd) + proof-shell-restart-cmd "ProofGeneral.restart" + + proof-shell-eager-annotation-start-length 1 + proof-shell-eager-annotation-start "\360\\|\362" + proof-shell-eager-annotation-end "\361\\|\363" + ;; see isar-pre-shell-start for proof-shell-trace-output-regexp + + ;; Isabelle is learning to talk PGIP... + proof-shell-match-pgip-cmd "<pgip" + proof-shell-issue-pgip-cmd 'isabelle-process-pgip + + ;; 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." + + ;; Theorem dependencies. NB: next regex anchored at end with eager annot end + proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\361" + proof-shell-theorem-dependency-list-split "\" \"" + proof-shell-show-dependency-cmd "thm %s;" + + ;; Allow font-locking for output based on hidden annotations, see + ;; isar-output-font-lock-keywords-1 + pg-use-specials-for-fontify t + + ;; === ANNOTATIONS === these ones are not implemented in Isabelle + proof-shell-result-start "\372 Pbp result \373" + proof-shell-result-end "\372 End Pbp result \373" + pg-subterm-anns-use-stack t + pg-subterm-start-char ?\372 + pg-subterm-sep-char ?\373 + pg-subterm-end-char ?\374 + pg-after-fontify-output-hook + (if proof-experimental-features + 'isabelle-convert-idmarkup-to-subterm 'pg-remove-specials) + pg-subterm-help-cmd "term %s" + + proof-shell-process-file + (cons + ;; Theory loader output + "Proof General, this file is loaded: \"\\(.*\\)\"" + (lambda (str) + (match-string 1 str))) + proof-shell-retract-files-regexp + "Proof General, you can unlock the file \"\\(.*\\)\"" + proof-shell-compute-new-files-list 'isar-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\"") + (add-hook 'proof-activate-scripting-hook 'isar-activate-scripting)) + + +;;; +;;; Theory loader operations +;;; + +(defun isar-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 (isar-remove-file name rest cmp-base) + (cons file (isar-remove-file name rest cmp-base)))))) + +(defun isar-shell-compute-new-files-list (str) + "Compute the new list of files read by the proof assistant. +This is called when Proof General spots output matching +proof-shell-retract-files-regexp." + (let* + ((name (match-string 1 str)) + (base-name (file-name-nondirectory name))) + (if (string= name base-name) + (isar-remove-file name proof-included-files-list t) + (isar-remove-file (file-truename name) proof-included-files-list nil)))) + +(defun isar-activate-scripting () + "Make sure the Isabelle/Isar toplevel is in a sane state." + (proof-cd-sync)) + + +;; +;; Define the derived modes +;; +(eval-and-compile +(define-derived-mode isar-shell-mode proof-shell-mode + "Isar shell" nil + (isar-shell-mode-config))) + +(eval-and-compile +(define-derived-mode isar-response-mode proof-response-mode + "response" nil + (isar-response-mode-config))) + +(eval-and-compile ; to define vars for byte comp. +(define-derived-mode isar-goals-mode proof-goals-mode + "proofstate" nil + (isar-goals-mode-config))) + +(eval-and-compile ; to define vars for byte comp. +(define-derived-mode isar-mode proof-mode + "Isar script" nil + (isar-mode-config))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Code that's Isabelle/Isar specific ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;; +;;; help menu +;;; + +;;; da: how about a `C-c C-a h ?' for listing available keys? + +;;; NB: definvisible must come after derived modes because uses +;;; isar-mode-map +(proof-definvisible isar-help-antiquotations "print_antiquotations" [h A]) +(proof-definvisible isar-help-attributes "print_attributes" [h a]) +(proof-definvisible isar-help-cases "print_cases" [h c]) +(proof-definvisible isar-help-claset "print_claset" [h C]) +(proof-definvisible isar-help-commands "print_commands" [h o]) +(proof-definvisible isar-help-facts "print_facts" [h f]) +(proof-definvisible isar-help-syntax "print_syntax" [h i]) +(proof-definvisible isar-help-induct-rules "print_induct_rules" [h I]) +(proof-definvisible isar-help-methods "print_methods" [h m]) +(proof-definvisible isar-help-simpset "print_simpset" [h S]) +(proof-definvisible isar-help-binds "print_binds" [h b]) +(proof-definvisible isar-help-theorems "print_theorems" [h t]) +(proof-definvisible isar-help-trans-rules "print_trans_rules" [h T]) + +(defpgdefault help-menu-entries + (append + isabelle-docs-menu + (list + (cons "Show me ..." + (list + ["antiquotations" isar-help-antiquotations t] + ["attributes" isar-help-attributes t] + ["cases" isar-help-cases t] + ["classical rules" isar-help-claset t] + ["commands" isar-help-commands t] + ["facts" isar-help-facts t] + ["inner syntax" isar-help-syntax t] + ["induct/cases rules" isar-help-induct-rules t] + ["methods" isar-help-methods t] + ["simplifier rules" isar-help-simpset t] + ["term bindings" isar-help-binds t] + ["theorems" isar-help-theorems t] + ["transitivity rules" isar-help-trans-rules t]))))) + +;; undo proof commands +(defun isar-count-undos (span) + "Count number of undos in a span, return the command needed to undo that far." + (let + ((case-fold-search nil) ;FIXME ?? + (ct 0) str i) + (while span + (setq str (span-property span 'cmd)) + (cond ((eq (span-property span 'type) 'vanilla) + (or (proof-string-match isar-undo-skip-regexp str) + (proof-string-match isar-undo-ignore-regexp str) + (setq ct (+ 1 ct)))) + ((eq (span-property span 'type) 'pbp) ;FIXME dead code? + ;; this case probably redundant for Isabelle, unless + ;; we think of some nice ways of matching non-undoable + ;; commands. + (cond ((not (proof-string-match isar-undo-skip-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))) + (isar-undos ct))) + +;; undo theory commands +(defun isar-find-and-forget (span) + "Return commands to be used to forget SPAN." + (let (str ans answers) + (while span + (setq str (span-property span 'cmd)) + (setq ans nil) + (cond + ;; comment, diagnostic, nested proof command: skip + ;; (da: adding new span types may break this code, + ;; ought to test for type 'cmd before looking at + ;; str below) + ;; FIXME: should adjust proof-nesting-depth here. + ((or (eq (span-property span 'type) 'comment) + (eq (span-property span 'type) 'proof); da: needed? + (proof-string-match isar-undo-skip-regexp str) + (proof-string-match isar-undo-ignore-regexp str))) + ;; finished goal: undo + ((eq (span-property span 'type) 'goalsave) + (setq ans isar-undo)) + ;; open goal: skip and exit + ((proof-string-match isar-goal-command-regexp str) + (setq span nil)) + ;; not undoable: fail and exit + ((proof-string-match isar-undo-fail-regexp str) + (setq answers nil) + (setq ans (isar-cannot-undo str)) + (setq span nil)) + ;; theory: remove and exit + ((proof-string-match isar-undo-remove-regexp str) + (setq ans (isar-remove (match-string 2 str))) + (setq span nil)) + ;; context switch: kill + ((proof-string-match isar-undo-kill-regexp str) + (setq ans isar-kill)) + ;; else: undo + (t + (setq ans isar-undo))) + (if ans (setq answers (cons ans answers))) + (if span (setq span (next-span span 'type)))) + (if (null answers) proof-no-command (apply 'concat answers)))) + + + +(defun isar-goal-command-p (str) + "Decide whether argument is a goal or not" + (proof-string-match isar-goal-command-regexp str)) + +(defun isar-global-save-command-p (span str) + "Decide whether argument really is a global save command" + (or + (proof-string-match isar-global-save-command-regexp str) + (let ((ans nil) (lev 0) cmd) + (while (and (not ans) span (setq span (prev-span span 'type))) + (setq cmd (span-property span 'cmd)) + (cond + ;; comment: skip + ((eq (span-property span 'type) 'comment)) + ;; local qed: enter block + ((proof-string-match isar-save-command-regexp cmd) + (setq lev (+ lev 1))) + ;; local goal: leave block, or done + ((proof-string-match isar-local-goal-command-regexp cmd) + (if (> lev 0) (setq lev (- lev 1)) (setq ans 'no))) + ;; global goal: done + ((proof-string-match isar-goal-command-regexp cmd) + (setq ans 'yes)))) + (eq ans 'yes)))) + +(defvar isar-current-goal 1 + "Last goal that emacs looked at.") + +(defun isar-state-preserving-p (cmd) + "Non-nil if command preserves the proofstate." + (proof-string-match isar-undo-skip-regexp cmd)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Commands specific to isar ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(proof-defshortcut isar-bold "\\<^bold>" [(control b)]) +(proof-defshortcut isar-super "\\<^sup>" [(control u)]) +(proof-defshortcut isar-sub "\\<^sub>" [(control l)]) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Isar shell startup and exit hooks ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;borrowed from plastic.el +(defvar isar-shell-current-line-width nil + "Current line width of the Isabelle process's pretty printing module. + Its value will be updated whenever the corresponding screen gets + selected.") + +;borrowed from plastic.el +(defun isar-shell-adjust-line-width () + "Use Isabelle's pretty printing facilities to adjust output line width. + Checks the width in the `proof-goals-buffer'" + (let ((ans "")) + (and (buffer-live-p proof-goals-buffer) + (proof-shell-live-buffer) + (save-excursion + (set-buffer proof-goals-buffer) + (let ((current-width + ;; Actually, one might sometimes + ;; want to get the width of the proof-response-buffer + ;; instead. Never mind. + (max 20 (window-width (get-buffer-window proof-goals-buffer))))) + + (if (equal current-width isar-shell-current-line-width) () + (setq isar-shell-current-line-width current-width) + (set-buffer proof-shell-buffer) + (setq ans (format "pretty_setmargin %d;" (- current-width 4))))))) + ans)) + +(defun isar-pre-shell-start () + (setq proof-prog-name (isabelle-command-line)) + (setq proof-mode-for-shell 'isar-shell-mode) + (setq proof-mode-for-goals 'isar-goals-mode) + (setq proof-mode-for-response 'isar-response-mode) + (setq proof-shell-trace-output-regexp "\375")) + + +;; +;; Configuring proof output buffer +;; + +(defun isar-preprocessing () ;dynamic scoping of `string' + "Insert sync markers - acts on variable STRING by dynamic scoping" + (if (proof-string-match isabelle-verbatim-regexp string) + (setq string (match-string 1 string)) + (unless (proof-string-match ";[ \t]*\\'" string) + (setq string (concat string ";"))) + (setq string (concat + "\\<^sync>" + (isar-shell-adjust-line-width) + ;; da: this was an attempted hack to deal with ML files, + ;; unfortunately Isar complains about not seeing a theory + ;; command first: ML_setup illegal at first line + ;; Another failure is that: (* comment *) foo; + ;; ignores foo. This could be fixed by scanning for + ;; comment end in proof-script.el's function + ;; proof-segment-upto-cmdstart (which becomes even more + ;; Isar specific, then...) + ;; (if (proof-string-match "\\.ML$" (buffer-name proof-script-buffer)) + ;; (format "ML_command {* %s *};" string) + ;; string) + string + " \\<^sync>;")))) + +(defun isar-mode-config () + (isar-mode-config-set-variables) + (isar-init-syntax-table) + (setq font-lock-keywords isar-font-lock-keywords-1) + (proof-config-done) + (set (make-local-variable 'outline-regexp) isar-outline-regexp) + (set (make-local-variable 'outline-heading-end-regexp) isar-outline-heading-end-regexp) + (setq blink-matching-paren-dont-ignore-comments t) + (add-hook 'proof-pre-shell-start-hook 'isar-pre-shell-start nil t) + (add-hook 'proof-shell-insert-hook 'isar-preprocessing)) + +(defun isar-shell-mode-config () + "Configure Proof General proof shell for Isabelle/Isar." + (isar-init-output-syntax-table) + (setq font-lock-keywords + (append + isar-output-font-lock-keywords-1 + (if (boundp 'x-symbol-isabelle-font-lock-keywords) + x-symbol-isabelle-font-lock-keywords))) + (isar-shell-mode-config-set-variables) + (proof-shell-config-done)) + +(defun isar-response-mode-config () + (isar-init-output-syntax-table) + (setq font-lock-keywords + (append + isar-output-font-lock-keywords-1 + (if (proof-ass x-symbol-enable) + x-symbol-isabelle-font-lock-keywords))) + (proof-response-config-done)) + +(defun isar-goals-mode-config () + ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO. + (setq pg-goals-change-goal "show %s.") + (setq pg-goals-error-regexp proof-shell-error-regexp) + (isar-init-output-syntax-table) + (setq font-lock-keywords + (append + isar-goals-font-lock-keywords + (if (proof-ass x-symbol-enable) + x-symbol-isabelle-font-lock-keywords))) + (proof-goals-config-done)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; x-symbol support +;; +;; The following settings configure the generic PG package. +;; The token language "Isabelle Symbols" is in file isa/x-symbol-isabelle.el +;; + +(setq + proof-xsym-activate-command + (isar-markup-ml "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode)") + proof-xsym-deactivate-command + (isar-markup-ml "print_mode := (Library.gen_rems (op =) (! print_mode, [\"xsymbols\", \"symbols\"]))")) + +(provide 'isar) diff --git a/isar/isartags b/isar/isartags new file mode 100644 index 00000000..0d65f8e6 --- /dev/null +++ b/isar/isartags @@ -0,0 +1,86 @@ +#!/usr/bin/perl +# +# Or perhaps: /usr/local/bin/perl +# +# FIXME: this code is just borrowed from legotags program, +# it isn't yet working! Please send us fixes. +# +# $Id$ +# +undef $/; + +if($#ARGV<$[) {die "No Files\n";} +open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n"; + +while(<>) +{ + print "Tagging $ARGV\n"; + $a=$_; + $cp=1; + $lp=1; + $tagstring=""; + + while(1) + { + +# ---- Get the next statement starting on a newline ---- + + if($a=~/^[ \t\n]*\(\*/) + { while($a=~/^\s*\(\*/) + { $d=1; $a=$'; $cp+=length $&; $lp+=(($wombat=$&)=~tr/\n/\n/); + while($d>0 && $a=~/\(\*|\*\)/) + { $a=$'; $cp+=2+length $`; $lp+=(($wombat=$`)=~tr/\n/\n/); + if($& eq "(*") {$d++} else {$d--}; + } + if($d!=0) {die "Unbalanced Comment?";} + } + } + + if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;} + while($a=~/^\n/) {$cp++;$lp++;$a=$'} + + if($a=~/^[^;]*;/) + { $stmt=$&; + $newa=$'; + $newcp=$cp+length $&; + $newlp=$lp+(($wombat=$&)=~tr/\n/\n/); } + else { last;} + +# ---- The above embarrasses itself if there are semicolons inside comments or +# ---- inside commands. Could do better. + +# print "----- (",$lp,",",$cp,")\n", $stmt, "\n"; + + if($stmt=~/^([ \t]*\$?theory\s*([\w\']+))\s*:/) + { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; } + + elsif($stmt=~/^([ \t]*\$?\[\s*[\w\']+)/) + { do adddecs($stmt,$1) } + + elsif($stmt=~/^([ \t]*Inductive\s*\[\s*[\w\']+)/) + { do adddecs($stmt,$1) } + +# ---- Maybe do something smart with discharge as well? + + $cp=$newcp; $lp=$newlp; $a=$newa; + } + print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; +} +close tagfile; + + +sub adddecs { + $wk=$_[0]; + $tag=$_[1]; + while($wk=~/\[\s*([\w\']+)/) + { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; + while($wk=~/^\s*,\s*([\w\']+)/) + { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; } + $d=1; + while($d>0 && $wk=~/\[|\]/) + { $wk=$'; if($& eq "[") {$d++} else {$d--}; + } + } + 0; +} + diff --git a/isar/todo b/isar/todo new file mode 100644 index 00000000..3b76d39a --- /dev/null +++ b/isar/todo @@ -0,0 +1,17 @@ +-*- mode:outline -*- + +* Things to do for Isabelle/Isar + +See also ../todo for generic things to do, priority codes. + +** B visualise dependencies: sometimes not applicable. + +** C func-menu: observe proof-syntactic-context (general problem of +func-menu setup?); + +** C undo 'use' command: unlock corresponding ML file; + +** C provide template for empty theory (or even just for Scratch.thy); + +** C proper proof-by-pointing support (hard; needs major reworking of +Isabelle's pretty-printing subsystem); |