# HG changeset patch # User wenzelm # Date 1296469109 -3600 # Node ID b9357f56fd640089dec306aacefb81d56ce39598 # Parent 4030fcc5c78531da658676ca8c073431e9fb63b3# Parent fcd67ce9810b3377bbdcdc1fdbfdfcf4b2e1415f merged diff -r 4030fcc5c785 -r b9357f56fd64 .hgtags --- a/.hgtags Fri Jan 28 11:26:08 2011 +1100 +++ b/.hgtags Mon Jan 31 11:18:29 2011 +0100 @@ -26,3 +26,4 @@ 5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009 6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1 35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2 +6d736d983d5cfec4a6c6fba174db2cd93493a96b Isabelle2011 diff -r 4030fcc5c785 -r b9357f56fd64 ANNOUNCE --- a/ANNOUNCE Fri Jan 28 11:26:08 2011 +1100 +++ b/ANNOUNCE Mon Jan 31 11:18:29 2011 +0100 @@ -1,34 +1,34 @@ -Subject: Announcing Isabelle2009-2 +Subject: Announcing Isabelle2011 To: isabelle-users@cl.cam.ac.uk -Isabelle2009-2 is now available. +Isabelle2011 is now available. -This release improves upon Isabelle2009-1 in many respects, see the -NEWS file in the distribution for more details. Some notable changes -are: +This version significantly improves upon Isabelle2009-2, see the NEWS +file in the distribution for more details. Some notable changes are: -* Explicit proof terms for type class reasoning. +* Experimental Prover IDE based on Isabelle/Scala and jEdit. + +* Coercive subtyping (configured in HOL/Complex_Main). -* Robust treatment of concrete syntax for different logical entities; -mixfix syntax in local proof context. +* HOL code generation: Scala as another target language. -* Type declarations and notation within local theory context. +* HOL: partial_function definitions. -* HOL: package for quotient types. +* HOL: various tool enhancements, including Quickcheck, Nitpick, + Sledgehammer, SMT integration. -* HOL code generation: simple concept for abstract datatypes obeying -invariants (e.g. red-black trees). +* HOL: various additions to theory library, including HOL-Algebra, + Imperative_HOL, Multivariate_Analysis, Probability. -* HOL: new development of the Reals using Cauchy Sequences. - -* HOL: reorganization of abstract algebra type class hierarchy. +* HOLCF: reorganization of library and related tools. -* HOL: substantial reorganization of main library and related tools. +* HOL/SPARK: interactive proof environment for verification conditions + generated by the SPARK Ada program verifier. -* HOLCF: reorganization of 'domain' package. +* Improved Isabelle/Isar implementation manual (covering Isabelle/ML). -You may get Isabelle2009-2 from the following mirror sites: +You may get Isabelle2011 from the following mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ diff -r 4030fcc5c785 -r b9357f56fd64 Admin/CHECKLIST --- a/Admin/CHECKLIST Fri Jan 28 11:26:08 2011 +1100 +++ b/Admin/CHECKLIST Mon Jan 31 11:18:29 2011 +0100 @@ -19,6 +19,8 @@ - check Admin/contributed_components; +- check funny base directory, e.g. "Test 中国"; + - diff NEWS wrt. last official release, which is read-only; - update https://isabelle.in.tum.de/repos/website; @@ -50,10 +52,12 @@ Final release stage =================== +- makedist: REPOS_NAME="isabelle-release" + - hgrc: default = /home/isabelle-repository/repos/isabelle-release isatest@macbroy28:hg-isabelle/.hg/hgrc isatest@atbroy102:hg-isabelle/.hg/hgrc -- makedist: REPOS_NAME="isabelle-release" +- isatest@macbroy28:devel-page/content/index.content diff -r 4030fcc5c785 -r b9357f56fd64 Admin/MacOS/App1/script --- a/Admin/MacOS/App1/script Fri Jan 28 11:26:08 2011 +1100 +++ b/Admin/MacOS/App1/script Mon Jan 31 11:18:29 2011 +0100 @@ -10,9 +10,12 @@ # sane environment defaults + cd "$HOME" PATH="$PATH:/opt/local/bin" +[ -z "$LANG" ] && export LANG=en_US.UTF-8 + # settings support @@ -54,10 +57,23 @@ fi +# enforce fonts + +if [ ! -f "$HOME/Library/Fonts/STIXGeneral.ttf" -a ! -f "$HOME/Library/Fonts/STIXGeneral.otf" ] +then + cp -f "$THIS/STIXv1.0.0/Fonts"/STIXGeneral* "$HOME/Library/Fonts/" + sleep 3 +fi + +EMACS_OPTIONS["${#EMACS_OPTIONS[@]}"]="-x" +EMACS_OPTIONS["${#EMACS_OPTIONS[@]}"]="true" + + # run interface with error feedback OUTPUT="/tmp/isabelle$$.out" +# ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1 ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1 RC=$? diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/3.7.1.1/interface --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/ProofGeneral/3.7.1.1/interface Mon Jan 31 11:18:29 2011 +0100 @@ -0,0 +1,262 @@ +#!/usr/bin/env bash +# +# interface,v 9.1 2008/02/06 15:40:45 makarius Exp +# +# Proof General interface wrapper for Isabelle. + + +## self references + +THIS="$(cd "$(dirname "$0")"; pwd)" +SUPER="$(cd "$THIS/.."; pwd)" + + +## diagnostics + +usage() +{ + echo + echo "Usage: Isabelle [OPTIONS] [FILES ...]" + echo + echo " Options are:" + echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)" + echo " -L NAME abbreviates -l NAME -k NAME" + echo " -P BOOL actually start Proof General (default true), otherwise" + echo " run plain tty session" + echo " -U BOOL enable Unicode (UTF-8) communication (default true)" + echo " -X BOOL configure the X-Symbol package on startup (default true)" + echo " -f SIZE set X-Symbol font size (default 12)" + 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 emacs)" + 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="" +ISAR="true" +START_PG="true" +GEOMETRY="" +KEYWORDS="" +LOGIC="$ISABELLE_LOGIC" +PROGNAME="emacs" +INITFILE="true" +WINDOWSYSTEM="true" +XSYMBOL="" +XSYMBOL_SETUP=true +XSYMBOL_FONTSIZE="12" +UNICODE="" + +getoptions() +{ + OPTIND=1 + while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT + do + case "$OPT" in + I) + ISAR="$OPTARG" + ;; + L) + KEYWORDS="$OPTARG" + LOGIC="$OPTARG" + ;; + P) + START_PG="$OPTARG" + ;; + U) + UNICODE="$OPTARG" + ;; + X) + XSYMBOL_SETUP="$OPTARG" + ;; + f) + XSYMBOL_FONTSIZE="$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 +} + +eval "OPTIONS=($PROOFGENERAL_OPTIONS)" +getoptions "${OPTIONS[@]}" + +getoptions "$@" +shift $(($OPTIND - 1)) + + +# args + +declare -a FILES=() + +if [ "$#" -eq 0 ]; then + FILES["${#FILES[@]}"]="Scratch.thy" +else + 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 + +# Isabelle2008 compatibility +[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE" +[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL" + +if [ "$START_PG" = false ]; then + + [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I" + exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC" + +else + + declare -a ARGS=() + + if [ -n "$GEOMETRY" ]; then + ARGS["${#ARGS[@]}"]="-geometry" + ARGS["${#ARGS[@]}"]="$GEOMETRY" + fi + + [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q" + + if [ "$WINDOWSYSTEM" = false ]; then + ARGS["${#ARGS[@]}"]="-nw" + XSYMBOL=false + elif [ -z "$DISPLAY" ]; then + XSYMBOL=false + else + [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts + fi + + if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ] + then + if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ] + then + cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/" + cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/" + sleep 3 + fi + fi + + ARGS["${#ARGS[@]}"]="-l" + ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el" + + if [ -n "$KEYWORDS" ]; then + if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then + ARGS["${#ARGS[@]}"]="-l" + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" + elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then + ARGS["${#ARGS[@]}"]="-l" + ARGS["${#ARGS[@]}"]="$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" + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el" + elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then + ARGS["${#ARGS[@]}"]="-l" + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el" + fi + + for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ + "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" + do + if [ -f "$FILE" ]; then + ARGS["${#ARGS[@]}"]="-l" + ARGS["${#ARGS[@]}"]="$FILE" + fi + done + + case "$LOGIC" in + /*) + ;; + */*) + LOGIC="$(pwd -P)/$LOGIC" + ;; + esac + + export PROOFGENERAL_HOME="$SUPER" + export PROOFGENERAL_ASSISTANTS="isar" + export PROOFGENERAL_LOGIC="$LOGIC" + export PROOFGENERAL_XSYMBOL="$XSYMBOL" + export PROOFGENERAL_UNICODE="$UNICODE" + + export ISABELLE_OPTIONS XSYMBOL_FONTSIZE + + exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}" + +fi diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch Mon Jan 31 11:18:29 2011 +0100 @@ -0,0 +1,21 @@ +--- a/isar/isar-syntax.el Wed Aug 06 11:43:47 2008 +0200 ++++ b/isar/isar-syntax.el Thu Sep 18 15:21:16 2008 +0200 +@@ -252,14 +252,9 @@ + + ;; antiquotations + +-;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for +-;; incomplete antiquotations like @{text bla"} (even though it is supposed to +-;; stop at eol anyway). +- +-(defconst isar-antiq-regexp +- (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}") +- "Regexp matching Isabelle/Isar antiquoations.") +- ++(defconst isar-antiq-regexp ++ (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}") ++ "Regexp matching Isabelle/Isar antiquotations.") + + ;; keyword nesting + + diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/3.7.1.1/menu.patch --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/ProofGeneral/3.7.1.1/menu.patch Mon Jan 31 11:18:29 2011 +0100 @@ -0,0 +1,30 @@ +--- a/isar/isar.el 2008-07-10 20:47:49.000000000 +0200 ++++ b/isar/isar.el 2009-11-26 20:51:44.103016094 +0100 +@@ -339,9 +339,12 @@ + (error "Aborted.")) + [(control p)]) + +-(proof-definvisible isar-cmd-refute "refute" [r]) + (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)]) ++(proof-definvisible isar-cmd-nitpick "nitpick" [(control n)]) ++(proof-definvisible isar-cmd-refute "refute" [r]) + (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)]) ++(proof-definvisible isar-cmd-atp-kill "atp_kill") ++(proof-definvisible isar-cmd-atp-info "atp_info") + + (defpgdefault menu-entries + (append +@@ -349,9 +352,12 @@ + (list + (cons "Commands" + (list +- ["refute" isar-cmd-refute t] + ["quickcheck" isar-cmd-quickcheck t] ++ ["nitpick" isar-cmd-nitpick t] ++ ["refute" isar-cmd-refute t] + ["sledgehammer" isar-cmd-sledgehammer t] ++ ["sledgehammer: kill" isar-cmd-atp-kill t] ++ ["sledgehammer: info" isar-cmd-atp-info t] + ["display draft" isar-cmd-display-draft t]))) + (list + (cons "Show me ..." diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/3.7.1.1/progname.patch --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/ProofGeneral/3.7.1.1/progname.patch Mon Jan 31 11:18:29 2011 +0100 @@ -0,0 +1,89 @@ +--- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200 ++++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100 +@@ -97,8 +97,8 @@ + (if (or proof-rsh-command + (file-executable-p isa-isatool-command)) + (let ((setting (isa-shell-command-to-string +- (concat isa-isatool-command +- " getenv -b " envvar)))) ++ (concat "\"" isa-isatool-command ++ "\" getenv -b " envvar)))) + (if (string-equal setting "") + default + setting)) +@@ -125,15 +125,12 @@ + :type 'file + :group 'isabelle) + +-(defvar isabelle-prog-name nil +- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.") +- + (defun isa-tool-list-logics () + "Generate a list of available object logics." + (if (isa-set-isatool-command) + (delete "" (split-string + (isa-shell-command-to-string +- (concat isa-isatool-command " findlogics")) "[ \t]")))) ++ (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]")))) + + (defcustom isabelle-logics-available nil + "*List of logics available to use with Isabelle. +@@ -177,7 +174,7 @@ + + (defun isabelle-set-prog-name (&optional filename) + "Make proper command line for running Isabelle. +-This function sets `isabelle-prog-name' and `proof-prog-name'." ++This function sets `proof-prog-name' and `isar-prog-args'." + (let* + ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run + ;; under the interface wrapper script) indicate command line +@@ -187,21 +184,20 @@ + (getenv "ISABELLE") ; command line override + (isa-getenv "ISABELLE") ; choose to match isatool + "isabelle")) ; to +- (isabelle-opts (getenv "ISABELLE_OPTIONS")) +- (opts (concat " -PI" ;; Proof General + Isar +- (if proof-shell-unicode " -m PGASCII" "") +- (if (and isabelle-opts (not (equal isabelle-opts ""))) +- (concat " " isabelle-opts) ""))) ++ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS"))) ++ (opts (append (list "-PI") ;; Proof General + Isar ++ (if proof-shell-unicode (list "-m" "PGASCII") nil) ++ isabelle-opts)) + (logic (or isabelle-chosen-logic + (getenv "PROOFGENERAL_LOGIC"))) + (logicarg (if (and logic (not (equal logic ""))) +- (concat " " logic) ""))) ++ (list logic) nil))) + (setq isabelle-chosen-logic-prev isabelle-chosen-logic) +- (setq isabelle-prog-name (concat isabelle opts logicarg)) +- (setq proof-prog-name isabelle-prog-name))) ++ (setq isar-prog-args (append opts logicarg)) ++ (setq proof-prog-name isabelle))) + + (defun isabelle-choose-logic (logic) +- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC." ++ "Adjust proof-prog-name and isar-prog-args for running LOGIC." + (interactive + (list (completing-read + "Use logic: " +@@ -224,9 +220,7 @@ + (if (isa-set-isatool-command) + (apply 'start-process + "isa-view-doc" nil +- (append (split-string +- isa-isatool-command) +- (list "doc" docname))))) ++ (list isa-isatool-command "doc" docname)))) + + (defun isa-tool-list-docs () + "Generate a list of documentation files available, with descriptions. +@@ -236,7 +230,7 @@ + passed to isa-tool-doc-command, DOCNAME will be viewed." + (if (isa-set-isatool-command) + (let ((docs (isa-shell-command-to-string +- (concat isa-isatool-command " doc")))) ++ (concat "\"" isa-isatool-command "\" doc")))) + (unless (string-equal docs "") + (mapcan + (function (lambda (docdes) diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/3.7.1.1/timeout.patch --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/ProofGeneral/3.7.1.1/timeout.patch Mon Jan 31 11:18:29 2011 +0100 @@ -0,0 +1,11 @@ +--- a/generic/proof-config.el 2008-07-21 18:37:10.000000000 +0200 ++++ b/generic/proof-config.el 2009-11-29 17:41:37.409062091 +0100 +@@ -1493,7 +1493,7 @@ + :type '(choice string (const nil)) + :group 'proof-shell) + +-(defcustom proof-shell-quit-timeout 4 ++(defcustom proof-shell-quit-timeout 45 + ;; FIXME could add option to quiz user before rude kill. + "The number of seconds to wait after sending proof-shell-quit-cmd. + After this timeout, the proof shell will be killed off more rudely. diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/3.7.1.1/version.patch --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/ProofGeneral/3.7.1.1/version.patch Mon Jan 31 11:18:29 2011 +0100 @@ -0,0 +1,20 @@ +--- a/generic/proof-site.el 2008-07-23 14:40:14.000000000 +0200 ++++ b/generic/proof-site.el 2009-11-28 16:13:56.409505412 +0100 +@@ -55,7 +55,7 @@ + + (eval-and-compile + ;; WARNING: do not edit next line (constant is edited in Makefile.devel) +- (defconst proof-general-version "Proof General Version 3.7.1. Released by da on Wed 23 Jul 2008." ++ (defconst proof-general-version "Proof General Version 3.7.1.1. Fabricated by makarius on Mon 30 Nov 2009." + "Version string identifying Proof General release.")) + + (defconst proof-general-short-version +@@ -64,7 +64,7 @@ + (string-match "Version \\([^ ]+\\)\\." proof-general-version) + (match-string 1 proof-general-version)))) + +-(defconst proof-general-version-year "2008") ++(defconst proof-general-version-year "2009") + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;; diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/4.1/dif --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/ProofGeneral/4.1/dif Mon Jan 31 11:18:29 2011 +0100 @@ -0,0 +1,39 @@ +diff -r ProofGeneral-4.1pre101216/generic/proof-useropts.el ProofGeneral-4.1pre101216-p1/generic/proof-useropts.el +121c121 +< (defcustom proof-strict-read-only 'retract +--- +> (defcustom proof-strict-read-only t +345c345 +< (defcustom proof-full-annotation t +--- +> (defcustom proof-full-annotation nil +diff -r ProofGeneral-4.1pre101216/isar/interface ProofGeneral-4.1pre101216-p1/isar/interface +3,4d2 +< # interface,v 11.0 2010/10/10 22:57:07 da Exp +< # +23a22 +> echo " -f FONT specify Emacs font" +56a56 +> FONT="" +66c66 +< while getopts "L:U:g:k:l:m:p:u:w:x:" OPT +--- +> while getopts "L:U:f:g:k:l:m:p:u:w:x:" OPT +75a76,78 +> f) +> FONT="$OPTARG" +> ;; +135a139,143 +> if [ -n "$FONT" ]; then +> ARGS["${#ARGS[@]}"]="-fn" +> ARGS["${#ARGS[@]}"]="$FONT" +> fi +> +diff -r ProofGeneral-4.1pre101216/isar/interface-setup.el ProofGeneral-4.1pre101216-p1/isar/interface-setup.el +13a14,19 +> ;; Tool bar +> ;; +> +> (if (and window-system (fboundp 'tool-bar-mode)) (tool-bar-mode t)) +> +> ;; diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/4.1/interface --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/ProofGeneral/4.1/interface Mon Jan 31 11:18:29 2011 +0100 @@ -0,0 +1,203 @@ +#!/usr/bin/env bash +# +# Proof General interface wrapper for Isabelle. + + +## self references + +THIS="$(cd "$(dirname "$0")"; pwd)" +SUPER="$(cd "$THIS/.."; pwd)" + + +## diagnostics + +usage() +{ + echo + echo "Usage: isabelle emacs [OPTIONS] [FILES ...]" + echo + echo " Options are:" + echo " -L NAME abbreviates -l NAME -k NAME" + echo " -U BOOL enable UTF-8 communication (default true)" + echo " -f FONT specify Emacs font" + 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 emacs)" + echo " -u BOOL use personal .emacs file (default true)" + echo " -w BOOL use window system (default true)" + echo " -x BOOL render Isabelle symbols via Unicode (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="" + +KEYWORDS="" +LOGIC="$ISABELLE_LOGIC" +UNICODE="" +FONT="" +GEOMETRY="" +PROGNAME="emacs" +INITFILE="true" +WINDOWSYSTEM="true" +UNICODE_SYMBOLS="" + +getoptions() +{ + OPTIND=1 + while getopts "L:U:f:g:k:l:m:p:u:w:x:" OPT + do + case "$OPT" in + L) + KEYWORDS="$OPTARG" + LOGIC="$OPTARG" + ;; + U) + UNICODE="$OPTARG" + ;; + f) + FONT="$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) + UNICODE_SYMBOLS="$OPTARG" + ;; + \?) + usage + ;; + esac + done +} + +eval "OPTIONS=($PROOFGENERAL_OPTIONS)" +getoptions "${OPTIONS[@]}" + +getoptions "$@" +shift $(($OPTIND - 1)) + + +# args + +declare -a FILES=() + +if [ "$#" -eq 0 ]; then + FILES["${#FILES[@]}"]="Scratch.thy" +else + while [ "$#" -gt 0 ]; do + FILES["${#FILES[@]}"]="$1" + shift + done +fi + + +## main + +declare -a ARGS=() + +if [ -n "$FONT" ]; then + ARGS["${#ARGS[@]}"]="-fn" + ARGS["${#ARGS[@]}"]="$FONT" +fi + +if [ -n "$GEOMETRY" ]; then + ARGS["${#ARGS[@]}"]="-geometry" + ARGS["${#ARGS[@]}"]="$GEOMETRY" +fi + +[ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q" +[ "$WINDOWSYSTEM" = false ] && ARGS["${#ARGS[@]}"]="-nw" + +ARGS["${#ARGS[@]}"]="-l" +ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el" + +if [ -n "$KEYWORDS" ]; then + if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then + ARGS["${#ARGS[@]}"]="-l" + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" + elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then + ARGS["${#ARGS[@]}"]="-l" + ARGS["${#ARGS[@]}"]="$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" + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el" +elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then + ARGS["${#ARGS[@]}"]="-l" + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el" +fi + +for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ + "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" +do + if [ -f "$FILE" ]; then + ARGS["${#ARGS[@]}"]="-l" + ARGS["${#ARGS[@]}"]="$FILE" + fi +done + +case "$LOGIC" in + /*) + ;; + */*) + LOGIC="$(pwd -P)/$LOGIC" + ;; +esac + +export PROOFGENERAL_HOME="$SUPER" +export PROOFGENERAL_ASSISTANTS="isar" +export PROOFGENERAL_LOGIC="$LOGIC" +export PROOFGENERAL_UNICODE="$UNICODE" +export PROOFGENERAL_UNICODE_SYMBOLS="$UNICODE_SYMBOLS" + +export ISABELLE_OPTIONS + +# Isabelle2008 compatibility +[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE" +[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL" + +exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}" + diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/interface --- a/Admin/ProofGeneral/interface Fri Jan 28 11:26:08 2011 +1100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,262 +0,0 @@ -#!/usr/bin/env bash -# -# interface,v 9.1 2008/02/06 15:40:45 makarius Exp -# -# Proof General interface wrapper for Isabelle. - - -## self references - -THIS="$(cd "$(dirname "$0")"; pwd)" -SUPER="$(cd "$THIS/.."; pwd)" - - -## diagnostics - -usage() -{ - echo - echo "Usage: Isabelle [OPTIONS] [FILES ...]" - echo - echo " Options are:" - echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)" - echo " -L NAME abbreviates -l NAME -k NAME" - echo " -P BOOL actually start Proof General (default true), otherwise" - echo " run plain tty session" - echo " -U BOOL enable Unicode (UTF-8) communication (default true)" - echo " -X BOOL configure the X-Symbol package on startup (default true)" - echo " -f SIZE set X-Symbol font size (default 12)" - 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 emacs)" - 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="" -ISAR="true" -START_PG="true" -GEOMETRY="" -KEYWORDS="" -LOGIC="$ISABELLE_LOGIC" -PROGNAME="emacs" -INITFILE="true" -WINDOWSYSTEM="true" -XSYMBOL="" -XSYMBOL_SETUP=true -XSYMBOL_FONTSIZE="12" -UNICODE="" - -getoptions() -{ - OPTIND=1 - while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT - do - case "$OPT" in - I) - ISAR="$OPTARG" - ;; - L) - KEYWORDS="$OPTARG" - LOGIC="$OPTARG" - ;; - P) - START_PG="$OPTARG" - ;; - U) - UNICODE="$OPTARG" - ;; - X) - XSYMBOL_SETUP="$OPTARG" - ;; - f) - XSYMBOL_FONTSIZE="$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 -} - -eval "OPTIONS=($PROOFGENERAL_OPTIONS)" -getoptions "${OPTIONS[@]}" - -getoptions "$@" -shift $(($OPTIND - 1)) - - -# args - -declare -a FILES=() - -if [ "$#" -eq 0 ]; then - FILES["${#FILES[@]}"]="Scratch.thy" -else - 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 - -# Isabelle2008 compatibility -[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE" -[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL" - -if [ "$START_PG" = false ]; then - - [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I" - exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC" - -else - - declare -a ARGS=() - - if [ -n "$GEOMETRY" ]; then - ARGS["${#ARGS[@]}"]="-geometry" - ARGS["${#ARGS[@]}"]="$GEOMETRY" - fi - - [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q" - - if [ "$WINDOWSYSTEM" = false ]; then - ARGS["${#ARGS[@]}"]="-nw" - XSYMBOL=false - elif [ -z "$DISPLAY" ]; then - XSYMBOL=false - else - [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts - fi - - if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ] - then - if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ] - then - cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/" - cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/" - sleep 3 - fi - fi - - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el" - - if [ -n "$KEYWORDS" ]; then - if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" - elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$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" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el" - elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el" - fi - - for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ - "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" - do - if [ -f "$FILE" ]; then - ARGS["${#ARGS[@]}"]="-l" - ARGS["${#ARGS[@]}"]="$FILE" - fi - done - - case "$LOGIC" in - /*) - ;; - */*) - LOGIC="$(pwd -P)/$LOGIC" - ;; - esac - - export PROOFGENERAL_HOME="$SUPER" - export PROOFGENERAL_ASSISTANTS="isar" - export PROOFGENERAL_LOGIC="$LOGIC" - export PROOFGENERAL_XSYMBOL="$XSYMBOL" - export PROOFGENERAL_UNICODE="$UNICODE" - - export ISABELLE_OPTIONS XSYMBOL_FONTSIZE - - exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}" - -fi diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/isar-antiq-regexp.patch --- a/Admin/ProofGeneral/isar-antiq-regexp.patch Fri Jan 28 11:26:08 2011 +1100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ ---- a/isar/isar-syntax.el Wed Aug 06 11:43:47 2008 +0200 -+++ b/isar/isar-syntax.el Thu Sep 18 15:21:16 2008 +0200 -@@ -252,14 +252,9 @@ - - ;; antiquotations - --;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for --;; incomplete antiquotations like @{text bla"} (even though it is supposed to --;; stop at eol anyway). -- --(defconst isar-antiq-regexp -- (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}") -- "Regexp matching Isabelle/Isar antiquoations.") -- -+(defconst isar-antiq-regexp -+ (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}") -+ "Regexp matching Isabelle/Isar antiquotations.") - - ;; keyword nesting - - diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/menu.patch --- a/Admin/ProofGeneral/menu.patch Fri Jan 28 11:26:08 2011 +1100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ ---- a/isar/isar.el 2008-07-10 20:47:49.000000000 +0200 -+++ b/isar/isar.el 2009-11-26 20:51:44.103016094 +0100 -@@ -339,9 +339,12 @@ - (error "Aborted.")) - [(control p)]) - --(proof-definvisible isar-cmd-refute "refute" [r]) - (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)]) -+(proof-definvisible isar-cmd-nitpick "nitpick" [(control n)]) -+(proof-definvisible isar-cmd-refute "refute" [r]) - (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)]) -+(proof-definvisible isar-cmd-atp-kill "atp_kill") -+(proof-definvisible isar-cmd-atp-info "atp_info") - - (defpgdefault menu-entries - (append -@@ -349,9 +352,12 @@ - (list - (cons "Commands" - (list -- ["refute" isar-cmd-refute t] - ["quickcheck" isar-cmd-quickcheck t] -+ ["nitpick" isar-cmd-nitpick t] -+ ["refute" isar-cmd-refute t] - ["sledgehammer" isar-cmd-sledgehammer t] -+ ["sledgehammer: kill" isar-cmd-atp-kill t] -+ ["sledgehammer: info" isar-cmd-atp-info t] - ["display draft" isar-cmd-display-draft t]))) - (list - (cons "Show me ..." diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/progname.patch --- a/Admin/ProofGeneral/progname.patch Fri Jan 28 11:26:08 2011 +1100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,89 +0,0 @@ ---- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200 -+++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100 -@@ -97,8 +97,8 @@ - (if (or proof-rsh-command - (file-executable-p isa-isatool-command)) - (let ((setting (isa-shell-command-to-string -- (concat isa-isatool-command -- " getenv -b " envvar)))) -+ (concat "\"" isa-isatool-command -+ "\" getenv -b " envvar)))) - (if (string-equal setting "") - default - setting)) -@@ -125,15 +125,12 @@ - :type 'file - :group 'isabelle) - --(defvar isabelle-prog-name nil -- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.") -- - (defun isa-tool-list-logics () - "Generate a list of available object logics." - (if (isa-set-isatool-command) - (delete "" (split-string - (isa-shell-command-to-string -- (concat isa-isatool-command " findlogics")) "[ \t]")))) -+ (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]")))) - - (defcustom isabelle-logics-available nil - "*List of logics available to use with Isabelle. -@@ -177,7 +174,7 @@ - - (defun isabelle-set-prog-name (&optional filename) - "Make proper command line for running Isabelle. --This function sets `isabelle-prog-name' and `proof-prog-name'." -+This function sets `proof-prog-name' and `isar-prog-args'." - (let* - ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run - ;; under the interface wrapper script) indicate command line -@@ -187,21 +184,20 @@ - (getenv "ISABELLE") ; command line override - (isa-getenv "ISABELLE") ; choose to match isatool - "isabelle")) ; to -- (isabelle-opts (getenv "ISABELLE_OPTIONS")) -- (opts (concat " -PI" ;; Proof General + Isar -- (if proof-shell-unicode " -m PGASCII" "") -- (if (and isabelle-opts (not (equal isabelle-opts ""))) -- (concat " " isabelle-opts) ""))) -+ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS"))) -+ (opts (append (list "-PI") ;; Proof General + Isar -+ (if proof-shell-unicode (list "-m" "PGASCII") nil) -+ isabelle-opts)) - (logic (or isabelle-chosen-logic - (getenv "PROOFGENERAL_LOGIC"))) - (logicarg (if (and logic (not (equal logic ""))) -- (concat " " logic) ""))) -+ (list logic) nil))) - (setq isabelle-chosen-logic-prev isabelle-chosen-logic) -- (setq isabelle-prog-name (concat isabelle opts logicarg)) -- (setq proof-prog-name isabelle-prog-name))) -+ (setq isar-prog-args (append opts logicarg)) -+ (setq proof-prog-name isabelle))) - - (defun isabelle-choose-logic (logic) -- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC." -+ "Adjust proof-prog-name and isar-prog-args for running LOGIC." - (interactive - (list (completing-read - "Use logic: " -@@ -224,9 +220,7 @@ - (if (isa-set-isatool-command) - (apply 'start-process - "isa-view-doc" nil -- (append (split-string -- isa-isatool-command) -- (list "doc" docname))))) -+ (list isa-isatool-command "doc" docname)))) - - (defun isa-tool-list-docs () - "Generate a list of documentation files available, with descriptions. -@@ -236,7 +230,7 @@ - passed to isa-tool-doc-command, DOCNAME will be viewed." - (if (isa-set-isatool-command) - (let ((docs (isa-shell-command-to-string -- (concat isa-isatool-command " doc")))) -+ (concat "\"" isa-isatool-command "\" doc")))) - (unless (string-equal docs "") - (mapcan - (function (lambda (docdes) diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/timeout.patch --- a/Admin/ProofGeneral/timeout.patch Fri Jan 28 11:26:08 2011 +1100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ ---- a/generic/proof-config.el 2008-07-21 18:37:10.000000000 +0200 -+++ b/generic/proof-config.el 2009-11-29 17:41:37.409062091 +0100 -@@ -1493,7 +1493,7 @@ - :type '(choice string (const nil)) - :group 'proof-shell) - --(defcustom proof-shell-quit-timeout 4 -+(defcustom proof-shell-quit-timeout 45 - ;; FIXME could add option to quiz user before rude kill. - "The number of seconds to wait after sending proof-shell-quit-cmd. - After this timeout, the proof shell will be killed off more rudely. diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/version.patch --- a/Admin/ProofGeneral/version.patch Fri Jan 28 11:26:08 2011 +1100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ ---- a/generic/proof-site.el 2008-07-23 14:40:14.000000000 +0200 -+++ b/generic/proof-site.el 2009-11-28 16:13:56.409505412 +0100 -@@ -55,7 +55,7 @@ - - (eval-and-compile - ;; WARNING: do not edit next line (constant is edited in Makefile.devel) -- (defconst proof-general-version "Proof General Version 3.7.1. Released by da on Wed 23 Jul 2008." -+ (defconst proof-general-version "Proof General Version 3.7.1.1. Fabricated by makarius on Mon 30 Nov 2009." - "Version string identifying Proof General release.")) - - (defconst proof-general-short-version -@@ -64,7 +64,7 @@ - (string-match "Version \\([^ ]+\\)\\." proof-general-version) - (match-string 1 proof-general-version)))) - --(defconst proof-general-version-year "2008") -+(defconst proof-general-version-year "2009") - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; diff -r 4030fcc5c785 -r b9357f56fd64 Admin/isatest/isatest-stats --- a/Admin/isatest/isatest-stats Fri Jan 28 11:26:08 2011 +1100 +++ b/Admin/isatest/isatest-stats Mon Jan 31 11:18:29 2011 +0100 @@ -6,7 +6,7 @@ THIS=$(cd "$(dirname "$0")"; pwd -P) -PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev" +PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev" ISABELLE_SESSIONS="\ HOL-Plain \ diff -r 4030fcc5c785 -r b9357f56fd64 Admin/isatest/settings/mac-poly64-M4 --- a/Admin/isatest/settings/mac-poly64-M4 Fri Jan 28 11:26:08 2011 +1100 +++ b/Admin/isatest/settings/mac-poly64-M4 Mon Jan 31 11:18:29 2011 +0100 @@ -1,10 +1,10 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-5.4.0" - ML_SYSTEM="polyml-5.4.0" + POLYML_HOME="/home/polyml/polyml-svn" + ML_SYSTEM="polyml-5.4.1" ML_PLATFORM="x86_64-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="--mutable 4000 --immutable 4000" + ML_OPTIONS="--mutable 1000 --immutable 1000 --gcthreads 4" ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4 diff -r 4030fcc5c785 -r b9357f56fd64 Admin/isatest/settings/mac-poly64-M8 --- a/Admin/isatest/settings/mac-poly64-M8 Fri Jan 28 11:26:08 2011 +1100 +++ b/Admin/isatest/settings/mac-poly64-M8 Mon Jan 31 11:18:29 2011 +0100 @@ -1,10 +1,10 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-5.4.0" - ML_SYSTEM="polyml-5.4.0" + POLYML_HOME="/home/polyml/polyml-svn" + ML_SYSTEM="polyml-5.4.1" ML_PLATFORM="x86_64-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="--mutable 4000 --immutable 4000" + ML_OPTIONS="--mutable 1000 --immutable 1000 --gcthreads 8" ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8 diff -r 4030fcc5c785 -r b9357f56fd64 Admin/makebundle --- a/Admin/makebundle Fri Jan 28 11:26:08 2011 +1100 +++ b/Admin/makebundle Mon Jan 31 11:18:29 2011 +0100 @@ -69,6 +69,20 @@ tar -C "$TMP" -x -z -f "$HEAPS_ARCHIVE" +( + cd "$TMP/$ISABELLE_NAME/contrib/ProofGeneral" + find . -name "*.elc" -exec rm {} ";" +) + +case "$PLATFORM" in + x86-cygwin) + rm "$TMP/$ISABELLE_NAME/contrib/ProofGeneral" + ln -s ProofGeneral-3.7.1.1 "$TMP/$ISABELLE_NAME/contrib/ProofGeneral" + ;; + *) + ;; +esac + BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz" echo "$(basename "$BUNDLE_ARCHIVE")" diff -r 4030fcc5c785 -r b9357f56fd64 Admin/makedist diff -r 4030fcc5c785 -r b9357f56fd64 NEWS --- a/NEWS Fri Jan 28 11:26:08 2011 +1100 +++ b/NEWS Mon Jan 31 11:18:29 2011 +0100 @@ -12,10 +12,12 @@ *** General *** * Experimental Prover IDE based on Isabelle/Scala and jEdit (see -src/Tools/jEdit). A bundled component provides "isabelle jedit" as -executable Isabelle tool. Note that this also serves as IDE for -Isabelle/ML, with useful tooltips and hyperlinks produced from its -static analysis. +src/Tools/jEdit). This also serves as IDE for Isabelle/ML, with +useful tooltips and hyperlinks produced from its static analysis. The +bundled component provides an executable Isabelle tool that can be run +like this: + + Isabelle2011/bin/isabelle jedit * Significantly improved Isabelle/Isar implementation manual. diff -r 4030fcc5c785 -r b9357f56fd64 doc-src/IsarImplementation/Thy/Local_Theory.thy --- a/doc-src/IsarImplementation/Thy/Local_Theory.thy Fri Jan 28 11:26:08 2011 +1100 +++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy Mon Jan 31 11:18:29 2011 +0100 @@ -96,7 +96,8 @@ text %mlref {* \begin{mldecls} @{index_ML_type local_theory: Proof.context} \\ - @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex] + @{index_ML Named_Target.init: "(local_theory -> local_theory) -> + string -> theory -> local_theory"} \\[1ex] @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory"} \\ @{index_ML Local_Theory.note: "Attrib.binding * thm list -> @@ -113,13 +114,15 @@ with operations on expecting a regular @{text "ctxt:"}~@{ML_type Proof.context}. - \item @{ML Named_Target.init}~@{text "name thy"} initializes a local - theory derived from the given background theory. An empty name - refers to a \emph{global theory} context, and a non-empty name - refers to a @{command locale} or @{command class} context (a - fully-qualified internal name is expected here). This is useful for - experimentation --- normally the Isar toplevel already takes care to - initialize the local theory context. + \item @{ML Named_Target.init}~@{text "before_exit name thy"} + initializes a local theory derived from the given background theory. + An empty name refers to a \emph{global theory} context, and a + non-empty name refers to a @{command locale} or @{command class} + context (a fully-qualified internal name is expected here). This is + useful for experimentation --- normally the Isar toplevel already + takes care to initialize the local theory context. The given @{text + "before_exit"} function is invoked before leaving the context; in + most situations plain identity @{ML I} is sufficient. \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs)) lthy"} defines a local entity according to the specification that is diff -r 4030fcc5c785 -r b9357f56fd64 doc-src/IsarImplementation/Thy/document/Local_Theory.tex --- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Fri Jan 28 11:26:08 2011 +1100 +++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Mon Jan 31 11:18:29 2011 +0100 @@ -122,7 +122,8 @@ \begin{isamarkuptext}% \begin{mldecls} \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\ - \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string -> theory -> local_theory| \\[1ex] + \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: (local_theory -> local_theory) ->|\isasep\isanewline% +\verb| string -> theory -> local_theory| \\[1ex] \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline% \verb| local_theory -> (term * (string * thm)) * local_theory| \\ \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline% @@ -138,13 +139,14 @@ any value \isa{lthy{\isaliteral{3A}{\isacharcolon}}}~\verb|local_theory| can be also used with operations on expecting a regular \isa{ctxt{\isaliteral{3A}{\isacharcolon}}}~\verb|Proof.context|. - \item \verb|Named_Target.init|~\isa{name\ thy} initializes a local - theory derived from the given background theory. An empty name - refers to a \emph{global theory} context, and a non-empty name - refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a - fully-qualified internal name is expected here). This is useful for - experimentation --- normally the Isar toplevel already takes care to - initialize the local theory context. + \item \verb|Named_Target.init|~\isa{before{\isaliteral{5F}{\isacharunderscore}}exit\ name\ thy} + initializes a local theory derived from the given background theory. + An empty name refers to a \emph{global theory} context, and a + non-empty name refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} + context (a fully-qualified internal name is expected here). This is + useful for experimentation --- normally the Isar toplevel already + takes care to initialize the local theory context. The given \isa{before{\isaliteral{5F}{\isacharunderscore}}exit} function is invoked before leaving the context; in + most situations plain identity \verb|I| is sufficient. \item \verb|Local_Theory.define|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}b{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ lthy} defines a local entity according to the specification that is given relatively to the current \isa{lthy} context. In diff -r 4030fcc5c785 -r b9357f56fd64 doc-src/IsarRef/Thy/Misc.thy --- a/doc-src/IsarRef/Thy/Misc.thy Fri Jan 28 11:26:08 2011 +1100 +++ b/doc-src/IsarRef/Thy/Misc.thy Mon Jan 31 11:18:29 2011 +0100 @@ -16,6 +16,7 @@ @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \end{matharray} @@ -35,6 +36,8 @@ ; 'thm_deps' thmrefs ; + 'unused_thms' (('name'+) '-' ('name'*))? + ; \end{rail} These commands print certain parts of the theory and proof context. @@ -93,6 +96,13 @@ \item @{command "thm_deps"}~@{text "a\<^sub>1 \ a\<^sub>n"} visualizes dependencies of facts, using Isabelle's graph browser tool (see also \cite{isabelle-sys}). + + \item @{command "unused_thms"}~@{text "A\<^isub>1 \ A\<^isub>m - B\<^isub>1 \ B\<^isub>n"} + displays all unused theorems in theories @{text "B\<^isub>1 \ B\<^isub>n"} + or their parents, but not in @{text "A\<^isub>1 \ A\<^isub>m"} or their parents. + If @{text n} is @{text 0}, the end of the range of theories + defaults to the current theory. If no range is specified, + only the unused theorems in the current theory are displayed. \item @{command "print_facts"} prints all local facts of the current context, both named and unnamed ones. diff -r 4030fcc5c785 -r b9357f56fd64 doc-src/IsarRef/Thy/document/Misc.tex --- a/doc-src/IsarRef/Thy/document/Misc.tex Fri Jan 28 11:26:08 2011 +1100 +++ b/doc-src/IsarRef/Thy/document/Misc.tex Mon Jan 31 11:18:29 2011 +0100 @@ -36,6 +36,7 @@ \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{find\_consts}\hypertarget{command.find-consts}{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ + \indexdef{}{command}{unused\_thms}\hypertarget{command.unused-thms}{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}facts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}binds}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \end{matharray} @@ -55,6 +56,8 @@ ; 'thm_deps' thmrefs ; + 'unused_thms' (('name'+) '-' ('name'*))? + ; \end{rail} These commands print certain parts of the theory and proof context. @@ -111,6 +114,13 @@ \item \hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} visualizes dependencies of facts, using Isabelle's graph browser tool (see also \cite{isabelle-sys}). + + \item \hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m\ {\isaliteral{2D}{\isacharminus}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} + displays all unused theorems in theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} + or their parents, but not in \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m{\isaliteral{22}{\isachardoublequote}}} or their parents. + If \isa{n} is \isa{{\isadigit{0}}}, the end of the range of theories + defaults to the current theory. If no range is specified, + only the unused theorems in the current theory are displayed. \item \hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}facts}}}} prints all local facts of the current context, both named and unnamed ones. diff -r 4030fcc5c785 -r b9357f56fd64 etc/proofgeneral-settings.el --- a/etc/proofgeneral-settings.el Fri Jan 28 11:26:08 2011 +1100 +++ b/etc/proofgeneral-settings.el Mon Jan 31 11:18:29 2011 +0100 @@ -1,12 +1,13 @@ ;;; Options for Proof General +;;; +;;; Examples for sensible settings: -;; Examples for sensible settings: - +;; keep sources clean (custom-set-variables '(indent-tabs-mode nil)) -(custom-set-variables '(proof-shell-quit-timeout 45)) -;(custom-set-variables '(isar-eta-contract nil)) +;; retain vital AltGr behaviour, e.g. on non-US Mac OS X +;(custom-set-variables '(ns-alternate-modifier 'none)) -;(custom-set-faces -; '(proof-locked-face -; ((((type x) (class color) (background light)) (:background "lightsteelblue2"))))) +;; longer timeout for saving persistent session +;(custom-set-variables '(proof-shell-quit-timeout 60)) + diff -r 4030fcc5c785 -r b9357f56fd64 etc/settings --- a/etc/settings Fri Jan 28 11:26:08 2011 +1100 +++ b/etc/settings Mon Jan 31 11:18:29 2011 +0100 @@ -56,6 +56,8 @@ if [ -n "$JAVA_HOME" ]; then ISABELLE_JAVA="$JAVA_HOME/bin/java" +elif [ -x /usr/libexec/java_home ]; then + ISABELLE_JAVA="$(/usr/libexec/java_home -v 1.6)"/bin/java else ISABELLE_JAVA="java" fi diff -r 4030fcc5c785 -r b9357f56fd64 lib/Tools/java --- a/lib/Tools/java Fri Jan 28 11:26:08 2011 +1100 +++ b/lib/Tools/java Mon Jan 31 11:18:29 2011 +0100 @@ -9,8 +9,8 @@ JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" if "$JAVA_EXE" -server >/dev/null 2>/dev/null then - exec "$JAVA_EXE" -server "$@" + exec "$JAVA_EXE" -Dfile.encoding=UTF-8 -server "$@" else - exec "$JAVA_EXE" "$@" + exec "$JAVA_EXE" -Dfile.encoding=UTF-8 "$@" fi diff -r 4030fcc5c785 -r b9357f56fd64 lib/Tools/scala --- a/lib/Tools/scala Fri Jan 28 11:26:08 2011 +1100 +++ b/lib/Tools/scala Mon Jan 31 11:18:29 2011 +0100 @@ -9,4 +9,4 @@ [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } CLASSPATH="$(jvmpath "$CLASSPATH")" -exec "$SCALA_HOME/bin/scala" "$@" +exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 "$@" diff -r 4030fcc5c785 -r b9357f56fd64 lib/scripts/feeder.pl --- a/lib/scripts/feeder.pl Fri Jan 28 11:26:08 2011 +1100 +++ b/lib/scripts/feeder.pl Mon Jan 31 11:18:29 2011 +0100 @@ -25,7 +25,7 @@ $emitpid && (print $$, "\n"); if ($head) { - utf8::encode($head); + utf8::upgrade($head); $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g; print $head, "\n"; } diff -r 4030fcc5c785 -r b9357f56fd64 lib/scripts/getsettings --- a/lib/scripts/getsettings Fri Jan 28 11:26:08 2011 +1100 +++ b/lib/scripts/getsettings Mon Jan 31 11:18:29 2011 +0100 @@ -56,13 +56,38 @@ #JVM path wrapper if [ "$OSTYPE" = cygwin ]; then CLASSPATH="$(cygpath -u -p "$CLASSPATH")" - function jvmpath() { cygpath -w -p "$@"; } + function jvmpath() { cygpath -C UTF8 -w -p "$@"; } THIS_CYGWIN="$(jvmpath "/")" else function jvmpath() { echo "$@"; } fi HOME_JVM="$HOME" +#shared library convenience +function librarypath () { + for X in "$@" + do + case "$ISABELLE_PLATFORM" in + *-darwin) + if [ -z "$DYLD_LIBRARY_PATH" ]; then + DYLD_LIBRARY_PATH="$X" + else + DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH" + fi + export DYLD_LIBRARY_PATH + ;; + *) + if [ -z "$LD_LIBRARY_PATH" ]; then + LD_LIBRARY_PATH="$X" + else + LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH" + fi + export LD_LIBRARY_PATH + ;; + esac + done +} + #CLASSPATH convenience function classpath () { for X in "$@" @@ -70,7 +95,7 @@ if [ -z "$CLASSPATH" ]; then CLASSPATH="$X" else - CLASSPATH="$CLASSPATH:$X" + CLASSPATH="$X:$CLASSPATH" fi done export CLASSPATH diff -r 4030fcc5c785 -r b9357f56fd64 lib/scripts/run-polyml --- a/lib/scripts/run-polyml Fri Jan 28 11:26:08 2011 +1100 +++ b/lib/scripts/run-polyml Mon Jan 31 11:18:29 2011 +0100 @@ -39,8 +39,7 @@ POLYLIB="$ML_HOME" fi -export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH" -export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH" +librarypath "$POLYLIB" ## prepare databases diff -r 4030fcc5c785 -r b9357f56fd64 src/HOL/Boogie/Tools/boogie_vcs.ML --- a/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Jan 28 11:26:08 2011 +1100 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Mon Jan 31 11:18:29 2011 +0100 @@ -276,9 +276,9 @@ structure VCs_Data = Theory_Data ( type T = vcs_data - val empty = make_vcs_data (NONE, K I, []) + val empty : T = make_vcs_data (NONE, K I, []) val extend = I - fun merge ({vcs=vcs1, filters=fs1, ...}, {vcs=vcs2, filters=fs2, ...}) = + fun merge ({vcs=vcs1, filters=fs1, ...} : T, {vcs=vcs2, filters=fs2, ...} : T) = (case (vcs1, vcs2) of (NONE, NONE) => make_vcs_data (NONE, K I, Ord_List.merge serial_ord (fs1, fs2)) diff -r 4030fcc5c785 -r b9357f56fd64 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Jan 28 11:26:08 2011 +1100 +++ b/src/HOL/HOL.thy Mon Jan 31 11:18:29 2011 +0100 @@ -1958,7 +1958,7 @@ subsubsection {* Evaluation and normalization by evaluation *} setup {* - Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of) + Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of) (* FIXME proper context!? *) *} ML {* diff -r 4030fcc5c785 -r b9357f56fd64 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy --- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Fri Jan 28 11:26:08 2011 +1100 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Mon Jan 31 11:18:29 2011 +0100 @@ -282,11 +282,11 @@ uint_word_of_int_id[OF `0 <= cd` `cd <= ?M`] uint_word_of_int_id[OF `0 <= ce` `ce <= ?M`]) let ?rotate_arg_l = - "((((ca + f 0 cb cc cd) smod 4294967296 + - x (r_l 0)) smod 4294967296 + k_l 0) smod 4294967296)" + "((((ca + f 0 cb cc cd) mod 4294967296 + + x (r_l 0)) mod 4294967296 + k_l 0) mod 4294967296)" let ?rotate_arg_r = - "((((ca + f 79 cb cc cd) smod 4294967296 + - x (r_r 0)) smod 4294967296 + k_r 0) smod 4294967296)" + "((((ca + f 79 cb cc cd) mod 4294967296 + + x (r_r 0)) mod 4294967296 + k_r 0) mod 4294967296)" note returns = `wordops__rotate (s_l 0) ?rotate_arg_l = rotate_left (s_l 0) ?rotate_arg_l` @@ -330,20 +330,20 @@ from this[OF x_lower x_upper x_lower' x_upper' `0 <= 0` `0 <= 79`] `0 \ ca` `0 \ ce` x_lower x_lower' show ?thesis unfolding returns(1) returns(2) unfolding returns - by (simp add: smod_pos_pos) + by simp qed spark_vc procedure_round_62 proof - let ?M = "4294967295::int" let ?rotate_arg_l = - "((((cla + f (loop__1__j + 1) clb clc cld) smod 4294967296 + - x (r_l (loop__1__j + 1))) smod 4294967296 + - k_l (loop__1__j + 1)) smod 4294967296)" + "((((cla + f (loop__1__j + 1) clb clc cld) mod 4294967296 + + x (r_l (loop__1__j + 1))) mod 4294967296 + + k_l (loop__1__j + 1)) mod 4294967296)" let ?rotate_arg_r = - "((((cra + f (79 - (loop__1__j + 1)) crb crc crd) smod - 4294967296 + x (r_r (loop__1__j + 1))) smod 4294967296 + - k_r (loop__1__j + 1)) smod 4294967296)" + "((((cra + f (79 - (loop__1__j + 1)) crb crc crd) mod + 4294967296 + x (r_r (loop__1__j + 1))) mod 4294967296 + + k_r (loop__1__j + 1)) mod 4294967296)" have s: "78 - loop__1__j = (79 - (loop__1__j + 1))" by simp note returns = @@ -415,7 +415,7 @@ `0 \ cla` `0 \ cle` `0 \ cra` `0 \ cre` x_lower x_lower' show ?thesis unfolding `loop__1__j + 1 + 1 = loop__1__j + 2` unfolding returns(1) returns(2) unfolding returns - by (simp add: smod_pos_pos) + by simp qed spark_vc procedure_round_76 @@ -456,7 +456,7 @@ unfolding round_def unfolding steps_to_steps' unfolding H1[symmetric] - by (simp add: uint_word_ariths(2) rdmods smod_pos_pos + by (simp add: uint_word_ariths(2) rdmods uint_word_of_int_id) qed diff -r 4030fcc5c785 -r b9357f56fd64 src/HOL/SPARK/SPARK_Setup.thy --- a/src/HOL/SPARK/SPARK_Setup.thy Fri Jan 28 11:26:08 2011 +1100 +++ b/src/HOL/SPARK/SPARK_Setup.thy Mon Jan 31 11:18:29 2011 +0100 @@ -15,60 +15,33 @@ begin text {* -SPARK versions of div and mod, see section 4.4.1.1 of SPARK Proof Manual +SPARK version of div, see section 4.4.1.1 of SPARK Proof Manual *} definition sdiv :: "int \ int \ int" (infixl "sdiv" 70) where - "a sdiv b = - (if 0 \ a then - if 0 \ b then a div b - else - (a div - b) - else - if 0 \ b then - (- a div b) - else - a div - b)" - -definition smod :: "int \ int \ int" (infixl "smod" 70) where - "a smod b = a - ((a sdiv b) * b)" + "a sdiv b = sgn a * sgn b * (\a\ div \b\)" lemma sdiv_minus_dividend: "- a sdiv b = - (a sdiv b)" - by (simp add: sdiv_def) + by (simp add: sdiv_def sgn_if) lemma sdiv_minus_divisor: "a sdiv - b = - (a sdiv b)" - by (simp add: sdiv_def) - -lemma smod_minus_dividend: "- a smod b = - (a smod b)" - by (simp add: smod_def sdiv_minus_dividend) - -lemma smod_minus_divisor: "a smod - b = a smod b" - by (simp add: smod_def sdiv_minus_divisor) + by (simp add: sdiv_def sgn_if) text {* -Correspondence between HOL's and SPARK's versions of div and mod +Correspondence between HOL's and SPARK's version of div *} lemma sdiv_pos_pos: "0 \ a \ 0 \ b \ a sdiv b = a div b" - by (simp add: sdiv_def) + by (simp add: sdiv_def sgn_if) lemma sdiv_pos_neg: "0 \ a \ b < 0 \ a sdiv b = - (a div - b)" - by (simp add: sdiv_def) + by (simp add: sdiv_def sgn_if) lemma sdiv_neg_pos: "a < 0 \ 0 \ b \ a sdiv b = - (- a div b)" - by (simp add: sdiv_def) + by (simp add: sdiv_def sgn_if) lemma sdiv_neg_neg: "a < 0 \ b < 0 \ a sdiv b = - a div - b" - by (simp add: sdiv_def) - -lemma smod_pos_pos: "0 \ a \ 0 \ b \ a smod b = a mod b" - by (simp add: smod_def sdiv_pos_pos zmod_zdiv_equality') - -lemma smod_pos_neg: "0 \ a \ b < 0 \ a smod b = a mod - b" - by (simp add: smod_def sdiv_pos_neg zmod_zdiv_equality') - -lemma smod_neg_pos: "a < 0 \ 0 \ b \ a smod b = - (- a mod b)" - by (simp add: smod_def sdiv_neg_pos zmod_zdiv_equality') - -lemma smod_neg_neg: "a < 0 \ b < 0 \ a smod b = - (- a mod - b)" - by (simp add: smod_def sdiv_neg_neg zmod_zdiv_equality') + by (simp add: sdiv_def sgn_if) text {* diff -r 4030fcc5c785 -r b9357f56fd64 src/HOL/SPARK/Tools/fdl_parser.ML --- a/src/HOL/SPARK/Tools/fdl_parser.ML Fri Jan 28 11:26:08 2011 +1100 +++ b/src/HOL/SPARK/Tools/fdl_parser.ML Mon Jan 31 11:18:29 2011 +0100 @@ -302,7 +302,7 @@ funs = update decl funs} handle Symtab.DUP s => error ("Duplicate function " ^ s); -val type_decl = $$$ "type" |-- !!! (identifier --| $$$ "=" -- +fun type_decl x = ($$$ "type" |-- !!! (identifier --| $$$ "=" -- ( identifier >> Basic_Type || $$$ "(" |-- !!! (list1 identifier --| $$$ ")") >> Enum_Type || $$$ "array" |-- !!! ($$$ "[" |-- list1 identifier --| $$$ "]" --| @@ -310,23 +310,23 @@ || $$$ "record" |-- !!! (enum1 ";" (list1 identifier -- !!! ($$$ ":" |-- identifier)) --| $$$ "end") >> Record_Type - || $$$ "pending" >> K Pending_Type)) >> add_type_decl; + || $$$ "pending" >> K Pending_Type)) >> add_type_decl) x; -val const_decl = $$$ "const" |-- !!! (identifier --| $$$ ":" -- identifier --| - $$$ "=" --| $$$ "pending") >> add_const_decl; +fun const_decl x = ($$$ "const" |-- !!! (identifier --| $$$ ":" -- identifier --| + $$$ "=" --| $$$ "pending") >> add_const_decl) x; -val var_decl = $$$ "var" |-- !!! (list1 identifier --| $$$ ":" -- identifier) >> - add_var_decl; +fun var_decl x = ($$$ "var" |-- !!! (list1 identifier --| $$$ ":" -- identifier) >> + add_var_decl) x; -val fun_decl = $$$ "function" |-- !!! (identifier -- +fun fun_decl x = ($$$ "function" |-- !!! (identifier -- (Scan.optional ($$$ "(" |-- !!! (list1 identifier --| $$$ ")")) [] --| - $$$ ":" -- identifier)) >> add_fun_decl; + $$$ ":" -- identifier)) >> add_fun_decl) x; -val declarations = - $$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" -- +fun declarations x = + ($$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" -- (Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --| !!! ($$$ ";")) >> (fn ds => apply ds empty_decls)) --| - $$$ "end" --| $$$ ";" + $$$ "end" --| $$$ ";") x; fun parse_declarations pos s = s |> diff -r 4030fcc5c785 -r b9357f56fd64 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Fri Jan 28 11:26:08 2011 +1100 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Jan 31 11:18:29 2011 +0100 @@ -287,7 +287,7 @@ | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv} (fst (tm_of vs e), fst (tm_of vs e')), integerN) - | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name smod} + | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name mod} (fst (tm_of vs e), fst (tm_of vs e')), integerN) | tm_of vs (Funct ("-", [e])) = diff -r 4030fcc5c785 -r b9357f56fd64 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Fri Jan 28 11:26:08 2011 +1100 +++ b/src/HOL/Tools/inductive_codegen.ML Mon Jan 31 11:18:29 2011 +0100 @@ -7,7 +7,7 @@ signature INDUCTIVE_CODEGEN = sig val add : string option -> int option -> attribute - val test_fn : (int * int * int -> term list option) Unsynchronized.ref + val test_fn : (int * int * int -> term list option) Unsynchronized.ref (* FIXME *) val test_term: Proof.context -> term -> int -> term list option * Quickcheck.report option val setup : theory -> theory @@ -845,12 +845,12 @@ Pretty.brk 1, Codegen.str "| NONE => NONE);"]) ^ "\n\nend;\n"; - val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s; + val test_fn' = NAMED_CRITICAL "codegen" (fn () => + (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! test_fn)); val values = Config.get ctxt random_values; val bound = Config.get ctxt depth_bound; val start = Config.get ctxt depth_start; val offset = Config.get ctxt size_offset; - val test_fn' = !test_fn; fun test k = (deepen bound (fn i => (Output.urgent_message ("Search depth: " ^ string_of_int i); test_fn' (i, values, k+offset))) start, NONE); diff -r 4030fcc5c785 -r b9357f56fd64 src/HOL/Tools/list_to_set_comprehension.ML --- a/src/HOL/Tools/list_to_set_comprehension.ML Fri Jan 28 11:26:08 2011 +1100 +++ b/src/HOL/Tools/list_to_set_comprehension.ML Mon Jan 31 11:18:29 2011 +0100 @@ -47,6 +47,11 @@ Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct | _ => raise CTERM ("conj_conv", [ct])); +fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th) + +fun conjunct_assoc_conv ct = Conv.try_conv + ((rewr_conv' @{thm conj_assoc}) then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct + fun right_hand_set_comprehension_conv conv ctxt = Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (all_exists_conv conv o #2) ctxt)) @@ -54,8 +59,6 @@ datatype termlets = If | Case of (typ * int) -fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th) - fun simproc ss redex = let val ctxt = Simplifier.the_context ss @@ -136,7 +139,7 @@ (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info))))) Conv.all_conv) then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) - then_conv (Conv.try_conv (rewr_conv' @{thm conj_assoc})))) context + then_conv conjunct_assoc_conv)) context then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => Conv.repeat_conv (all_but_last_exists_conv (K (rewr_conv' @{thm simp_thms(39)})) ctxt)) context)))) 1) ctxt 1 THEN tac ctxt cont @@ -172,7 +175,7 @@ if eqs = [] then NONE (* no rewriting, nothing to be done *) else let - val Type (@{type_name List.list}, [rT]) = fastype_of t + val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t) val pat_eq = case try dest_singleton_list t of SOME t' => Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) diff -r 4030fcc5c785 -r b9357f56fd64 src/Pure/ML-Systems/proper_int.ML --- a/src/Pure/ML-Systems/proper_int.ML Fri Jan 28 11:26:08 2011 +1100 +++ b/src/Pure/ML-Systems/proper_int.ML Mon Jan 31 11:18:29 2011 +0100 @@ -141,7 +141,7 @@ structure StringCvt = struct open StringCvt; - datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option + datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option; fun realfmt fmt = Real.fmt (case fmt of EXACT => StringCvt.EXACT @@ -160,36 +160,36 @@ struct open Word; val wordSize = mk_int Word.wordSize; - val toInt = mk_int o Word.toInt; - val toIntX = mk_int o Word.toIntX; - val fromInt = Word.fromInt o dest_int; + val toInt = Word.toLargeInt; + val toIntX = Word.toLargeIntX; + val fromInt = Word.fromLargeInt; end; structure Word8 = struct open Word8; val wordSize = mk_int Word8.wordSize; - val toInt = mk_int o Word8.toInt; - val toIntX = mk_int o Word8.toIntX; - val fromInt = Word8.fromInt o dest_int; + val toInt = Word8.toLargeInt; + val toIntX = Word8.toLargeIntX; + val fromInt = Word8.fromLargeInt; end; structure Word32 = struct open Word32; val wordSize = mk_int Word32.wordSize; - val toInt = mk_int o Word32.toInt; - val toIntX = mk_int o Word32.toIntX; - val fromInt = Word32.fromInt o dest_int; + val toInt = Word32.toLargeInt; + val toIntX = Word32.toLargeIntX; + val fromInt = Word32.fromLargeInt; end; structure LargeWord = struct open LargeWord; val wordSize = mk_int LargeWord.wordSize; - val toInt = mk_int o LargeWord.toInt; - val toIntX = mk_int o LargeWord.toIntX; - val fromInt = LargeWord.fromInt o dest_int; + val toInt = LargeWord.toLargeInt; + val toIntX = LargeWord.toLargeIntX; + val fromInt = LargeWord.fromLargeInt; end; diff -r 4030fcc5c785 -r b9357f56fd64 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Jan 28 11:26:08 2011 +1100 +++ b/src/Pure/PIDE/document.ML Mon Jan 31 11:18:29 2011 +0100 @@ -18,6 +18,7 @@ type edit = string * ((command_id option * command_id option) list) option type state val init_state: state + val cancel: state -> unit val define_command: command_id -> string -> state -> state val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state val execute: version_id -> state -> state @@ -181,6 +182,15 @@ NONE => err_undef "command execution" id | SOME exec => exec); + +(* document execution *) + +fun cancel (State {execution, ...}) = + List.app Future.cancel execution; + +fun await_cancellation (State {execution, ...}) = + ignore (Future.join_results execution); + end; @@ -284,6 +294,7 @@ fun edit (old_id: version_id) (new_id: version_id) edits state = let val old_version = the_version state old_id; + val _ = Time.now (); (* FIXME odd workaround *) val new_version = fold edit_nodes edits old_version; fun update_node name (rev_updates, version, st) = @@ -323,17 +334,19 @@ fun force_exec NONE = () | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id)); - val _ = List.app Future.cancel execution; - fun await_cancellation () = Future.join_results execution; + val _ = cancel state; val execution' = (* FIXME proper node deps *) - node_names_of version |> map (fn name => - Future.fork_pri 1 (fn () => - (await_cancellation (); - fold_entries NONE (fn (_, exec) => fn () => force_exec exec) - (get_node version name) ()))); + [Future.fork_pri 1 (fn () => + let + val _ = await_cancellation state; + val _ = + node_names_of version |> List.app (fn name => + fold_entries NONE (fn (_, exec) => fn () => force_exec exec) + (get_node version name) ()); + in () end)]; - val _ = await_cancellation (); + val _ = await_cancellation state; (* FIXME async!? *) in (versions, commands, execs, execution') end); diff -r 4030fcc5c785 -r b9357f56fd64 src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Fri Jan 28 11:26:08 2011 +1100 +++ b/src/Pure/PIDE/isar_document.ML Mon Jan 31 11:18:29 2011 +0100 @@ -30,6 +30,7 @@ (XML_Data.dest_option XML_Data.dest_int) (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml); + val _ = Document.cancel state; val (updates, state') = Document.edit old_id new_id edits state; val _ = implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates) diff -r 4030fcc5c785 -r b9357f56fd64 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Fri Jan 28 11:26:08 2011 +1100 +++ b/src/Pure/codegen.ML Mon Jan 31 11:18:29 2011 +0100 @@ -75,9 +75,9 @@ val mk_type: bool -> typ -> Pretty.T val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T - val test_fn: (int -> term list option) Unsynchronized.ref + val test_fn: (int -> term list option) Unsynchronized.ref (* FIXME *) val test_term: Proof.context -> term -> int -> term list option - val eval_result: (unit -> term) Unsynchronized.ref + val eval_result: (unit -> term) Unsynchronized.ref (* FIXME *) val eval_term: theory -> term -> term val evaluation_conv: cterm -> thm val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list @@ -894,8 +894,9 @@ Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]), str ");"]) ^ "\n\nend;\n"; - val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s; - in (fn size => (! test_fn size)) end; + val test_fn' = NAMED_CRITICAL "codegen" (fn () => + (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! test_fn)); + in test_fn' end; @@ -905,7 +906,7 @@ fun eval_term thy t = let - val ctxt = ProofContext.init_global thy; + val ctxt = ProofContext.init_global thy; (* FIXME *) val e = let val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse @@ -924,9 +925,10 @@ [str "(result ())"], str ");"]) ^ "\n\nend;\n"; - val _ = NAMED_CRITICAL "codegen" (fn () => (* FIXME ??? *) - ML_Context.eval_text_in (SOME ctxt) false Position.none s); - in !eval_result end; + in + NAMED_CRITICAL "codegen" (fn () => + (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! eval_result)) + end in e () end; val (_, evaluation_conv) = Context.>>> (Context.map_theory_result diff -r 4030fcc5c785 -r b9357f56fd64 src/Tools/jEdit/dist-template/README.html --- a/src/Tools/jEdit/dist-template/README.html Fri Jan 28 11:26:08 2011 +1100 +++ b/src/Tools/jEdit/dist-template/README.html Mon Jan 31 11:18:29 2011 +0100 @@ -1,4 +1,4 @@ - + @@ -9,7 +9,7 @@ -

