# HG changeset patch
# User wenzelm
# Date 1296157580 -3600
# Node ID d1cac8c778ed7540acec00b400a40d382867ae71
# Parent  e4c03351301ac1cb01ced4d1f828f1f6182d985d
old Proof General patches;

diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/3.7.1.1/interface
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/3.7.1.1/interface	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
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch	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
+ 
+
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/3.7.1.1/menu.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/3.7.1.1/menu.patch	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 ..."
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/3.7.1.1/progname.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/3.7.1.1/progname.patch	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)
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/3.7.1.1/timeout.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/3.7.1.1/timeout.patch	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.
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/3.7.1.1/version.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/3.7.1.1/version.patch	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")
+ 
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+ ;;
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/interface
--- 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
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/isar-antiq-regexp.patch
--- 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
- 
-
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/menu.patch
--- 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 ..."
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/progname.patch
--- 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)
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/timeout.patch
--- 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.
diff -r e4c03351301a -r d1cac8c778ed Admin/ProofGeneral/version.patch
--- 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")
- 
- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
- ;;