diff options
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/BUGS | 9 | ||||
| -rw-r--r-- | isar/Example.thy | 25 | ||||
| -rw-r--r-- | isar/README | 28 | ||||
| -rw-r--r-- | isar/interface | 166 | ||||
| -rw-r--r-- | isar/isar-keywords.el | 396 | ||||
| -rw-r--r-- | isar/isar-syntax.el | 390 | ||||
| -rw-r--r-- | isar/isar.el | 547 | ||||
| -rw-r--r-- | isar/todo | 27 |
8 files changed, 1588 insertions, 0 deletions
diff --git a/isar/BUGS b/isar/BUGS new file mode 100644 index 00000000..baddf520 --- /dev/null +++ b/isar/BUGS @@ -0,0 +1,9 @@ +-*- mode:outline -*- + +* Isabelle/Isar Proof General Bugs + +See also ../BUGS for generic bugs. + +Nothing specific here, check isa/BUGS for some issues that may apply +to Isar as well. + diff --git a/isar/Example.thy b/isar/Example.thy new file mode 100644 index 00000000..22c0a4e1 --- /dev/null +++ b/isar/Example.thy @@ -0,0 +1,25 @@ +(* -*- isar -*- + + Example proof document for Isabelle/Isar Proof General. + + $Id$ + + The first line forces Isabelle/Isar Proof General, otherwise + you may get the theory mode of ordinary Isabelle Proof General + See the manual for other ways to select Isabelle/Isar PG. +*) + +theory Example = Main: + +theorem and_comms: "A & B --> B & A" +proof + assume "A & B" + thus "B & A" + proof + assume A B + show ?thesis + .. + qed +qed + +end diff --git a/isar/README b/isar/README new file mode 100644 index 00000000..c87965ce --- /dev/null +++ b/isar/README @@ -0,0 +1,28 @@ +Isabelle/Isar Proof General + +Written by Markus Wenzel + +$Id$ + +Status: supported +Maintainer: Markus Wenzel +Isabelle version: 99-1 +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. + +There is no support for proof by pointing yet, and no tags program. + +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. diff --git a/isar/interface b/isar/interface new file mode 100644 index 00000000..ffc45cbc --- /dev/null +++ b/isar/interface @@ -0,0 +1,166 @@ +#!/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 " -X BOOL configure the X-Symbol package on startup (default true)" + 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="" +LOGIC="$ISABELLE_LOGIC" +PROGNAME="xemacs" +INITFILE="true" +WINDOWSYSTEM="true" +XSYMBOL="" +XSYMBOLSETUP=true + +getoptions() +{ + OPTIND=1 + while getopts "I:X:l:m:p:u:w:x:" OPT + do + case "$OPT" in + I) + ISAR="$OPTARG" + ;; + X) + XSYMBOLSETUP="$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 + + +## main + +ARGS="" + +[ "$INITFILE" = false ] && ARGS="$ARGS -q" + +if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then + ARGS="$ARGS -T Isabelle" + [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && "$ISATOOL" installfonts -x +else + ARGS="$ARGS -nw" + XSYMBOL=false +fi + +[ ! "$XSYMBOLSETUP" = true ] && XSYMBOL_HOME="" + + +ARGS="$ARGS -l '$SUPER/isa/interface-setup.el'" + +for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ + "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" +do + [ -f "$FILE" ] && ARGS="$ARGS -l '$FILE'" +done + +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" diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el new file mode 100644 index 00000000..780e7d16 --- /dev/null +++ b/isar/isar-keywords.el @@ -0,0 +1,396 @@ +;; +;; Keyword classification tables for Isabelle/Isar. +;; This file generated by Isabelle -- DO NOT EDIT! +;; +;; $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..d56c4961 --- /dev/null +++ b/isar/isar-syntax.el @@ -0,0 +1,390 @@ +;; isar-syntax.el Syntax expressions for Isabelle/Isar +;; Copyright (C) 1994-1998 LFCS Edinburgh. +;; +;; 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 ?\* ". 23") + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4") + (modify-syntax-entry ?\{ "(}1") + (modify-syntax-entry ?\} "){4")) + +(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-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. { }) + +(defun isar-ids-to-regexp (l) + "Maps a non-empty list of tokens `l' to a regexp matching any element" + (mapconcat + (lambda (s) (if (string-match "^\\W$" s) s (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 (theorem.*):" + "^goal (lemma.*):" + "^goal (have.*):" + "^goal (show.*):" + "^picking this:" + "^using this:" + "^this:" + "^term bindings:" + "^facts:" + "^cases:" + "^prems:" + "^fixed variables:" + "^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-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..a1356705 --- /dev/null +++ b/isar/isar.el @@ -0,0 +1,547 @@ +;; isar.el Major mode for Isabelle/Isar proof assistant +;; Copyright (C) 1994-1998 LFCS Edinburgh. +;; +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author / Maintainer: Markus Wenzel <wenzelm@in.tum.de> +;; +;; $Id$ +;; + + +;; Add Isabelle image onto splash screen +(customize-set-variable + 'proof-splash-extensions + '(list + nil + (proof-splash-display-image "isabelle_transparent" t))) + +;; In case Isar mode was invoked directly or by -*- isar -*- at +;; the start of the file, ensure that Isar mode is used from now +;; on for .thy files. +;; FIXME: be less messy with auto-mode-alist here (remove dups) +(setq auto-mode-alist + (cons '("\\.thy$" . isar-mode) auto-mode-alist)) + +(require 'proof) +(require 'isar-syntax) + +;; Completion table for Isabelle/Isar identifiers +(defpgdefault completion-table isar-keywords-major) + +;; Add generic code for Isabelle and Isabelle/Isar +(setq load-path (cons (concat proof-home-directory "isa/") load-path)) +(require 'isabelle-system) +(require 'x-symbol-isabelle) + +(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-comment-end)) + (cmt-start-regexp (regexp-quote proof-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 (buffer-syntactic-context)) + (delete-backward-char 1))))) + + +(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 + isar-any-command-regexp + (regexp-quote ";")) + proof-comment-start isar-comment-start + proof-comment-end isar-comment-end + proof-comment-start-regexp isar-comment-start-regexp + proof-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 nil + 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 + ;; da: for pbp. + ;; proof-goal-hyp-fn 'isar-goal-hyp + proof-state-preserving-p 'isar-state-preserving-p + proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list)) + +(defun isar-shell-mode-config-set-variables () + "Configure generic proof shell mode variables for Isabelle/Isar." + (setq + proof-shell-first-special-char ?\350 + + proof-shell-wakeup-char ?\372 + proof-shell-annotated-prompt-regexp "^\\w*[>#] \372" + + ;; This pattern is just for comint. + proof-shell-prompt-pattern "^\\w*[>#] " + + ;; for issuing command, not used to track cwd in any way. + proof-shell-cd-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\\|\360Interrupt" + proof-shell-error-regexp "\364\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " + proof-shell-abort-goal-regexp nil ; n.a. + + ;; matches names of assumptions + proof-shell-assumption-regexp isar-id + ;; matches subgoal name + ;; da: not used at the moment, maybe after 3.0 used for + ;; proof-generic-goal-hyp-fn to get pbp-like features. + ;; proof-shell-goal-regexp "\370[ \t]*\\([0-9]+\\)\\." + + proof-shell-start-goals-regexp "\366\n" + proof-shell-end-goals-regexp "\367" + proof-shell-goal-char ?\370 + + proof-assistant-setting-format 'isar-markup-ml + proof-shell-init-cmd (proof-assistant-settings-cmd) + proof-shell-restart-cmd "ProofGeneral.restart" + proof-shell-quit-cmd "quit();" + + proof-shell-eager-annotation-start-length 1 + proof-shell-eager-annotation-start "\360\\|\362" + proof-shell-eager-annotation-end "\361\\|\363" + + ;; Some messages delimited by eager annotations + proof-shell-clear-response-regexp "Proof General, please clear the response buffer." + proof-shell-clear-goals-regexp "Proof General, please clear the goals buffer." + + ;; Dirty hack to allow font-locking for output based on hidden + ;; annotations, see isar-output-font-lock-keywords-1 + proof-shell-leave-annotations-in-output t + + ;; === ANNOTATIONS === ones below here are broken + proof-shell-result-start "\372 Pbp result \373" + proof-shell-result-end "\372 End Pbp result \373" + proof-analyse-using-stack t + proof-shell-start-char ?\372 + proof-shell-end-char ?\373 + proof-shell-field-char ?\374 + + 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.") + + +;; +;; Define the derived modes +;; +(eval-and-compile +(define-derived-mode isar-shell-mode proof-shell-mode + "Isabelle/Isar shell" nil + (isar-shell-mode-config))) + +(eval-and-compile +(define-derived-mode isar-response-mode proof-response-mode + "Isabelle/Isar response" nil + (isar-response-mode-config))) + +(eval-and-compile ; to define vars for byte comp. +(define-derived-mode isar-goals-mode proof-goals-mode + "Isabelle/Isar proofstate" nil + (isar-goals-mode-config))) + +(eval-and-compile ; to define vars for byte comp. +(define-derived-mode isar-mode proof-mode + "Isabelle/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-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] + ["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) + (setq ct (+ 1 ct)))) + ((eq (span-property span 'type) 'pbp) + ;; this case probably redundant for Isabelle, unless + ;; we think of some nice ways of matching non-undoable + ;; commands. + (cond ((not (proof-string-match isar-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 or diagnostic command: skip + ((or (eq (span-property span 'type) 'comment) + (proof-string-match isar-undo-skip-regexp str))) + ;; finished goal: undo + ((eq (span-property span 'type) 'proof) + (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 + (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)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; 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)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Configuring proof and pbp mode and setting up various utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun isar-preprocessing () ;dynamic scoping of `string' + "Insert sync markers - acts on variable STRING by dynamic scoping" + (if (string-match isabelle-verbatim-regexp string) + (setq string (match-string 1 string)) + (unless (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 (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 ;FIXME handle x-symbol stuff by generic code!? + (append isar-output-font-lock-keywords-1 x-symbol-isabelle-font-lock-keywords)) + (isar-shell-mode-config-set-variables) + (proof-shell-config-done)) + +(defun isar-response-mode-config () + (setq font-lock-keywords ;FIXME handle x-symbol stuff by generic code!? + (append isar-output-font-lock-keywords-1 x-symbol-isabelle-font-lock-keywords)) + (isar-init-output-syntax-table) + (proof-response-config-done)) + +(defun isar-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) + (isar-init-output-syntax-table) + (setq font-lock-keywords ;FIXME handle x-symbol stuff by generic code!? + (append isar-goals-font-lock-keywords x-symbol-isabelle-font-lock-keywords)) + (proof-goals-config-done)) + + +;; +;; x-symbol support +;; +;; The following settings configure the generic PG package; the main +;; part is in 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 := (! print_mode \\\\ [\"xsymbols\",\"symbols\"])")) + + +(provide 'isar) diff --git a/isar/todo b/isar/todo new file mode 100644 index 00000000..912019c0 --- /dev/null +++ b/isar/todo @@ -0,0 +1,27 @@ +-*- mode:outline -*- + +* Things to do for Isabelle/Isar + +See also ../todo for generic things to do, priority codes. + +** 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); + +** C tune behaviour of goals/response buffers (e.g. hide empty +response buffers when using 2 buffer model); + +** D Combine with isa/ to get single Isabelle PG instance, somehow? +Then users could use both proof languages in the same session. + +** D Fixup so that typing in shell buffer updates locked buffer status. +It works in Isabelle/classic, why not here? (But users shouldn't +type in shell buffer, anyway). + +** D support proof-next-error? |