--- 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
--- 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/
--- 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
--- 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=$?
--- /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
--- /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
+
+
--- /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 ..."
--- /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)
--- /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.
--- /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")
+
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+ ;;
--- /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))
+>
+> ;;
--- /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[@]}"
+
--- 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
--- 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
-
-
--- 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 ..."
--- 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)
--- 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.
--- 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")
-
- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
- ;;
--- 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 \
--- 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
--- 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
--- 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")"
--- 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.
--- 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
--- 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
--- 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 \<rightarrow>"} \\
@{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\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 \<dots> 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 \<dots> A\<^isub>m - B\<^isub>1 \<dots> B\<^isub>n"}
+ displays all unused theorems in theories @{text "B\<^isub>1 \<dots> B\<^isub>n"}
+ or their parents, but not in @{text "A\<^isub>1 \<dots> 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.
--- 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.
--- 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))
+
--- 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
--- 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
--- 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 "$@"
--- 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";
}
--- 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
--- 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
--- 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))
--- 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 {*
--- 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 \<le> ca` `0 \<le> 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 \<le> cla` `0 \<le> cle` `0 \<le> cra` `0 \<le> 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
--- 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 \<Rightarrow> int \<Rightarrow> int" (infixl "sdiv" 70) where
- "a sdiv b =
- (if 0 \<le> a then
- if 0 \<le> b then a div b
- else - (a div - b)
- else
- if 0 \<le> b then - (- a div b)
- else - a div - b)"
-
-definition smod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "smod" 70) where
- "a smod b = a - ((a sdiv b) * b)"
+ "a sdiv b = sgn a * sgn b * (\<bar>a\<bar> div \<bar>b\<bar>)"
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 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a sdiv b = a div b"
- by (simp add: sdiv_def)
+ by (simp add: sdiv_def sgn_if)
lemma sdiv_pos_neg: "0 \<le> a \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - (a div - b)"
- by (simp add: sdiv_def)
+ by (simp add: sdiv_def sgn_if)
lemma sdiv_neg_pos: "a < 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a sdiv b = - (- a div b)"
- by (simp add: sdiv_def)
+ by (simp add: sdiv_def sgn_if)
lemma sdiv_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - a div - b"
- by (simp add: sdiv_def)
-
-lemma smod_pos_pos: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a smod b = a mod b"
- by (simp add: smod_def sdiv_pos_pos zmod_zdiv_equality')
-
-lemma smod_pos_neg: "0 \<le> a \<Longrightarrow> b < 0 \<Longrightarrow> a smod b = a mod - b"
- by (simp add: smod_def sdiv_pos_neg zmod_zdiv_equality')
-
-lemma smod_neg_pos: "a < 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a smod b = - (- a mod b)"
- by (simp add: smod_def sdiv_neg_pos zmod_zdiv_equality')
-
-lemma smod_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 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 {*
--- 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 |>
--- 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])) =
--- 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);
--- 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})
--- 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;
--- 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);
--- 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)
--- 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
--- 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 @@
-<?xml version="1.0" encoding="ISO-8859-1" ?>
+<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
@@ -9,7 +9,7 @@
<body>
-<h2>Notes on the Isabelle/jEdit Prover IDE</h2>
+<h2>The Isabelle/jEdit Prover IDE</h2>
<ul>
@@ -34,6 +34,70 @@
</ul>
+
+<h2>Isabelle symbols and fonts</h2>
+
+<ul>
+
+ <li>Isabelle supports infinitely many symbols:<br/>
+ α, β, γ, …<br/>
+ ∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
+ ≤, ≥, ⊓, ⊔, …<br/>
+ ℵ, △, ∇, …<br/>
+ <tt>\<foo></tt>, <tt>\<bar></tt>, <tt>\<baz></tt>, …<br/>
+ </li>
+
+ <li>A default mapping relates some Isabelle symbols to Unicode points
+ (see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>).
+ </li>
+
+ <li>The <em>IsabelleText</em> font ensures that Unicode points are actually
+ seen on the screen (or printer).
+ </li>
+
+ <li>Input methods:
+ <ul>
+ <li>copy/paste from decoded source files</li>
+ <li>copy/paste from prover output</li>
+ <li>completion provided by Isabelle plugin, e.g.<br/>
+
+ <table border="1">
+ <tr><th><b>name</b></th> <th><b>abbreviation</b></th> <th><b>symbol</b></th></tr>
+
+ <tr><td>lambda</td> <td></td> <td>λ</td></tr>
+ <tr><td>Rightarrow</td> <td><tt>=></tt></td> <td>⇒</td></tr>
+ <tr><td>Longrightarrow</td> <td><tt>==></tt></td> <td>⟹</td></tr>
+
+ <tr><td>And</td> <td><tt>!!</tt></td> <td>⋀</td></tr>
+ <tr><td>equiv</td> <td><tt>==</tt></td> <td>≡</td></tr>
+
+ <tr><td>forall</td> <td><tt>!</tt></td> <td>∀</td></tr>
+ <tr><td>exists</td> <td><tt>?</tt></td> <td>∃</td></tr>
+ <tr><td>longrightarrow</td> <td><tt>--></tt></td> <td>⟶</td></tr>
+ <tr><td>and</td> <td><tt>/\</tt></td> <td>∧</td></tr>
+ <tr><td>or</td> <td><tt>\/</tt></td> <td>∨</td></tr>
+ <tr><td>not</td> <td><tt>~ </tt></td> <td>¬</td></tr>
+ <tr><td>noteq</td> <td><tt>~=</tt></td> <td>≠</td></tr>
+ <tr><td>in</td> <td><tt>:</tt></td> <td>∈</td></tr>
+ <tr><td>notin</td> <td><tt>~:</tt></td> <td>∉</td></tr>
+ </table>
+ </li>
+ </ul>
+ </li>
+
+ <li><b>NOTE:</b> The above abbreviations refer to the input method.
+ The logical notation provides ASCII alternatives that often
+ coincide, but deviate occasionally.
+ </li>
+
+ <li><b>NOTE:</b> 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.
+ </li>
+
+</ul>
+
+
<h2>Limitations and workrounds (January 2011)</h2>
<ul>
--- 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