Notes on the Isabelle/jEdit Prover IDE

+

The Isabelle/jEdit Prover IDE

    @@ -34,6 +34,70 @@
+ +

Isabelle symbols and fonts

+ +
    + +
  • Isabelle supports infinitely many symbols:
    + α, β, γ, …
    + ∀, ∃, ∨, ∧, ⟶, ⟷, …
    + ≤, ≥, ⊓, ⊔, …
    + ℵ, △, ∇, …
    + \<foo>, \<bar>, \<baz>, …
    +
    • + +
  • A default mapping relates some Isabelle symbols to Unicode points + (see $ISABELLE_HOME/etc/symbols and $ISABELLE_HOME_USER/etc/symbols). +
    • + +
  • The IsabelleText font ensures that Unicode points are actually + seen on the screen (or printer). +
    • + +
  • Input methods: +
      +
    • copy/paste from decoded source files
      • +
    • copy/paste from prover output
      • +
    • completion provided by Isabelle plugin, e.g.
      + + + + + + + + + + + + + + + + + + + + +
      name abbreviation symbol
      lambda λ
      Rightarrow => ⇒
      Longrightarrow ==> ⟹
      And !! ⋀
      equiv == ≡
      forall ! ∀
      exists ? ∃
      longrightarrow --> ⟶
      and /\ ∧
      or \/ ∨
      not ~ ¬
      noteq ~= ≠
      in : ∈
      notin ~: ∉
      +
      • +
    +
    • + +
  • NOTE: The above abbreviations refer to the input method. + The logical notation provides ASCII alternatives that often + coincide, but deviate occasionally. +
    • + +
  • NOTE: Generic jEdit abbreviations or plugins perform similar + source replacement operations; this works for Isabelle as long + as the Unicode sequences coincide with the symbol mapping. +
    • + +
+ +

Limitations and workrounds (January 2011)

    diff -r 4030fcc5c785 -r b9357f56fd64 src/Tools/jEdit/dist-template/properties/jedit.props --- a/src/Tools/jEdit/dist-template/properties/jedit.props Fri Jan 28 11:26:08 2011 +1100 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Mon Jan 31 11:18:29 2011 +0100 @@ -178,9 +178,9 @@ insert-newline-indent.shortcut= insert-newline.shortcut=ENTER isabelle-output.dock-position=bottom -isabelle-session.dock-position=bottom isabelle-output.height=174 isabelle-output.width=412 +isabelle-session.dock-position=bottom line-end.shortcut=END line-home.shortcut=HOME lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel @@ -188,6 +188,8 @@ mode.isabelle.folding=sidekick mode.isabelle.sidekick.showStatusWindow.label=true print.font=IsabelleText +restore.remote=false +restore=false sidekick-tree.dock-position=right sidekick.buffer-save-parse=true sidekick.complete-delay=300 @@ -207,4 +209,5 @@ view.height=787 view.middleMousePaste=true view.showToolbar=false +view.thickCaret=true view.width=1072