--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/3.7.1.1/interface Thu Jan 27 20:46:20 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 Thu Jan 27 20:46:20 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 Thu Jan 27 20:46:20 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 Thu Jan 27 20:46:20 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 Thu Jan 27 20:46:20 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 Thu Jan 27 20:46:20 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")
+
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+ ;;
--- a/Admin/ProofGeneral/interface Thu Jan 27 17:37:42 2011 +0100
+++ /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 Thu Jan 27 17:37:42 2011 +0100
+++ /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 Thu Jan 27 17:37:42 2011 +0100
+++ /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 Thu Jan 27 17:37:42 2011 +0100
+++ /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 Thu Jan 27 17:37:42 2011 +0100
+++ /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 Thu Jan 27 17:37:42 2011 +0100
+++ /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")
-
- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
- ;;