1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/Admin/ProofGeneral/3.7.1.1/interface Thu Jan 27 20:46:20 2011 +0100
1.3 @@ -0,0 +1,262 @@
1.4 +#!/usr/bin/env bash
1.5 +#
1.6 +# interface,v 9.1 2008/02/06 15:40:45 makarius Exp
1.7 +#
1.8 +# Proof General interface wrapper for Isabelle.
1.9 +
1.10 +
1.11 +## self references
1.12 +
1.13 +THIS="$(cd "$(dirname "$0")"; pwd)"
1.14 +SUPER="$(cd "$THIS/.."; pwd)"
1.15 +
1.16 +
1.17 +## diagnostics
1.18 +
1.19 +usage()
1.20 +{
1.21 + echo
1.22 + echo "Usage: Isabelle [OPTIONS] [FILES ...]"
1.23 + echo
1.24 + echo " Options are:"
1.25 + echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)"
1.26 + echo " -L NAME abbreviates -l NAME -k NAME"
1.27 + echo " -P BOOL actually start Proof General (default true), otherwise"
1.28 + echo " run plain tty session"
1.29 + echo " -U BOOL enable Unicode (UTF-8) communication (default true)"
1.30 + echo " -X BOOL configure the X-Symbol package on startup (default true)"
1.31 + echo " -f SIZE set X-Symbol font size (default 12)"
1.32 + echo " -g GEOMETRY specify Emacs geometry"
1.33 + echo " -k NAME use specific isar-keywords for named logic"
1.34 + echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
1.35 + echo " -m MODE add print mode for output"
1.36 + echo " -p NAME Emacs program name (default emacs)"
1.37 + echo " -u BOOL use personal .emacs file (default true)"
1.38 + echo " -w BOOL use window system (default true)"
1.39 + echo " -x BOOL enable the X-Symbol package on startup (default false)"
1.40 + echo
1.41 + echo "Starts Proof General for Isabelle with theory and proof FILES"
1.42 + echo "(default Scratch.thy)."
1.43 + echo
1.44 + echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS"
1.45 + echo
1.46 + exit 1
1.47 +}
1.48 +
1.49 +fail()
1.50 +{
1.51 + echo "$1" >&2
1.52 + exit 2
1.53 +}
1.54 +
1.55 +
1.56 +## process command line
1.57 +
1.58 +# options
1.59 +
1.60 +ISABELLE_OPTIONS=""
1.61 +ISAR="true"
1.62 +START_PG="true"
1.63 +GEOMETRY=""
1.64 +KEYWORDS=""
1.65 +LOGIC="$ISABELLE_LOGIC"
1.66 +PROGNAME="emacs"
1.67 +INITFILE="true"
1.68 +WINDOWSYSTEM="true"
1.69 +XSYMBOL=""
1.70 +XSYMBOL_SETUP=true
1.71 +XSYMBOL_FONTSIZE="12"
1.72 +UNICODE=""
1.73 +
1.74 +getoptions()
1.75 +{
1.76 + OPTIND=1
1.77 + while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT
1.78 + do
1.79 + case "$OPT" in
1.80 + I)
1.81 + ISAR="$OPTARG"
1.82 + ;;
1.83 + L)
1.84 + KEYWORDS="$OPTARG"
1.85 + LOGIC="$OPTARG"
1.86 + ;;
1.87 + P)
1.88 + START_PG="$OPTARG"
1.89 + ;;
1.90 + U)
1.91 + UNICODE="$OPTARG"
1.92 + ;;
1.93 + X)
1.94 + XSYMBOL_SETUP="$OPTARG"
1.95 + ;;
1.96 + f)
1.97 + XSYMBOL_FONTSIZE="$OPTARG"
1.98 + ;;
1.99 + g)
1.100 + GEOMETRY="$OPTARG"
1.101 + ;;
1.102 + k)
1.103 + KEYWORDS="$OPTARG"
1.104 + ;;
1.105 + l)
1.106 + LOGIC="$OPTARG"
1.107 + ;;
1.108 + m)
1.109 + if [ -z "$ISABELLE_OPTIONS" ]; then
1.110 + ISABELLE_OPTIONS="-m $OPTARG"
1.111 + else
1.112 + ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
1.113 + fi
1.114 + ;;
1.115 + p)
1.116 + PROGNAME="$OPTARG"
1.117 + ;;
1.118 + u)
1.119 + INITFILE="$OPTARG"
1.120 + ;;
1.121 + w)
1.122 + WINDOWSYSTEM="$OPTARG"
1.123 + ;;
1.124 + x)
1.125 + XSYMBOL="$OPTARG"
1.126 + ;;
1.127 + \?)
1.128 + usage
1.129 + ;;
1.130 + esac
1.131 + done
1.132 +}
1.133 +
1.134 +eval "OPTIONS=($PROOFGENERAL_OPTIONS)"
1.135 +getoptions "${OPTIONS[@]}"
1.136 +
1.137 +getoptions "$@"
1.138 +shift $(($OPTIND - 1))
1.139 +
1.140 +
1.141 +# args
1.142 +
1.143 +declare -a FILES=()
1.144 +
1.145 +if [ "$#" -eq 0 ]; then
1.146 + FILES["${#FILES[@]}"]="Scratch.thy"
1.147 +else
1.148 + while [ "$#" -gt 0 ]; do
1.149 + FILES["${#FILES[@]}"]="$1"
1.150 + shift
1.151 + done
1.152 +fi
1.153 +
1.154 +
1.155 +## smart X11 font installation
1.156 +
1.157 +function checkfonts ()
1.158 +{
1.159 + XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1
1.160 +
1.161 + case "$XLSFONTS" in
1.162 + xlsfonts:*)
1.163 + return 1
1.164 + ;;
1.165 + esac
1.166 +
1.167 + return 0
1.168 +}
1.169 +
1.170 +function installfonts ()
1.171 +{
1.172 + checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
1.173 +}
1.174 +
1.175 +
1.176 +## main
1.177 +
1.178 +# Isabelle2008 compatibility
1.179 +[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE"
1.180 +[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL"
1.181 +
1.182 +if [ "$START_PG" = false ]; then
1.183 +
1.184 + [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
1.185 + exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
1.186 +
1.187 +else
1.188 +
1.189 + declare -a ARGS=()
1.190 +
1.191 + if [ -n "$GEOMETRY" ]; then
1.192 + ARGS["${#ARGS[@]}"]="-geometry"
1.193 + ARGS["${#ARGS[@]}"]="$GEOMETRY"
1.194 + fi
1.195 +
1.196 + [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q"
1.197 +
1.198 + if [ "$WINDOWSYSTEM" = false ]; then
1.199 + ARGS["${#ARGS[@]}"]="-nw"
1.200 + XSYMBOL=false
1.201 + elif [ -z "$DISPLAY" ]; then
1.202 + XSYMBOL=false
1.203 + else
1.204 + [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts
1.205 + fi
1.206 +
1.207 + if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ]
1.208 + then
1.209 + if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ]
1.210 + then
1.211 + cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/"
1.212 + cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/"
1.213 + sleep 3
1.214 + fi
1.215 + fi
1.216 +
1.217 + ARGS["${#ARGS[@]}"]="-l"
1.218 + ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el"
1.219 +
1.220 + if [ -n "$KEYWORDS" ]; then
1.221 + if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
1.222 + ARGS["${#ARGS[@]}"]="-l"
1.223 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el"
1.224 + elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
1.225 + ARGS["${#ARGS[@]}"]="-l"
1.226 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el"
1.227 + else
1.228 + fail "No isar-keywords file for '$KEYWORDS'"
1.229 + fi
1.230 + elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
1.231 + ARGS["${#ARGS[@]}"]="-l"
1.232 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el"
1.233 + elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
1.234 + ARGS["${#ARGS[@]}"]="-l"
1.235 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el"
1.236 + fi
1.237 +
1.238 + for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
1.239 + "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
1.240 + do
1.241 + if [ -f "$FILE" ]; then
1.242 + ARGS["${#ARGS[@]}"]="-l"
1.243 + ARGS["${#ARGS[@]}"]="$FILE"
1.244 + fi
1.245 + done
1.246 +
1.247 + case "$LOGIC" in
1.248 + /*)
1.249 + ;;
1.250 + */*)
1.251 + LOGIC="$(pwd -P)/$LOGIC"
1.252 + ;;
1.253 + esac
1.254 +
1.255 + export PROOFGENERAL_HOME="$SUPER"
1.256 + export PROOFGENERAL_ASSISTANTS="isar"
1.257 + export PROOFGENERAL_LOGIC="$LOGIC"
1.258 + export PROOFGENERAL_XSYMBOL="$XSYMBOL"
1.259 + export PROOFGENERAL_UNICODE="$UNICODE"
1.260 +
1.261 + export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
1.262 +
1.263 + exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"
1.264 +
1.265 +fi
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch Thu Jan 27 20:46:20 2011 +0100
2.3 @@ -0,0 +1,21 @@
2.4 +--- a/isar/isar-syntax.el Wed Aug 06 11:43:47 2008 +0200
2.5 ++++ b/isar/isar-syntax.el Thu Sep 18 15:21:16 2008 +0200
2.6 +@@ -252,14 +252,9 @@
2.7 +
2.8 + ;; antiquotations
2.9 +
2.10 +-;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for
2.11 +-;; incomplete antiquotations like @{text bla"} (even though it is supposed to
2.12 +-;; stop at eol anyway).
2.13 +-
2.14 +-(defconst isar-antiq-regexp
2.15 +- (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}")
2.16 +- "Regexp matching Isabelle/Isar antiquoations.")
2.17 +-
2.18 ++(defconst isar-antiq-regexp
2.19 ++ (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}")
2.20 ++ "Regexp matching Isabelle/Isar antiquotations.")
2.21 +
2.22 + ;; keyword nesting
2.23 +
2.24 +
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/Admin/ProofGeneral/3.7.1.1/menu.patch Thu Jan 27 20:46:20 2011 +0100
3.3 @@ -0,0 +1,30 @@
3.4 +--- a/isar/isar.el 2008-07-10 20:47:49.000000000 +0200
3.5 ++++ b/isar/isar.el 2009-11-26 20:51:44.103016094 +0100
3.6 +@@ -339,9 +339,12 @@
3.7 + (error "Aborted."))
3.8 + [(control p)])
3.9 +
3.10 +-(proof-definvisible isar-cmd-refute "refute" [r])
3.11 + (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)])
3.12 ++(proof-definvisible isar-cmd-nitpick "nitpick" [(control n)])
3.13 ++(proof-definvisible isar-cmd-refute "refute" [r])
3.14 + (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)])
3.15 ++(proof-definvisible isar-cmd-atp-kill "atp_kill")
3.16 ++(proof-definvisible isar-cmd-atp-info "atp_info")
3.17 +
3.18 + (defpgdefault menu-entries
3.19 + (append
3.20 +@@ -349,9 +352,12 @@
3.21 + (list
3.22 + (cons "Commands"
3.23 + (list
3.24 +- ["refute" isar-cmd-refute t]
3.25 + ["quickcheck" isar-cmd-quickcheck t]
3.26 ++ ["nitpick" isar-cmd-nitpick t]
3.27 ++ ["refute" isar-cmd-refute t]
3.28 + ["sledgehammer" isar-cmd-sledgehammer t]
3.29 ++ ["sledgehammer: kill" isar-cmd-atp-kill t]
3.30 ++ ["sledgehammer: info" isar-cmd-atp-info t]
3.31 + ["display draft" isar-cmd-display-draft t])))
3.32 + (list
3.33 + (cons "Show me ..."
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/Admin/ProofGeneral/3.7.1.1/progname.patch Thu Jan 27 20:46:20 2011 +0100
4.3 @@ -0,0 +1,89 @@
4.4 +--- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200
4.5 ++++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100
4.6 +@@ -97,8 +97,8 @@
4.7 + (if (or proof-rsh-command
4.8 + (file-executable-p isa-isatool-command))
4.9 + (let ((setting (isa-shell-command-to-string
4.10 +- (concat isa-isatool-command
4.11 +- " getenv -b " envvar))))
4.12 ++ (concat "\"" isa-isatool-command
4.13 ++ "\" getenv -b " envvar))))
4.14 + (if (string-equal setting "")
4.15 + default
4.16 + setting))
4.17 +@@ -125,15 +125,12 @@
4.18 + :type 'file
4.19 + :group 'isabelle)
4.20 +
4.21 +-(defvar isabelle-prog-name nil
4.22 +- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
4.23 +-
4.24 + (defun isa-tool-list-logics ()
4.25 + "Generate a list of available object logics."
4.26 + (if (isa-set-isatool-command)
4.27 + (delete "" (split-string
4.28 + (isa-shell-command-to-string
4.29 +- (concat isa-isatool-command " findlogics")) "[ \t]"))))
4.30 ++ (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]"))))
4.31 +
4.32 + (defcustom isabelle-logics-available nil
4.33 + "*List of logics available to use with Isabelle.
4.34 +@@ -177,7 +174,7 @@
4.35 +
4.36 + (defun isabelle-set-prog-name (&optional filename)
4.37 + "Make proper command line for running Isabelle.
4.38 +-This function sets `isabelle-prog-name' and `proof-prog-name'."
4.39 ++This function sets `proof-prog-name' and `isar-prog-args'."
4.40 + (let*
4.41 + ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
4.42 + ;; under the interface wrapper script) indicate command line
4.43 +@@ -187,21 +184,20 @@
4.44 + (getenv "ISABELLE") ; command line override
4.45 + (isa-getenv "ISABELLE") ; choose to match isatool
4.46 + "isabelle")) ; to
4.47 +- (isabelle-opts (getenv "ISABELLE_OPTIONS"))
4.48 +- (opts (concat " -PI" ;; Proof General + Isar
4.49 +- (if proof-shell-unicode " -m PGASCII" "")
4.50 +- (if (and isabelle-opts (not (equal isabelle-opts "")))
4.51 +- (concat " " isabelle-opts) "")))
4.52 ++ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
4.53 ++ (opts (append (list "-PI") ;; Proof General + Isar
4.54 ++ (if proof-shell-unicode (list "-m" "PGASCII") nil)
4.55 ++ isabelle-opts))
4.56 + (logic (or isabelle-chosen-logic
4.57 + (getenv "PROOFGENERAL_LOGIC")))
4.58 + (logicarg (if (and logic (not (equal logic "")))
4.59 +- (concat " " logic) "")))
4.60 ++ (list logic) nil)))
4.61 + (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
4.62 +- (setq isabelle-prog-name (concat isabelle opts logicarg))
4.63 +- (setq proof-prog-name isabelle-prog-name)))
4.64 ++ (setq isar-prog-args (append opts logicarg))
4.65 ++ (setq proof-prog-name isabelle)))
4.66 +
4.67 + (defun isabelle-choose-logic (logic)
4.68 +- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
4.69 ++ "Adjust proof-prog-name and isar-prog-args for running LOGIC."
4.70 + (interactive
4.71 + (list (completing-read
4.72 + "Use logic: "
4.73 +@@ -224,9 +220,7 @@
4.74 + (if (isa-set-isatool-command)
4.75 + (apply 'start-process
4.76 + "isa-view-doc" nil
4.77 +- (append (split-string
4.78 +- isa-isatool-command)
4.79 +- (list "doc" docname)))))
4.80 ++ (list isa-isatool-command "doc" docname))))
4.81 +
4.82 + (defun isa-tool-list-docs ()
4.83 + "Generate a list of documentation files available, with descriptions.
4.84 +@@ -236,7 +230,7 @@
4.85 + passed to isa-tool-doc-command, DOCNAME will be viewed."
4.86 + (if (isa-set-isatool-command)
4.87 + (let ((docs (isa-shell-command-to-string
4.88 +- (concat isa-isatool-command " doc"))))
4.89 ++ (concat "\"" isa-isatool-command "\" doc"))))
4.90 + (unless (string-equal docs "")
4.91 + (mapcan
4.92 + (function (lambda (docdes)
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/Admin/ProofGeneral/3.7.1.1/timeout.patch Thu Jan 27 20:46:20 2011 +0100
5.3 @@ -0,0 +1,11 @@
5.4 +--- a/generic/proof-config.el 2008-07-21 18:37:10.000000000 +0200
5.5 ++++ b/generic/proof-config.el 2009-11-29 17:41:37.409062091 +0100
5.6 +@@ -1493,7 +1493,7 @@
5.7 + :type '(choice string (const nil))
5.8 + :group 'proof-shell)
5.9 +
5.10 +-(defcustom proof-shell-quit-timeout 4
5.11 ++(defcustom proof-shell-quit-timeout 45
5.12 + ;; FIXME could add option to quiz user before rude kill.
5.13 + "The number of seconds to wait after sending proof-shell-quit-cmd.
5.14 + After this timeout, the proof shell will be killed off more rudely.
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/Admin/ProofGeneral/3.7.1.1/version.patch Thu Jan 27 20:46:20 2011 +0100
6.3 @@ -0,0 +1,20 @@
6.4 +--- a/generic/proof-site.el 2008-07-23 14:40:14.000000000 +0200
6.5 ++++ b/generic/proof-site.el 2009-11-28 16:13:56.409505412 +0100
6.6 +@@ -55,7 +55,7 @@
6.7 +
6.8 + (eval-and-compile
6.9 + ;; WARNING: do not edit next line (constant is edited in Makefile.devel)
6.10 +- (defconst proof-general-version "Proof General Version 3.7.1. Released by da on Wed 23 Jul 2008."
6.11 ++ (defconst proof-general-version "Proof General Version 3.7.1.1. Fabricated by makarius on Mon 30 Nov 2009."
6.12 + "Version string identifying Proof General release."))
6.13 +
6.14 + (defconst proof-general-short-version
6.15 +@@ -64,7 +64,7 @@
6.16 + (string-match "Version \\([^ ]+\\)\\." proof-general-version)
6.17 + (match-string 1 proof-general-version))))
6.18 +
6.19 +-(defconst proof-general-version-year "2008")
6.20 ++(defconst proof-general-version-year "2009")
6.21 +
6.22 + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
6.23 + ;;
7.1 --- a/Admin/ProofGeneral/interface Thu Jan 27 17:37:42 2011 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,262 +0,0 @@
7.4 -#!/usr/bin/env bash
7.5 -#
7.6 -# interface,v 9.1 2008/02/06 15:40:45 makarius Exp
7.7 -#
7.8 -# Proof General interface wrapper for Isabelle.
7.9 -
7.10 -
7.11 -## self references
7.12 -
7.13 -THIS="$(cd "$(dirname "$0")"; pwd)"
7.14 -SUPER="$(cd "$THIS/.."; pwd)"
7.15 -
7.16 -
7.17 -## diagnostics
7.18 -
7.19 -usage()
7.20 -{
7.21 - echo
7.22 - echo "Usage: Isabelle [OPTIONS] [FILES ...]"
7.23 - echo
7.24 - echo " Options are:"
7.25 - echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)"
7.26 - echo " -L NAME abbreviates -l NAME -k NAME"
7.27 - echo " -P BOOL actually start Proof General (default true), otherwise"
7.28 - echo " run plain tty session"
7.29 - echo " -U BOOL enable Unicode (UTF-8) communication (default true)"
7.30 - echo " -X BOOL configure the X-Symbol package on startup (default true)"
7.31 - echo " -f SIZE set X-Symbol font size (default 12)"
7.32 - echo " -g GEOMETRY specify Emacs geometry"
7.33 - echo " -k NAME use specific isar-keywords for named logic"
7.34 - echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
7.35 - echo " -m MODE add print mode for output"
7.36 - echo " -p NAME Emacs program name (default emacs)"
7.37 - echo " -u BOOL use personal .emacs file (default true)"
7.38 - echo " -w BOOL use window system (default true)"
7.39 - echo " -x BOOL enable the X-Symbol package on startup (default false)"
7.40 - echo
7.41 - echo "Starts Proof General for Isabelle with theory and proof FILES"
7.42 - echo "(default Scratch.thy)."
7.43 - echo
7.44 - echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS"
7.45 - echo
7.46 - exit 1
7.47 -}
7.48 -
7.49 -fail()
7.50 -{
7.51 - echo "$1" >&2
7.52 - exit 2
7.53 -}
7.54 -
7.55 -
7.56 -## process command line
7.57 -
7.58 -# options
7.59 -
7.60 -ISABELLE_OPTIONS=""
7.61 -ISAR="true"
7.62 -START_PG="true"
7.63 -GEOMETRY=""
7.64 -KEYWORDS=""
7.65 -LOGIC="$ISABELLE_LOGIC"
7.66 -PROGNAME="emacs"
7.67 -INITFILE="true"
7.68 -WINDOWSYSTEM="true"
7.69 -XSYMBOL=""
7.70 -XSYMBOL_SETUP=true
7.71 -XSYMBOL_FONTSIZE="12"
7.72 -UNICODE=""
7.73 -
7.74 -getoptions()
7.75 -{
7.76 - OPTIND=1
7.77 - while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT
7.78 - do
7.79 - case "$OPT" in
7.80 - I)
7.81 - ISAR="$OPTARG"
7.82 - ;;
7.83 - L)
7.84 - KEYWORDS="$OPTARG"
7.85 - LOGIC="$OPTARG"
7.86 - ;;
7.87 - P)
7.88 - START_PG="$OPTARG"
7.89 - ;;
7.90 - U)
7.91 - UNICODE="$OPTARG"
7.92 - ;;
7.93 - X)
7.94 - XSYMBOL_SETUP="$OPTARG"
7.95 - ;;
7.96 - f)
7.97 - XSYMBOL_FONTSIZE="$OPTARG"
7.98 - ;;
7.99 - g)
7.100 - GEOMETRY="$OPTARG"
7.101 - ;;
7.102 - k)
7.103 - KEYWORDS="$OPTARG"
7.104 - ;;
7.105 - l)
7.106 - LOGIC="$OPTARG"
7.107 - ;;
7.108 - m)
7.109 - if [ -z "$ISABELLE_OPTIONS" ]; then
7.110 - ISABELLE_OPTIONS="-m $OPTARG"
7.111 - else
7.112 - ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
7.113 - fi
7.114 - ;;
7.115 - p)
7.116 - PROGNAME="$OPTARG"
7.117 - ;;
7.118 - u)
7.119 - INITFILE="$OPTARG"
7.120 - ;;
7.121 - w)
7.122 - WINDOWSYSTEM="$OPTARG"
7.123 - ;;
7.124 - x)
7.125 - XSYMBOL="$OPTARG"
7.126 - ;;
7.127 - \?)
7.128 - usage
7.129 - ;;
7.130 - esac
7.131 - done
7.132 -}
7.133 -
7.134 -eval "OPTIONS=($PROOFGENERAL_OPTIONS)"
7.135 -getoptions "${OPTIONS[@]}"
7.136 -
7.137 -getoptions "$@"
7.138 -shift $(($OPTIND - 1))
7.139 -
7.140 -
7.141 -# args
7.142 -
7.143 -declare -a FILES=()
7.144 -
7.145 -if [ "$#" -eq 0 ]; then
7.146 - FILES["${#FILES[@]}"]="Scratch.thy"
7.147 -else
7.148 - while [ "$#" -gt 0 ]; do
7.149 - FILES["${#FILES[@]}"]="$1"
7.150 - shift
7.151 - done
7.152 -fi
7.153 -
7.154 -
7.155 -## smart X11 font installation
7.156 -
7.157 -function checkfonts ()
7.158 -{
7.159 - XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1
7.160 -
7.161 - case "$XLSFONTS" in
7.162 - xlsfonts:*)
7.163 - return 1
7.164 - ;;
7.165 - esac
7.166 -
7.167 - return 0
7.168 -}
7.169 -
7.170 -function installfonts ()
7.171 -{
7.172 - checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
7.173 -}
7.174 -
7.175 -
7.176 -## main
7.177 -
7.178 -# Isabelle2008 compatibility
7.179 -[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE"
7.180 -[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL"
7.181 -
7.182 -if [ "$START_PG" = false ]; then
7.183 -
7.184 - [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
7.185 - exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
7.186 -
7.187 -else
7.188 -
7.189 - declare -a ARGS=()
7.190 -
7.191 - if [ -n "$GEOMETRY" ]; then
7.192 - ARGS["${#ARGS[@]}"]="-geometry"
7.193 - ARGS["${#ARGS[@]}"]="$GEOMETRY"
7.194 - fi
7.195 -
7.196 - [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q"
7.197 -
7.198 - if [ "$WINDOWSYSTEM" = false ]; then
7.199 - ARGS["${#ARGS[@]}"]="-nw"
7.200 - XSYMBOL=false
7.201 - elif [ -z "$DISPLAY" ]; then
7.202 - XSYMBOL=false
7.203 - else
7.204 - [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts
7.205 - fi
7.206 -
7.207 - if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ]
7.208 - then
7.209 - if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ]
7.210 - then
7.211 - cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/"
7.212 - cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/"
7.213 - sleep 3
7.214 - fi
7.215 - fi
7.216 -
7.217 - ARGS["${#ARGS[@]}"]="-l"
7.218 - ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el"
7.219 -
7.220 - if [ -n "$KEYWORDS" ]; then
7.221 - if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
7.222 - ARGS["${#ARGS[@]}"]="-l"
7.223 - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el"
7.224 - elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
7.225 - ARGS["${#ARGS[@]}"]="-l"
7.226 - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el"
7.227 - else
7.228 - fail "No isar-keywords file for '$KEYWORDS'"
7.229 - fi
7.230 - elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
7.231 - ARGS["${#ARGS[@]}"]="-l"
7.232 - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el"
7.233 - elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
7.234 - ARGS["${#ARGS[@]}"]="-l"
7.235 - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el"
7.236 - fi
7.237 -
7.238 - for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
7.239 - "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
7.240 - do
7.241 - if [ -f "$FILE" ]; then
7.242 - ARGS["${#ARGS[@]}"]="-l"
7.243 - ARGS["${#ARGS[@]}"]="$FILE"
7.244 - fi
7.245 - done
7.246 -
7.247 - case "$LOGIC" in
7.248 - /*)
7.249 - ;;
7.250 - */*)
7.251 - LOGIC="$(pwd -P)/$LOGIC"
7.252 - ;;
7.253 - esac
7.254 -
7.255 - export PROOFGENERAL_HOME="$SUPER"
7.256 - export PROOFGENERAL_ASSISTANTS="isar"
7.257 - export PROOFGENERAL_LOGIC="$LOGIC"
7.258 - export PROOFGENERAL_XSYMBOL="$XSYMBOL"
7.259 - export PROOFGENERAL_UNICODE="$UNICODE"
7.260 -
7.261 - export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
7.262 -
7.263 - exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"
7.264 -
7.265 -fi
8.1 --- a/Admin/ProofGeneral/isar-antiq-regexp.patch Thu Jan 27 17:37:42 2011 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,21 +0,0 @@
8.4 ---- a/isar/isar-syntax.el Wed Aug 06 11:43:47 2008 +0200
8.5 -+++ b/isar/isar-syntax.el Thu Sep 18 15:21:16 2008 +0200
8.6 -@@ -252,14 +252,9 @@
8.7 -
8.8 - ;; antiquotations
8.9 -
8.10 --;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for
8.11 --;; incomplete antiquotations like @{text bla"} (even though it is supposed to
8.12 --;; stop at eol anyway).
8.13 --
8.14 --(defconst isar-antiq-regexp
8.15 -- (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}")
8.16 -- "Regexp matching Isabelle/Isar antiquoations.")
8.17 --
8.18 -+(defconst isar-antiq-regexp
8.19 -+ (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}")
8.20 -+ "Regexp matching Isabelle/Isar antiquotations.")
8.21 -
8.22 - ;; keyword nesting
8.23 -
8.24 -
9.1 --- a/Admin/ProofGeneral/menu.patch Thu Jan 27 17:37:42 2011 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,30 +0,0 @@
9.4 ---- a/isar/isar.el 2008-07-10 20:47:49.000000000 +0200
9.5 -+++ b/isar/isar.el 2009-11-26 20:51:44.103016094 +0100
9.6 -@@ -339,9 +339,12 @@
9.7 - (error "Aborted."))
9.8 - [(control p)])
9.9 -
9.10 --(proof-definvisible isar-cmd-refute "refute" [r])
9.11 - (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)])
9.12 -+(proof-definvisible isar-cmd-nitpick "nitpick" [(control n)])
9.13 -+(proof-definvisible isar-cmd-refute "refute" [r])
9.14 - (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)])
9.15 -+(proof-definvisible isar-cmd-atp-kill "atp_kill")
9.16 -+(proof-definvisible isar-cmd-atp-info "atp_info")
9.17 -
9.18 - (defpgdefault menu-entries
9.19 - (append
9.20 -@@ -349,9 +352,12 @@
9.21 - (list
9.22 - (cons "Commands"
9.23 - (list
9.24 -- ["refute" isar-cmd-refute t]
9.25 - ["quickcheck" isar-cmd-quickcheck t]
9.26 -+ ["nitpick" isar-cmd-nitpick t]
9.27 -+ ["refute" isar-cmd-refute t]
9.28 - ["sledgehammer" isar-cmd-sledgehammer t]
9.29 -+ ["sledgehammer: kill" isar-cmd-atp-kill t]
9.30 -+ ["sledgehammer: info" isar-cmd-atp-info t]
9.31 - ["display draft" isar-cmd-display-draft t])))
9.32 - (list
9.33 - (cons "Show me ..."
10.1 --- a/Admin/ProofGeneral/progname.patch Thu Jan 27 17:37:42 2011 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,89 +0,0 @@
10.4 ---- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200
10.5 -+++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100
10.6 -@@ -97,8 +97,8 @@
10.7 - (if (or proof-rsh-command
10.8 - (file-executable-p isa-isatool-command))
10.9 - (let ((setting (isa-shell-command-to-string
10.10 -- (concat isa-isatool-command
10.11 -- " getenv -b " envvar))))
10.12 -+ (concat "\"" isa-isatool-command
10.13 -+ "\" getenv -b " envvar))))
10.14 - (if (string-equal setting "")
10.15 - default
10.16 - setting))
10.17 -@@ -125,15 +125,12 @@
10.18 - :type 'file
10.19 - :group 'isabelle)
10.20 -
10.21 --(defvar isabelle-prog-name nil
10.22 -- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
10.23 --
10.24 - (defun isa-tool-list-logics ()
10.25 - "Generate a list of available object logics."
10.26 - (if (isa-set-isatool-command)
10.27 - (delete "" (split-string
10.28 - (isa-shell-command-to-string
10.29 -- (concat isa-isatool-command " findlogics")) "[ \t]"))))
10.30 -+ (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]"))))
10.31 -
10.32 - (defcustom isabelle-logics-available nil
10.33 - "*List of logics available to use with Isabelle.
10.34 -@@ -177,7 +174,7 @@
10.35 -
10.36 - (defun isabelle-set-prog-name (&optional filename)
10.37 - "Make proper command line for running Isabelle.
10.38 --This function sets `isabelle-prog-name' and `proof-prog-name'."
10.39 -+This function sets `proof-prog-name' and `isar-prog-args'."
10.40 - (let*
10.41 - ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
10.42 - ;; under the interface wrapper script) indicate command line
10.43 -@@ -187,21 +184,20 @@
10.44 - (getenv "ISABELLE") ; command line override
10.45 - (isa-getenv "ISABELLE") ; choose to match isatool
10.46 - "isabelle")) ; to
10.47 -- (isabelle-opts (getenv "ISABELLE_OPTIONS"))
10.48 -- (opts (concat " -PI" ;; Proof General + Isar
10.49 -- (if proof-shell-unicode " -m PGASCII" "")
10.50 -- (if (and isabelle-opts (not (equal isabelle-opts "")))
10.51 -- (concat " " isabelle-opts) "")))
10.52 -+ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
10.53 -+ (opts (append (list "-PI") ;; Proof General + Isar
10.54 -+ (if proof-shell-unicode (list "-m" "PGASCII") nil)
10.55 -+ isabelle-opts))
10.56 - (logic (or isabelle-chosen-logic
10.57 - (getenv "PROOFGENERAL_LOGIC")))
10.58 - (logicarg (if (and logic (not (equal logic "")))
10.59 -- (concat " " logic) "")))
10.60 -+ (list logic) nil)))
10.61 - (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
10.62 -- (setq isabelle-prog-name (concat isabelle opts logicarg))
10.63 -- (setq proof-prog-name isabelle-prog-name)))
10.64 -+ (setq isar-prog-args (append opts logicarg))
10.65 -+ (setq proof-prog-name isabelle)))
10.66 -
10.67 - (defun isabelle-choose-logic (logic)
10.68 -- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
10.69 -+ "Adjust proof-prog-name and isar-prog-args for running LOGIC."
10.70 - (interactive
10.71 - (list (completing-read
10.72 - "Use logic: "
10.73 -@@ -224,9 +220,7 @@
10.74 - (if (isa-set-isatool-command)
10.75 - (apply 'start-process
10.76 - "isa-view-doc" nil
10.77 -- (append (split-string
10.78 -- isa-isatool-command)
10.79 -- (list "doc" docname)))))
10.80 -+ (list isa-isatool-command "doc" docname))))
10.81 -
10.82 - (defun isa-tool-list-docs ()
10.83 - "Generate a list of documentation files available, with descriptions.
10.84 -@@ -236,7 +230,7 @@
10.85 - passed to isa-tool-doc-command, DOCNAME will be viewed."
10.86 - (if (isa-set-isatool-command)
10.87 - (let ((docs (isa-shell-command-to-string
10.88 -- (concat isa-isatool-command " doc"))))
10.89 -+ (concat "\"" isa-isatool-command "\" doc"))))
10.90 - (unless (string-equal docs "")
10.91 - (mapcan
10.92 - (function (lambda (docdes)
11.1 --- a/Admin/ProofGeneral/timeout.patch Thu Jan 27 17:37:42 2011 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,11 +0,0 @@
11.4 ---- a/generic/proof-config.el 2008-07-21 18:37:10.000000000 +0200
11.5 -+++ b/generic/proof-config.el 2009-11-29 17:41:37.409062091 +0100
11.6 -@@ -1493,7 +1493,7 @@
11.7 - :type '(choice string (const nil))
11.8 - :group 'proof-shell)
11.9 -
11.10 --(defcustom proof-shell-quit-timeout 4
11.11 -+(defcustom proof-shell-quit-timeout 45
11.12 - ;; FIXME could add option to quiz user before rude kill.
11.13 - "The number of seconds to wait after sending proof-shell-quit-cmd.
11.14 - After this timeout, the proof shell will be killed off more rudely.
12.1 --- a/Admin/ProofGeneral/version.patch Thu Jan 27 17:37:42 2011 +0100
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,20 +0,0 @@
12.4 ---- a/generic/proof-site.el 2008-07-23 14:40:14.000000000 +0200
12.5 -+++ b/generic/proof-site.el 2009-11-28 16:13:56.409505412 +0100
12.6 -@@ -55,7 +55,7 @@
12.7 -
12.8 - (eval-and-compile
12.9 - ;; WARNING: do not edit next line (constant is edited in Makefile.devel)
12.10 -- (defconst proof-general-version "Proof General Version 3.7.1. Released by da on Wed 23 Jul 2008."
12.11 -+ (defconst proof-general-version "Proof General Version 3.7.1.1. Fabricated by makarius on Mon 30 Nov 2009."
12.12 - "Version string identifying Proof General release."))
12.13 -
12.14 - (defconst proof-general-short-version
12.15 -@@ -64,7 +64,7 @@
12.16 - (string-match "Version \\([^ ]+\\)\\." proof-general-version)
12.17 - (match-string 1 proof-general-version))))
12.18 -
12.19 --(defconst proof-general-version-year "2008")
12.20 -+(defconst proof-general-version-year "2009")
12.21 -
12.22 - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
12.23 - ;;