discontinued Proof General;
authorwenzelm
Fri Oct 31 11:18:17 2014 +0100 (2014-10-31)
changeset 5884222b87ab47d3b
parent 58840 f4bb3068d819
child 58843 521cea5fa777
discontinued Proof General;
Admin/ProofGeneral/3.7.1.1/interface
Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch
Admin/ProofGeneral/3.7.1.1/menu.patch
Admin/ProofGeneral/3.7.1.1/progname.patch
Admin/ProofGeneral/3.7.1.1/timeout.patch
Admin/ProofGeneral/3.7.1.1/version.patch
Admin/components/optional
Admin/lib/Tools/update_keywords
NEWS
bin/isabelle_process
etc/isar-keywords-ZF.el
etc/isar-keywords.el
lib/Tools/keywords
src/Doc/Classes/Classes.thy
src/Doc/Implementation/ML.thy
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Doc/Isar_Ref/Outer_Syntax.thy
src/Doc/System/Basics.thy
src/Doc/Tutorial/Documents/Documents.thy
src/Doc/Tutorial/Types/Overloading.thy
src/HOL/ROOT
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/try0.ML
src/HOL/ex/Nominal2_Dummy.thy
src/Pure/General/secure.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/keywords.scala
src/Pure/Tools/proof_general.ML
src/Pure/build-jars
src/Pure/pure_syn.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/Admin/ProofGeneral/3.7.1.1/interface	Thu Oct 30 23:14:11 2014 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,262 +0,0 @@
     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 --- a/Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch	Thu Oct 30 23:14:11 2014 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,21 +0,0 @@
     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 --- a/Admin/ProofGeneral/3.7.1.1/menu.patch	Thu Oct 30 23:14:11 2014 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,30 +0,0 @@
     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 --- a/Admin/ProofGeneral/3.7.1.1/progname.patch	Thu Oct 30 23:14:11 2014 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,89 +0,0 @@
     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 --- a/Admin/ProofGeneral/3.7.1.1/timeout.patch	Thu Oct 30 23:14:11 2014 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,11 +0,0 @@
     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 --- a/Admin/ProofGeneral/3.7.1.1/version.patch	Thu Oct 30 23:14:11 2014 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,20 +0,0 @@
     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/components/optional	Thu Oct 30 23:14:11 2014 +0100
     7.2 +++ b/Admin/components/optional	Fri Oct 31 11:18:17 2014 +0100
     7.3 @@ -1,3 +1,2 @@
     7.4  #optional components that could impact build time significantly
     7.5  hol-light-bundle-0.5-126
     7.6 -ProofGeneral-4.2-2
     8.1 --- a/Admin/lib/Tools/update_keywords	Thu Oct 30 23:14:11 2014 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,15 +0,0 @@
     8.4 -#!/usr/bin/env bash
     8.5 -#
     8.6 -# Author: Makarius
     8.7 -#
     8.8 -# DESCRIPTION: update standard keyword files for Emacs Proof General
     8.9 -# (Proof General legacy)
    8.10 -
    8.11 -isabelle_admin_build jars || exit $?
    8.12 -
    8.13 -declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
    8.14 -
    8.15 -cd "$ISABELLE_HOME/etc"
    8.16 -
    8.17 -"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords update_keywords
    8.18 -
     9.1 --- a/NEWS	Thu Oct 30 23:14:11 2014 +0100
     9.2 +++ b/NEWS	Fri Oct 31 11:18:17 2014 +0100
     9.3 @@ -187,6 +187,8 @@
     9.4  
     9.5  *** System ***
     9.6  
     9.7 +* Proof General support has been discontinued.  Minor INCOMPATIBILITY.
     9.8 +
     9.9  * The Isabelle tool "update_cartouches" changes theory files to use
    9.10  cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
    9.11  
    10.1 --- a/bin/isabelle_process	Thu Oct 30 23:14:11 2014 +0100
    10.2 +++ b/bin/isabelle_process	Fri Oct 31 11:18:17 2014 +0100
    10.3 @@ -28,7 +28,6 @@
    10.4    echo "  Options are:"
    10.5    echo "    -I           startup Isar interaction mode"
    10.6    echo "    -O           system options from given YXML file"
    10.7 -  echo "    -P           startup Proof General interaction mode"
    10.8    echo "    -S           secure mode -- disallow critical operations"
    10.9    echo "    -T ADDR      startup process wrapper, with socket address"
   10.10    echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
   10.11 @@ -60,7 +59,6 @@
   10.12  
   10.13  ISAR=""
   10.14  OPTIONS_FILE=""
   10.15 -PROOFGENERAL=""
   10.16  SECURE=""
   10.17  WRAPPER_SOCKET=""
   10.18  WRAPPER_FIFOS=""
   10.19 @@ -71,7 +69,7 @@
   10.20  READONLY=""
   10.21  NOWRITE=""
   10.22  
   10.23 -while getopts "IO:PST:W:e:m:o:qrw" OPT
   10.24 +while getopts "IO:ST:W:e:m:o:qrw" OPT
   10.25  do
   10.26    case "$OPT" in
   10.27      I)
   10.28 @@ -80,9 +78,6 @@
   10.29      O)
   10.30        OPTIONS_FILE="$OPTARG"
   10.31        ;;
   10.32 -    P)
   10.33 -      PROOFGENERAL=true
   10.34 -      ;;
   10.35      S)
   10.36        SECURE=true
   10.37        ;;
   10.38 @@ -237,9 +232,7 @@
   10.39    if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
   10.40      MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
   10.41    fi
   10.42 -  if [ -n "$PROOFGENERAL" ]; then
   10.43 -    MLTEXT="$MLTEXT; ProofGeneral.init ();"
   10.44 -  elif [ -n "$ISAR" ]; then
   10.45 +  if [ -n "$ISAR" ]; then
   10.46      MLTEXT="$MLTEXT; Isar.main ();"
   10.47    else
   10.48      NICE=""
    11.1 --- a/etc/isar-keywords-ZF.el	Thu Oct 30 23:14:11 2014 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,502 +0,0 @@
    11.4 -;;
    11.5 -;; Keyword classification tables for Isabelle/Isar.
    11.6 -;; Generated from Pure + ZF.
    11.7 -;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
    11.8 -;;
    11.9 -
   11.10 -(defconst isar-keywords-major
   11.11 -  '("\\."
   11.12 -    "\\.\\."
   11.13 -    "Isabelle\\.command"
   11.14 -    "ML"
   11.15 -    "ML_command"
   11.16 -    "ML_file"
   11.17 -    "ML_prf"
   11.18 -    "ML_val"
   11.19 -    "ProofGeneral\\.inform_file_processed"
   11.20 -    "ProofGeneral\\.inform_file_retracted"
   11.21 -    "ProofGeneral\\.kill_proof"
   11.22 -    "ProofGeneral\\.pr"
   11.23 -    "ProofGeneral\\.process_pgip"
   11.24 -    "ProofGeneral\\.restart"
   11.25 -    "ProofGeneral\\.undo"
   11.26 -    "SML_export"
   11.27 -    "SML_file"
   11.28 -    "SML_import"
   11.29 -    "abbreviation"
   11.30 -    "also"
   11.31 -    "apply"
   11.32 -    "apply_end"
   11.33 -    "assume"
   11.34 -    "attribute_setup"
   11.35 -    "axiomatization"
   11.36 -    "back"
   11.37 -    "bundle"
   11.38 -    "by"
   11.39 -    "cannot_undo"
   11.40 -    "case"
   11.41 -    "chapter"
   11.42 -    "class"
   11.43 -    "class_deps"
   11.44 -    "codatatype"
   11.45 -    "code_datatype"
   11.46 -    "coinductive"
   11.47 -    "commit"
   11.48 -    "consts"
   11.49 -    "context"
   11.50 -    "corollary"
   11.51 -    "datatype"
   11.52 -    "declaration"
   11.53 -    "declare"
   11.54 -    "def"
   11.55 -    "default_sort"
   11.56 -    "defer"
   11.57 -    "definition"
   11.58 -    "defs"
   11.59 -    "disable_pr"
   11.60 -    "display_drafts"
   11.61 -    "done"
   11.62 -    "enable_pr"
   11.63 -    "end"
   11.64 -    "exit"
   11.65 -    "extract"
   11.66 -    "extract_type"
   11.67 -    "finally"
   11.68 -    "find_consts"
   11.69 -    "find_theorems"
   11.70 -    "fix"
   11.71 -    "from"
   11.72 -    "full_prf"
   11.73 -    "guess"
   11.74 -    "have"
   11.75 -    "header"
   11.76 -    "help"
   11.77 -    "hence"
   11.78 -    "hide_class"
   11.79 -    "hide_const"
   11.80 -    "hide_fact"
   11.81 -    "hide_type"
   11.82 -    "include"
   11.83 -    "including"
   11.84 -    "inductive"
   11.85 -    "inductive_cases"
   11.86 -    "init_toplevel"
   11.87 -    "instance"
   11.88 -    "instantiation"
   11.89 -    "interpret"
   11.90 -    "interpretation"
   11.91 -    "judgment"
   11.92 -    "kill"
   11.93 -    "kill_thy"
   11.94 -    "lemma"
   11.95 -    "lemmas"
   11.96 -    "let"
   11.97 -    "linear_undo"
   11.98 -    "local_setup"
   11.99 -    "locale"
  11.100 -    "locale_deps"
  11.101 -    "method_setup"
  11.102 -    "moreover"
  11.103 -    "named_theorems"
  11.104 -    "next"
  11.105 -    "no_notation"
  11.106 -    "no_syntax"
  11.107 -    "no_translations"
  11.108 -    "no_type_notation"
  11.109 -    "nonterminal"
  11.110 -    "notation"
  11.111 -    "note"
  11.112 -    "notepad"
  11.113 -    "obtain"
  11.114 -    "oops"
  11.115 -    "oracle"
  11.116 -    "overloading"
  11.117 -    "parse_ast_translation"
  11.118 -    "parse_translation"
  11.119 -    "pr"
  11.120 -    "prefer"
  11.121 -    "presume"
  11.122 -    "pretty_setmargin"
  11.123 -    "prf"
  11.124 -    "primrec"
  11.125 -    "print_ML_antiquotations"
  11.126 -    "print_abbrevs"
  11.127 -    "print_antiquotations"
  11.128 -    "print_ast_translation"
  11.129 -    "print_attributes"
  11.130 -    "print_binds"
  11.131 -    "print_bundles"
  11.132 -    "print_cases"
  11.133 -    "print_claset"
  11.134 -    "print_classes"
  11.135 -    "print_codesetup"
  11.136 -    "print_commands"
  11.137 -    "print_context"
  11.138 -    "print_defn_rules"
  11.139 -    "print_dependencies"
  11.140 -    "print_facts"
  11.141 -    "print_induct_rules"
  11.142 -    "print_interps"
  11.143 -    "print_locale"
  11.144 -    "print_locales"
  11.145 -    "print_methods"
  11.146 -    "print_options"
  11.147 -    "print_rules"
  11.148 -    "print_simpset"
  11.149 -    "print_state"
  11.150 -    "print_statement"
  11.151 -    "print_syntax"
  11.152 -    "print_tcset"
  11.153 -    "print_term_bindings"
  11.154 -    "print_theorems"
  11.155 -    "print_theory"
  11.156 -    "print_trans_rules"
  11.157 -    "print_translation"
  11.158 -    "proof"
  11.159 -    "prop"
  11.160 -    "qed"
  11.161 -    "quit"
  11.162 -    "realizability"
  11.163 -    "realizers"
  11.164 -    "remove_thy"
  11.165 -    "rep_datatype"
  11.166 -    "schematic_corollary"
  11.167 -    "schematic_lemma"
  11.168 -    "schematic_theorem"
  11.169 -    "sect"
  11.170 -    "section"
  11.171 -    "setup"
  11.172 -    "show"
  11.173 -    "simproc_setup"
  11.174 -    "sorry"
  11.175 -    "subclass"
  11.176 -    "sublocale"
  11.177 -    "subsect"
  11.178 -    "subsection"
  11.179 -    "subsubsect"
  11.180 -    "subsubsection"
  11.181 -    "syntax"
  11.182 -    "syntax_declaration"
  11.183 -    "term"
  11.184 -    "text"
  11.185 -    "text_raw"
  11.186 -    "then"
  11.187 -    "theorem"
  11.188 -    "theorems"
  11.189 -    "theory"
  11.190 -    "thm"
  11.191 -    "thm_deps"
  11.192 -    "thus"
  11.193 -    "thy_deps"
  11.194 -    "translations"
  11.195 -    "txt"
  11.196 -    "txt_raw"
  11.197 -    "typ"
  11.198 -    "type_notation"
  11.199 -    "type_synonym"
  11.200 -    "typed_print_translation"
  11.201 -    "typedecl"
  11.202 -    "ultimately"
  11.203 -    "undo"
  11.204 -    "undos_proof"
  11.205 -    "unfolding"
  11.206 -    "unused_thms"
  11.207 -    "use_thy"
  11.208 -    "using"
  11.209 -    "welcome"
  11.210 -    "with"
  11.211 -    "write"
  11.212 -    "{"
  11.213 -    "}"))
  11.214 -
  11.215 -(defconst isar-keywords-minor
  11.216 -  '("and"
  11.217 -    "assumes"
  11.218 -    "attach"
  11.219 -    "begin"
  11.220 -    "binder"
  11.221 -    "case_eqns"
  11.222 -    "con_defs"
  11.223 -    "constrains"
  11.224 -    "defines"
  11.225 -    "domains"
  11.226 -    "elimination"
  11.227 -    "fixes"
  11.228 -    "for"
  11.229 -    "identifier"
  11.230 -    "if"
  11.231 -    "imports"
  11.232 -    "in"
  11.233 -    "includes"
  11.234 -    "induction"
  11.235 -    "infix"
  11.236 -    "infixl"
  11.237 -    "infixr"
  11.238 -    "intros"
  11.239 -    "is"
  11.240 -    "keywords"
  11.241 -    "monos"
  11.242 -    "notes"
  11.243 -    "obtains"
  11.244 -    "open"
  11.245 -    "output"
  11.246 -    "overloaded"
  11.247 -    "pervasive"
  11.248 -    "recursor_eqns"
  11.249 -    "shows"
  11.250 -    "structure"
  11.251 -    "type_elims"
  11.252 -    "type_intros"
  11.253 -    "unchecked"
  11.254 -    "where"))
  11.255 -
  11.256 -(defconst isar-keywords-control
  11.257 -  '("Isabelle\\.command"
  11.258 -    "ProofGeneral\\.inform_file_processed"
  11.259 -    "ProofGeneral\\.inform_file_retracted"
  11.260 -    "ProofGeneral\\.kill_proof"
  11.261 -    "ProofGeneral\\.pr"
  11.262 -    "ProofGeneral\\.process_pgip"
  11.263 -    "ProofGeneral\\.restart"
  11.264 -    "ProofGeneral\\.undo"
  11.265 -    "cannot_undo"
  11.266 -    "commit"
  11.267 -    "disable_pr"
  11.268 -    "enable_pr"
  11.269 -    "exit"
  11.270 -    "init_toplevel"
  11.271 -    "kill"
  11.272 -    "kill_thy"
  11.273 -    "linear_undo"
  11.274 -    "pretty_setmargin"
  11.275 -    "quit"
  11.276 -    "remove_thy"
  11.277 -    "undo"
  11.278 -    "undos_proof"
  11.279 -    "use_thy"))
  11.280 -
  11.281 -(defconst isar-keywords-diag
  11.282 -  '("ML_command"
  11.283 -    "ML_val"
  11.284 -    "class_deps"
  11.285 -    "display_drafts"
  11.286 -    "find_consts"
  11.287 -    "find_theorems"
  11.288 -    "full_prf"
  11.289 -    "header"
  11.290 -    "help"
  11.291 -    "locale_deps"
  11.292 -    "pr"
  11.293 -    "prf"
  11.294 -    "print_ML_antiquotations"
  11.295 -    "print_abbrevs"
  11.296 -    "print_antiquotations"
  11.297 -    "print_attributes"
  11.298 -    "print_binds"
  11.299 -    "print_bundles"
  11.300 -    "print_cases"
  11.301 -    "print_claset"
  11.302 -    "print_classes"
  11.303 -    "print_codesetup"
  11.304 -    "print_commands"
  11.305 -    "print_context"
  11.306 -    "print_defn_rules"
  11.307 -    "print_dependencies"
  11.308 -    "print_facts"
  11.309 -    "print_induct_rules"
  11.310 -    "print_interps"
  11.311 -    "print_locale"
  11.312 -    "print_locales"
  11.313 -    "print_methods"
  11.314 -    "print_options"
  11.315 -    "print_rules"
  11.316 -    "print_simpset"
  11.317 -    "print_state"
  11.318 -    "print_statement"
  11.319 -    "print_syntax"
  11.320 -    "print_tcset"
  11.321 -    "print_term_bindings"
  11.322 -    "print_theorems"
  11.323 -    "print_theory"
  11.324 -    "print_trans_rules"
  11.325 -    "prop"
  11.326 -    "term"
  11.327 -    "thm"
  11.328 -    "thm_deps"
  11.329 -    "thy_deps"
  11.330 -    "typ"
  11.331 -    "unused_thms"
  11.332 -    "welcome"))
  11.333 -
  11.334 -(defconst isar-keywords-theory-begin
  11.335 -  '("theory"))
  11.336 -
  11.337 -(defconst isar-keywords-theory-switch
  11.338 -  '())
  11.339 -
  11.340 -(defconst isar-keywords-theory-end
  11.341 -  '("end"))
  11.342 -
  11.343 -(defconst isar-keywords-theory-heading
  11.344 -  '("chapter"
  11.345 -    "section"
  11.346 -    "subsection"
  11.347 -    "subsubsection"))
  11.348 -
  11.349 -(defconst isar-keywords-theory-decl
  11.350 -  '("ML"
  11.351 -    "ML_file"
  11.352 -    "SML_export"
  11.353 -    "SML_file"
  11.354 -    "SML_import"
  11.355 -    "abbreviation"
  11.356 -    "attribute_setup"
  11.357 -    "axiomatization"
  11.358 -    "bundle"
  11.359 -    "class"
  11.360 -    "codatatype"
  11.361 -    "code_datatype"
  11.362 -    "coinductive"
  11.363 -    "consts"
  11.364 -    "context"
  11.365 -    "datatype"
  11.366 -    "declaration"
  11.367 -    "declare"
  11.368 -    "default_sort"
  11.369 -    "definition"
  11.370 -    "defs"
  11.371 -    "extract"
  11.372 -    "extract_type"
  11.373 -    "hide_class"
  11.374 -    "hide_const"
  11.375 -    "hide_fact"
  11.376 -    "hide_type"
  11.377 -    "inductive"
  11.378 -    "inductive_cases"
  11.379 -    "instantiation"
  11.380 -    "judgment"
  11.381 -    "lemmas"
  11.382 -    "local_setup"
  11.383 -    "locale"
  11.384 -    "method_setup"
  11.385 -    "named_theorems"
  11.386 -    "no_notation"
  11.387 -    "no_syntax"
  11.388 -    "no_translations"
  11.389 -    "no_type_notation"
  11.390 -    "nonterminal"
  11.391 -    "notation"
  11.392 -    "notepad"
  11.393 -    "oracle"
  11.394 -    "overloading"
  11.395 -    "parse_ast_translation"
  11.396 -    "parse_translation"
  11.397 -    "primrec"
  11.398 -    "print_ast_translation"
  11.399 -    "print_translation"
  11.400 -    "realizability"
  11.401 -    "realizers"
  11.402 -    "rep_datatype"
  11.403 -    "setup"
  11.404 -    "simproc_setup"
  11.405 -    "syntax"
  11.406 -    "syntax_declaration"
  11.407 -    "text"
  11.408 -    "text_raw"
  11.409 -    "theorems"
  11.410 -    "translations"
  11.411 -    "type_notation"
  11.412 -    "type_synonym"
  11.413 -    "typed_print_translation"
  11.414 -    "typedecl"))
  11.415 -
  11.416 -(defconst isar-keywords-theory-script
  11.417 -  '())
  11.418 -
  11.419 -(defconst isar-keywords-theory-goal
  11.420 -  '("corollary"
  11.421 -    "instance"
  11.422 -    "interpretation"
  11.423 -    "lemma"
  11.424 -    "schematic_corollary"
  11.425 -    "schematic_lemma"
  11.426 -    "schematic_theorem"
  11.427 -    "subclass"
  11.428 -    "sublocale"
  11.429 -    "theorem"))
  11.430 -
  11.431 -(defconst isar-keywords-qed
  11.432 -  '("\\."
  11.433 -    "\\.\\."
  11.434 -    "by"
  11.435 -    "done"
  11.436 -    "sorry"))
  11.437 -
  11.438 -(defconst isar-keywords-qed-block
  11.439 -  '("qed"))
  11.440 -
  11.441 -(defconst isar-keywords-qed-global
  11.442 -  '("oops"))
  11.443 -
  11.444 -(defconst isar-keywords-proof-heading
  11.445 -  '("sect"
  11.446 -    "subsect"
  11.447 -    "subsubsect"))
  11.448 -
  11.449 -(defconst isar-keywords-proof-goal
  11.450 -  '("have"
  11.451 -    "hence"
  11.452 -    "interpret"))
  11.453 -
  11.454 -(defconst isar-keywords-proof-block
  11.455 -  '("next"
  11.456 -    "proof"))
  11.457 -
  11.458 -(defconst isar-keywords-proof-open
  11.459 -  '("{"))
  11.460 -
  11.461 -(defconst isar-keywords-proof-close
  11.462 -  '("}"))
  11.463 -
  11.464 -(defconst isar-keywords-proof-chain
  11.465 -  '("finally"
  11.466 -    "from"
  11.467 -    "then"
  11.468 -    "ultimately"
  11.469 -    "with"))
  11.470 -
  11.471 -(defconst isar-keywords-proof-decl
  11.472 -  '("ML_prf"
  11.473 -    "also"
  11.474 -    "include"
  11.475 -    "including"
  11.476 -    "let"
  11.477 -    "moreover"
  11.478 -    "note"
  11.479 -    "txt"
  11.480 -    "txt_raw"
  11.481 -    "unfolding"
  11.482 -    "using"
  11.483 -    "write"))
  11.484 -
  11.485 -(defconst isar-keywords-proof-asm
  11.486 -  '("assume"
  11.487 -    "case"
  11.488 -    "def"
  11.489 -    "fix"
  11.490 -    "presume"))
  11.491 -
  11.492 -(defconst isar-keywords-proof-asm-goal
  11.493 -  '("guess"
  11.494 -    "obtain"
  11.495 -    "show"
  11.496 -    "thus"))
  11.497 -
  11.498 -(defconst isar-keywords-proof-script
  11.499 -  '("apply"
  11.500 -    "apply_end"
  11.501 -    "back"
  11.502 -    "defer"
  11.503 -    "prefer"))
  11.504 -
  11.505 -(provide 'isar-keywords)
    12.1 --- a/etc/isar-keywords.el	Thu Oct 30 23:14:11 2014 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,718 +0,0 @@
    12.4 -;;
    12.5 -;; Keyword classification tables for Isabelle/Isar.
    12.6 -;; Generated from HOL + HOL-Auth + HOL-Bali + HOL-Datatype_Examples + HOL-Decision_Procs + HOL-Hahn_Banach + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Induct + HOL-Library + HOL-Multivariate_Analysis + HOL-Mutabelle + HOL-Nominal + HOL-Predicate_Compile_Examples + HOL-Probability + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
    12.7 -;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
    12.8 -;;
    12.9 -
   12.10 -(defconst isar-keywords-major
   12.11 -  '("\\."
   12.12 -    "\\.\\."
   12.13 -    "Isabelle\\.command"
   12.14 -    "ML"
   12.15 -    "ML_command"
   12.16 -    "ML_file"
   12.17 -    "ML_prf"
   12.18 -    "ML_val"
   12.19 -    "ProofGeneral\\.inform_file_processed"
   12.20 -    "ProofGeneral\\.inform_file_retracted"
   12.21 -    "ProofGeneral\\.kill_proof"
   12.22 -    "ProofGeneral\\.pr"
   12.23 -    "ProofGeneral\\.process_pgip"
   12.24 -    "ProofGeneral\\.restart"
   12.25 -    "ProofGeneral\\.undo"
   12.26 -    "SML_export"
   12.27 -    "SML_file"
   12.28 -    "SML_import"
   12.29 -    "abbreviation"
   12.30 -    "adhoc_overloading"
   12.31 -    "also"
   12.32 -    "apply"
   12.33 -    "apply_end"
   12.34 -    "approximate"
   12.35 -    "assume"
   12.36 -    "atom_decl"
   12.37 -    "attribute_setup"
   12.38 -    "axiomatization"
   12.39 -    "back"
   12.40 -    "bnf"
   12.41 -    "bnf_axiomatization"
   12.42 -    "boogie_file"
   12.43 -    "bundle"
   12.44 -    "by"
   12.45 -    "cannot_undo"
   12.46 -    "cartouche"
   12.47 -    "case"
   12.48 -    "case_of_simps"
   12.49 -    "chapter"
   12.50 -    "class"
   12.51 -    "class_deps"
   12.52 -    "codatatype"
   12.53 -    "code_datatype"
   12.54 -    "code_deps"
   12.55 -    "code_identifier"
   12.56 -    "code_monad"
   12.57 -    "code_pred"
   12.58 -    "code_printing"
   12.59 -    "code_reflect"
   12.60 -    "code_reserved"
   12.61 -    "code_thms"
   12.62 -    "coinductive"
   12.63 -    "coinductive_set"
   12.64 -    "commit"
   12.65 -    "consts"
   12.66 -    "context"
   12.67 -    "corollary"
   12.68 -    "cpodef"
   12.69 -    "datatype"
   12.70 -    "datatype_compat"
   12.71 -    "declaration"
   12.72 -    "declare"
   12.73 -    "def"
   12.74 -    "default_sort"
   12.75 -    "defer"
   12.76 -    "defer_recdef"
   12.77 -    "definition"
   12.78 -    "defs"
   12.79 -    "disable_pr"
   12.80 -    "display_drafts"
   12.81 -    "domain"
   12.82 -    "domain_isomorphism"
   12.83 -    "domaindef"
   12.84 -    "done"
   12.85 -    "enable_pr"
   12.86 -    "end"
   12.87 -    "equivariance"
   12.88 -    "exit"
   12.89 -    "export_code"
   12.90 -    "extract"
   12.91 -    "extract_type"
   12.92 -    "finally"
   12.93 -    "find_consts"
   12.94 -    "find_theorems"
   12.95 -    "find_unused_assms"
   12.96 -    "fix"
   12.97 -    "fixrec"
   12.98 -    "free_constructors"
   12.99 -    "from"
  12.100 -    "full_prf"
  12.101 -    "fun"
  12.102 -    "fun_cases"
  12.103 -    "function"
  12.104 -    "functor"
  12.105 -    "guess"
  12.106 -    "have"
  12.107 -    "header"
  12.108 -    "help"
  12.109 -    "hence"
  12.110 -    "hide_class"
  12.111 -    "hide_const"
  12.112 -    "hide_fact"
  12.113 -    "hide_type"
  12.114 -    "import_const_map"
  12.115 -    "import_file"
  12.116 -    "import_tptp"
  12.117 -    "import_type_map"
  12.118 -    "include"
  12.119 -    "including"
  12.120 -    "inductive"
  12.121 -    "inductive_cases"
  12.122 -    "inductive_set"
  12.123 -    "inductive_simps"
  12.124 -    "init_toplevel"
  12.125 -    "instance"
  12.126 -    "instantiation"
  12.127 -    "interpret"
  12.128 -    "interpretation"
  12.129 -    "judgment"
  12.130 -    "kill"
  12.131 -    "kill_thy"
  12.132 -    "lemma"
  12.133 -    "lemmas"
  12.134 -    "let"
  12.135 -    "lift_definition"
  12.136 -    "lifting_forget"
  12.137 -    "lifting_update"
  12.138 -    "linear_undo"
  12.139 -    "local_setup"
  12.140 -    "locale"
  12.141 -    "locale_deps"
  12.142 -    "method_setup"
  12.143 -    "moreover"
  12.144 -    "named_theorems"
  12.145 -    "next"
  12.146 -    "nitpick"
  12.147 -    "nitpick_params"
  12.148 -    "no_adhoc_overloading"
  12.149 -    "no_notation"
  12.150 -    "no_syntax"
  12.151 -    "no_translations"
  12.152 -    "no_type_notation"
  12.153 -    "nominal_datatype"
  12.154 -    "nominal_function"
  12.155 -    "nominal_inductive"
  12.156 -    "nominal_inductive2"
  12.157 -    "nominal_primrec"
  12.158 -    "nominal_termination"
  12.159 -    "nonterminal"
  12.160 -    "notation"
  12.161 -    "note"
  12.162 -    "notepad"
  12.163 -    "obtain"
  12.164 -    "old_datatype"
  12.165 -    "old_rep_datatype"
  12.166 -    "old_smt_status"
  12.167 -    "oops"
  12.168 -    "oracle"
  12.169 -    "overloading"
  12.170 -    "parse_ast_translation"
  12.171 -    "parse_translation"
  12.172 -    "partial_function"
  12.173 -    "pcpodef"
  12.174 -    "permanent_interpretation"
  12.175 -    "pr"
  12.176 -    "prefer"
  12.177 -    "presume"
  12.178 -    "pretty_setmargin"
  12.179 -    "prf"
  12.180 -    "primcorec"
  12.181 -    "primcorecursive"
  12.182 -    "primrec"
  12.183 -    "print_ML_antiquotations"
  12.184 -    "print_abbrevs"
  12.185 -    "print_antiquotations"
  12.186 -    "print_ast_translation"
  12.187 -    "print_attributes"
  12.188 -    "print_binds"
  12.189 -    "print_bnfs"
  12.190 -    "print_bundles"
  12.191 -    "print_case_translations"
  12.192 -    "print_cases"
  12.193 -    "print_claset"
  12.194 -    "print_classes"
  12.195 -    "print_codeproc"
  12.196 -    "print_codesetup"
  12.197 -    "print_coercions"
  12.198 -    "print_commands"
  12.199 -    "print_context"
  12.200 -    "print_defn_rules"
  12.201 -    "print_dependencies"
  12.202 -    "print_facts"
  12.203 -    "print_induct_rules"
  12.204 -    "print_inductives"
  12.205 -    "print_interps"
  12.206 -    "print_locale"
  12.207 -    "print_locales"
  12.208 -    "print_methods"
  12.209 -    "print_options"
  12.210 -    "print_orders"
  12.211 -    "print_quot_maps"
  12.212 -    "print_quotconsts"
  12.213 -    "print_quotients"
  12.214 -    "print_quotientsQ3"
  12.215 -    "print_quotmapsQ3"
  12.216 -    "print_rules"
  12.217 -    "print_simpset"
  12.218 -    "print_state"
  12.219 -    "print_statement"
  12.220 -    "print_syntax"
  12.221 -    "print_term_bindings"
  12.222 -    "print_theorems"
  12.223 -    "print_theory"
  12.224 -    "print_trans_rules"
  12.225 -    "print_translation"
  12.226 -    "proof"
  12.227 -    "prop"
  12.228 -    "qed"
  12.229 -    "quickcheck"
  12.230 -    "quickcheck_generator"
  12.231 -    "quickcheck_params"
  12.232 -    "quit"
  12.233 -    "quotient_definition"
  12.234 -    "quotient_type"
  12.235 -    "realizability"
  12.236 -    "realizers"
  12.237 -    "recdef"
  12.238 -    "recdef_tc"
  12.239 -    "record"
  12.240 -    "refute"
  12.241 -    "refute_params"
  12.242 -    "remove_thy"
  12.243 -    "schematic_corollary"
  12.244 -    "schematic_lemma"
  12.245 -    "schematic_theorem"
  12.246 -    "sect"
  12.247 -    "section"
  12.248 -    "setup"
  12.249 -    "setup_lifting"
  12.250 -    "show"
  12.251 -    "simproc_setup"
  12.252 -    "simps_of_case"
  12.253 -    "sledgehammer"
  12.254 -    "sledgehammer_params"
  12.255 -    "smt_status"
  12.256 -    "solve_direct"
  12.257 -    "sorry"
  12.258 -    "spark_end"
  12.259 -    "spark_open"
  12.260 -    "spark_open_vcg"
  12.261 -    "spark_proof_functions"
  12.262 -    "spark_status"
  12.263 -    "spark_types"
  12.264 -    "spark_vc"
  12.265 -    "specification"
  12.266 -    "statespace"
  12.267 -    "subclass"
  12.268 -    "sublocale"
  12.269 -    "subsect"
  12.270 -    "subsection"
  12.271 -    "subsubsect"
  12.272 -    "subsubsection"
  12.273 -    "syntax"
  12.274 -    "syntax_declaration"
  12.275 -    "term"
  12.276 -    "term_cartouche"
  12.277 -    "termination"
  12.278 -    "test_code"
  12.279 -    "text"
  12.280 -    "text_cartouche"
  12.281 -    "text_raw"
  12.282 -    "then"
  12.283 -    "theorem"
  12.284 -    "theorems"
  12.285 -    "theory"
  12.286 -    "thm"
  12.287 -    "thm_deps"
  12.288 -    "thus"
  12.289 -    "thy_deps"
  12.290 -    "translations"
  12.291 -    "try"
  12.292 -    "try0"
  12.293 -    "txt"
  12.294 -    "txt_raw"
  12.295 -    "typ"
  12.296 -    "type_notation"
  12.297 -    "type_synonym"
  12.298 -    "typed_print_translation"
  12.299 -    "typedecl"
  12.300 -    "typedef"
  12.301 -    "ultimately"
  12.302 -    "undo"
  12.303 -    "undos_proof"
  12.304 -    "unfolding"
  12.305 -    "unused_thms"
  12.306 -    "use_thy"
  12.307 -    "using"
  12.308 -    "value"
  12.309 -    "values"
  12.310 -    "values_prolog"
  12.311 -    "welcome"
  12.312 -    "with"
  12.313 -    "write"
  12.314 -    "{"
  12.315 -    "}"))
  12.316 -
  12.317 -(defconst isar-keywords-minor
  12.318 -  '("and"
  12.319 -    "assumes"
  12.320 -    "attach"
  12.321 -    "avoids"
  12.322 -    "begin"
  12.323 -    "binder"
  12.324 -    "binds"
  12.325 -    "checking"
  12.326 -    "class_instance"
  12.327 -    "class_relation"
  12.328 -    "code_module"
  12.329 -    "congs"
  12.330 -    "constant"
  12.331 -    "constrains"
  12.332 -    "datatypes"
  12.333 -    "defines"
  12.334 -    "defining"
  12.335 -    "file"
  12.336 -    "fixes"
  12.337 -    "for"
  12.338 -    "functions"
  12.339 -    "hints"
  12.340 -    "identifier"
  12.341 -    "if"
  12.342 -    "imports"
  12.343 -    "in"
  12.344 -    "includes"
  12.345 -    "infix"
  12.346 -    "infixl"
  12.347 -    "infixr"
  12.348 -    "is"
  12.349 -    "keywords"
  12.350 -    "lazy"
  12.351 -    "module_name"
  12.352 -    "monos"
  12.353 -    "morphisms"
  12.354 -    "notes"
  12.355 -    "obtains"
  12.356 -    "open"
  12.357 -    "output"
  12.358 -    "overloaded"
  12.359 -    "parametric"
  12.360 -    "permissive"
  12.361 -    "pervasive"
  12.362 -    "shows"
  12.363 -    "structure"
  12.364 -    "type_class"
  12.365 -    "type_constructor"
  12.366 -    "unchecked"
  12.367 -    "unsafe"
  12.368 -    "where"))
  12.369 -
  12.370 -(defconst isar-keywords-control
  12.371 -  '("Isabelle\\.command"
  12.372 -    "ProofGeneral\\.inform_file_processed"
  12.373 -    "ProofGeneral\\.inform_file_retracted"
  12.374 -    "ProofGeneral\\.kill_proof"
  12.375 -    "ProofGeneral\\.pr"
  12.376 -    "ProofGeneral\\.process_pgip"
  12.377 -    "ProofGeneral\\.restart"
  12.378 -    "ProofGeneral\\.undo"
  12.379 -    "cannot_undo"
  12.380 -    "commit"
  12.381 -    "disable_pr"
  12.382 -    "enable_pr"
  12.383 -    "exit"
  12.384 -    "init_toplevel"
  12.385 -    "kill"
  12.386 -    "kill_thy"
  12.387 -    "linear_undo"
  12.388 -    "pretty_setmargin"
  12.389 -    "quit"
  12.390 -    "remove_thy"
  12.391 -    "undo"
  12.392 -    "undos_proof"
  12.393 -    "use_thy"))
  12.394 -
  12.395 -(defconst isar-keywords-diag
  12.396 -  '("ML_command"
  12.397 -    "ML_val"
  12.398 -    "approximate"
  12.399 -    "cartouche"
  12.400 -    "class_deps"
  12.401 -    "code_deps"
  12.402 -    "code_thms"
  12.403 -    "display_drafts"
  12.404 -    "find_consts"
  12.405 -    "find_theorems"
  12.406 -    "find_unused_assms"
  12.407 -    "full_prf"
  12.408 -    "header"
  12.409 -    "help"
  12.410 -    "locale_deps"
  12.411 -    "nitpick"
  12.412 -    "old_smt_status"
  12.413 -    "pr"
  12.414 -    "prf"
  12.415 -    "print_ML_antiquotations"
  12.416 -    "print_abbrevs"
  12.417 -    "print_antiquotations"
  12.418 -    "print_attributes"
  12.419 -    "print_binds"
  12.420 -    "print_bnfs"
  12.421 -    "print_bundles"
  12.422 -    "print_case_translations"
  12.423 -    "print_cases"
  12.424 -    "print_claset"
  12.425 -    "print_classes"
  12.426 -    "print_codeproc"
  12.427 -    "print_codesetup"
  12.428 -    "print_coercions"
  12.429 -    "print_commands"
  12.430 -    "print_context"
  12.431 -    "print_defn_rules"
  12.432 -    "print_dependencies"
  12.433 -    "print_facts"
  12.434 -    "print_induct_rules"
  12.435 -    "print_inductives"
  12.436 -    "print_interps"
  12.437 -    "print_locale"
  12.438 -    "print_locales"
  12.439 -    "print_methods"
  12.440 -    "print_options"
  12.441 -    "print_orders"
  12.442 -    "print_quot_maps"
  12.443 -    "print_quotconsts"
  12.444 -    "print_quotients"
  12.445 -    "print_quotientsQ3"
  12.446 -    "print_quotmapsQ3"
  12.447 -    "print_rules"
  12.448 -    "print_simpset"
  12.449 -    "print_state"
  12.450 -    "print_statement"
  12.451 -    "print_syntax"
  12.452 -    "print_term_bindings"
  12.453 -    "print_theorems"
  12.454 -    "print_theory"
  12.455 -    "print_trans_rules"
  12.456 -    "prop"
  12.457 -    "quickcheck"
  12.458 -    "refute"
  12.459 -    "sledgehammer"
  12.460 -    "smt_status"
  12.461 -    "solve_direct"
  12.462 -    "spark_status"
  12.463 -    "term"
  12.464 -    "term_cartouche"
  12.465 -    "test_code"
  12.466 -    "thm"
  12.467 -    "thm_deps"
  12.468 -    "thy_deps"
  12.469 -    "try"
  12.470 -    "try0"
  12.471 -    "typ"
  12.472 -    "unused_thms"
  12.473 -    "value"
  12.474 -    "values"
  12.475 -    "values_prolog"
  12.476 -    "welcome"))
  12.477 -
  12.478 -(defconst isar-keywords-theory-begin
  12.479 -  '("theory"))
  12.480 -
  12.481 -(defconst isar-keywords-theory-switch
  12.482 -  '())
  12.483 -
  12.484 -(defconst isar-keywords-theory-end
  12.485 -  '("end"))
  12.486 -
  12.487 -(defconst isar-keywords-theory-heading
  12.488 -  '("chapter"
  12.489 -    "section"
  12.490 -    "subsection"
  12.491 -    "subsubsection"))
  12.492 -
  12.493 -(defconst isar-keywords-theory-decl
  12.494 -  '("ML"
  12.495 -    "ML_file"
  12.496 -    "SML_export"
  12.497 -    "SML_file"
  12.498 -    "SML_import"
  12.499 -    "abbreviation"
  12.500 -    "adhoc_overloading"
  12.501 -    "atom_decl"
  12.502 -    "attribute_setup"
  12.503 -    "axiomatization"
  12.504 -    "bnf_axiomatization"
  12.505 -    "boogie_file"
  12.506 -    "bundle"
  12.507 -    "case_of_simps"
  12.508 -    "class"
  12.509 -    "codatatype"
  12.510 -    "code_datatype"
  12.511 -    "code_identifier"
  12.512 -    "code_monad"
  12.513 -    "code_printing"
  12.514 -    "code_reflect"
  12.515 -    "code_reserved"
  12.516 -    "coinductive"
  12.517 -    "coinductive_set"
  12.518 -    "consts"
  12.519 -    "context"
  12.520 -    "datatype"
  12.521 -    "datatype_compat"
  12.522 -    "declaration"
  12.523 -    "declare"
  12.524 -    "default_sort"
  12.525 -    "defer_recdef"
  12.526 -    "definition"
  12.527 -    "defs"
  12.528 -    "domain"
  12.529 -    "domain_isomorphism"
  12.530 -    "domaindef"
  12.531 -    "equivariance"
  12.532 -    "export_code"
  12.533 -    "extract"
  12.534 -    "extract_type"
  12.535 -    "fixrec"
  12.536 -    "fun"
  12.537 -    "fun_cases"
  12.538 -    "hide_class"
  12.539 -    "hide_const"
  12.540 -    "hide_fact"
  12.541 -    "hide_type"
  12.542 -    "import_const_map"
  12.543 -    "import_file"
  12.544 -    "import_tptp"
  12.545 -    "import_type_map"
  12.546 -    "inductive"
  12.547 -    "inductive_cases"
  12.548 -    "inductive_set"
  12.549 -    "inductive_simps"
  12.550 -    "instantiation"
  12.551 -    "judgment"
  12.552 -    "lemmas"
  12.553 -    "lifting_forget"
  12.554 -    "lifting_update"
  12.555 -    "local_setup"
  12.556 -    "locale"
  12.557 -    "method_setup"
  12.558 -    "named_theorems"
  12.559 -    "nitpick_params"
  12.560 -    "no_adhoc_overloading"
  12.561 -    "no_notation"
  12.562 -    "no_syntax"
  12.563 -    "no_translations"
  12.564 -    "no_type_notation"
  12.565 -    "nominal_datatype"
  12.566 -    "nonterminal"
  12.567 -    "notation"
  12.568 -    "notepad"
  12.569 -    "old_datatype"
  12.570 -    "oracle"
  12.571 -    "overloading"
  12.572 -    "parse_ast_translation"
  12.573 -    "parse_translation"
  12.574 -    "partial_function"
  12.575 -    "primcorec"
  12.576 -    "primrec"
  12.577 -    "print_ast_translation"
  12.578 -    "print_translation"
  12.579 -    "quickcheck_generator"
  12.580 -    "quickcheck_params"
  12.581 -    "realizability"
  12.582 -    "realizers"
  12.583 -    "recdef"
  12.584 -    "record"
  12.585 -    "refute_params"
  12.586 -    "setup"
  12.587 -    "setup_lifting"
  12.588 -    "simproc_setup"
  12.589 -    "simps_of_case"
  12.590 -    "sledgehammer_params"
  12.591 -    "spark_end"
  12.592 -    "spark_open"
  12.593 -    "spark_open_vcg"
  12.594 -    "spark_proof_functions"
  12.595 -    "spark_types"
  12.596 -    "statespace"
  12.597 -    "syntax"
  12.598 -    "syntax_declaration"
  12.599 -    "text"
  12.600 -    "text_cartouche"
  12.601 -    "text_raw"
  12.602 -    "theorems"
  12.603 -    "translations"
  12.604 -    "type_notation"
  12.605 -    "type_synonym"
  12.606 -    "typed_print_translation"
  12.607 -    "typedecl"))
  12.608 -
  12.609 -(defconst isar-keywords-theory-script
  12.610 -  '())
  12.611 -
  12.612 -(defconst isar-keywords-theory-goal
  12.613 -  '("bnf"
  12.614 -    "code_pred"
  12.615 -    "corollary"
  12.616 -    "cpodef"
  12.617 -    "free_constructors"
  12.618 -    "function"
  12.619 -    "functor"
  12.620 -    "instance"
  12.621 -    "interpretation"
  12.622 -    "lemma"
  12.623 -    "lift_definition"
  12.624 -    "nominal_function"
  12.625 -    "nominal_inductive"
  12.626 -    "nominal_inductive2"
  12.627 -    "nominal_primrec"
  12.628 -    "nominal_termination"
  12.629 -    "old_rep_datatype"
  12.630 -    "pcpodef"
  12.631 -    "permanent_interpretation"
  12.632 -    "primcorecursive"
  12.633 -    "quotient_definition"
  12.634 -    "quotient_type"
  12.635 -    "recdef_tc"
  12.636 -    "schematic_corollary"
  12.637 -    "schematic_lemma"
  12.638 -    "schematic_theorem"
  12.639 -    "spark_vc"
  12.640 -    "specification"
  12.641 -    "subclass"
  12.642 -    "sublocale"
  12.643 -    "termination"
  12.644 -    "theorem"
  12.645 -    "typedef"))
  12.646 -
  12.647 -(defconst isar-keywords-qed
  12.648 -  '("\\."
  12.649 -    "\\.\\."
  12.650 -    "by"
  12.651 -    "done"
  12.652 -    "sorry"))
  12.653 -
  12.654 -(defconst isar-keywords-qed-block
  12.655 -  '("qed"))
  12.656 -
  12.657 -(defconst isar-keywords-qed-global
  12.658 -  '("oops"))
  12.659 -
  12.660 -(defconst isar-keywords-proof-heading
  12.661 -  '("sect"
  12.662 -    "subsect"
  12.663 -    "subsubsect"))
  12.664 -
  12.665 -(defconst isar-keywords-proof-goal
  12.666 -  '("have"
  12.667 -    "hence"
  12.668 -    "interpret"))
  12.669 -
  12.670 -(defconst isar-keywords-proof-block
  12.671 -  '("next"
  12.672 -    "proof"))
  12.673 -
  12.674 -(defconst isar-keywords-proof-open
  12.675 -  '("{"))
  12.676 -
  12.677 -(defconst isar-keywords-proof-close
  12.678 -  '("}"))
  12.679 -
  12.680 -(defconst isar-keywords-proof-chain
  12.681 -  '("finally"
  12.682 -    "from"
  12.683 -    "then"
  12.684 -    "ultimately"
  12.685 -    "with"))
  12.686 -
  12.687 -(defconst isar-keywords-proof-decl
  12.688 -  '("ML_prf"
  12.689 -    "also"
  12.690 -    "include"
  12.691 -    "including"
  12.692 -    "let"
  12.693 -    "moreover"
  12.694 -    "note"
  12.695 -    "txt"
  12.696 -    "txt_raw"
  12.697 -    "unfolding"
  12.698 -    "using"
  12.699 -    "write"))
  12.700 -
  12.701 -(defconst isar-keywords-proof-asm
  12.702 -  '("assume"
  12.703 -    "case"
  12.704 -    "def"
  12.705 -    "fix"
  12.706 -    "presume"))
  12.707 -
  12.708 -(defconst isar-keywords-proof-asm-goal
  12.709 -  '("guess"
  12.710 -    "obtain"
  12.711 -    "show"
  12.712 -    "thus"))
  12.713 -
  12.714 -(defconst isar-keywords-proof-script
  12.715 -  '("apply"
  12.716 -    "apply_end"
  12.717 -    "back"
  12.718 -    "defer"
  12.719 -    "prefer"))
  12.720 -
  12.721 -(provide 'isar-keywords)
    13.1 --- a/lib/Tools/keywords	Thu Oct 30 23:14:11 2014 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,60 +0,0 @@
    13.4 -#!/usr/bin/env bash
    13.5 -#
    13.6 -# Author: Makarius
    13.7 -#
    13.8 -# DESCRIPTION: generate keyword files for Emacs Proof General
    13.9 -
   13.10 -
   13.11 -## diagnostics
   13.12 -
   13.13 -PRG="$(basename "$0")"
   13.14 -
   13.15 -function usage()
   13.16 -{
   13.17 -  echo
   13.18 -  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
   13.19 -  echo
   13.20 -  echo "  Options are:"
   13.21 -  echo "    -d DIR       include session directory"
   13.22 -  echo "    -k NAME      specific name of keywords collection (default: empty)"
   13.23 -  echo
   13.24 -  echo "  Generate keyword files for Emacs Proof General from Isabelle sessions."
   13.25 -  echo
   13.26 -  exit 1
   13.27 -}
   13.28 -
   13.29 -
   13.30 -## process command line
   13.31 -
   13.32 -# options
   13.33 -
   13.34 -declare -a DIRS=()
   13.35 -KEYWORDS_NAME=""
   13.36 -
   13.37 -while getopts "d:k:" OPT
   13.38 -do
   13.39 -  case "$OPT" in
   13.40 -    d)
   13.41 -      DIRS["${#DIRS[@]}"]="$OPTARG"
   13.42 -      ;;
   13.43 -    k)
   13.44 -      KEYWORDS_NAME="$OPTARG"
   13.45 -      ;;
   13.46 -    \?)
   13.47 -      usage
   13.48 -      ;;
   13.49 -  esac
   13.50 -done
   13.51 -
   13.52 -shift $(($OPTIND - 1))
   13.53 -
   13.54 -
   13.55 -## main
   13.56 -
   13.57 -isabelle_admin_build jars || exit $?
   13.58 -
   13.59 -declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
   13.60 -
   13.61 -"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords keywords \
   13.62 -  "$KEYWORDS_NAME" "${DIRS[@]}" $'\n' "$@"
   13.63 -
    14.1 --- a/src/Doc/Classes/Classes.thy	Thu Oct 30 23:14:11 2014 +0100
    14.2 +++ b/src/Doc/Classes/Classes.thy	Fri Oct 31 11:18:17 2014 +0100
    14.3 @@ -179,8 +179,7 @@
    14.4    primrec declaration; by default, the local name of a class operation
    14.5    @{text f} to be instantiated on type constructor @{text \<kappa>} is
    14.6    mangled as @{text f_\<kappa>}.  In case of uncertainty, these names may be
    14.7 -  inspected using the @{command "print_context"} command or the
    14.8 -  corresponding ProofGeneral button.
    14.9 +  inspected using the @{command "print_context"} command.
   14.10  *}
   14.11  
   14.12  subsection {* Lifting and parametric types *}
    15.1 --- a/src/Doc/Implementation/ML.thy	Thu Oct 30 23:14:11 2014 +0100
    15.2 +++ b/src/Doc/Implementation/ML.thy	Fri Oct 31 11:18:17 2014 +0100
    15.3 @@ -1056,9 +1056,7 @@
    15.4  
    15.5    \begin{warn}
    15.6    The actual error channel is accessed via @{ML Output.error_message}, but
    15.7 -  the old interaction protocol of Proof~General \emph{crashes} if that
    15.8 -  function is used in regular ML code: error output and toplevel
    15.9 -  command failure always need to coincide in classic TTY interaction.
   15.10 +  this is normally not used directly in user code.
   15.11    \end{warn}
   15.12  
   15.13    \end{description}
    16.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Thu Oct 30 23:14:11 2014 +0100
    16.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Oct 31 11:18:17 2014 +0100
    16.3 @@ -151,8 +151,7 @@
    16.4    and sort constraints.  This enables Prover IDE users to retrieve
    16.5    that information via tooltips or popups while hovering with the
    16.6    mouse over the output window, for example.  Consequently, this
    16.7 -  option is enabled by default for Isabelle/jEdit, but disabled for
    16.8 -  TTY and Proof~General~/Emacs where document markup would not work.
    16.9 +  option is enabled by default for Isabelle/jEdit.
   16.10  
   16.11    \item @{attribute show_types} and @{attribute show_sorts} control
   16.12    printing of type constraints for term variables, and sort
   16.13 @@ -274,12 +273,6 @@
   16.14  
   16.15    \end{description}
   16.16  
   16.17 -  \begin{warn}
   16.18 -  The old global reference @{ML print_mode} should never be used
   16.19 -  directly in applications.  Its main reason for being publicly
   16.20 -  accessible is to support historic versions of Proof~General.
   16.21 -  \end{warn}
   16.22 -
   16.23    \medskip The pretty printer for inner syntax maintains alternative
   16.24    mixfix productions for any print mode name invented by the user, say
   16.25    in commands like @{command notation} or @{command abbreviation}.
   16.26 @@ -299,9 +292,7 @@
   16.27  
   16.28    \item @{verbatim xsymbols}: enable proper mathematical symbols
   16.29    instead of ASCII art.\footnote{This traditional mode name stems from
   16.30 -  the ``X-Symbol'' package for old versions Proof~General with XEmacs,
   16.31 -  although that package has been superseded by Unicode in recent
   16.32 -  years.}
   16.33 +  the ``X-Symbol'' package for classic Proof~General with XEmacs.}
   16.34  
   16.35    \item @{verbatim HTML}: additional mode that is active in HTML
   16.36    presentation of Isabelle theory sources; allows to provide
    17.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Thu Oct 30 23:14:11 2014 +0100
    17.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Oct 31 11:18:17 2014 +0100
    17.3 @@ -42,25 +42,10 @@
    17.4    next command keyword.
    17.5  
    17.6    More advanced interfaces such as Isabelle/jEdit @{cite "Wenzel:2012"}
    17.7 -  and Proof~General @{cite proofgeneral} do not require explicit
    17.8 -  semicolons: command spans are determined by inspecting the content
    17.9 -  of the editor buffer.  In the printed presentation of Isabelle/Isar
   17.10 -  documents semicolons are omitted altogether for readability.
   17.11 -
   17.12 -  \begin{warn}
   17.13 -    Proof~General requires certain syntax classification tables in
   17.14 -    order to achieve properly synchronized interaction with the
   17.15 -    Isabelle/Isar process.  These tables need to be consistent with
   17.16 -    the Isabelle version and particular logic image to be used in a
   17.17 -    running session (common object-logics may well change the outer
   17.18 -    syntax).  The standard setup should work correctly with any of the
   17.19 -    ``official'' logic images derived from Isabelle/HOL (including
   17.20 -    HOLCF etc.).  Users of alternative logics may need to tell
   17.21 -    Proof~General explicitly, e.g.\ by giving an option @{verbatim "-k ZF"}
   17.22 -    (in conjunction with @{verbatim "-l ZF"}, to specify the default
   17.23 -    logic image).  Note that option @{verbatim "-L"} does both
   17.24 -    of this at the same time.
   17.25 -  \end{warn}
   17.26 +  do not require explicit semicolons: command spans are determined by
   17.27 +  inspecting the content of the editor buffer.  In the printed
   17.28 +  presentation of Isabelle/Isar documents semicolons are omitted
   17.29 +  altogether for readability.
   17.30  \<close>
   17.31  
   17.32  
   17.33 @@ -205,7 +190,7 @@
   17.34    Common mathematical symbols such as @{text \<forall>} are represented in
   17.35    Isabelle as @{verbatim \<forall>}.  There are infinitely many Isabelle
   17.36    symbols like this, although proper presentation is left to front-end
   17.37 -  tools such as {\LaTeX}, Proof~General, or Isabelle/jEdit.  A list of
   17.38 +  tools such as {\LaTeX} or Isabelle/jEdit.  A list of
   17.39    predefined Isabelle symbols that work well with these tools is given
   17.40    in \appref{app:symbols}.  Note that @{verbatim "\<lambda>"} does not belong
   17.41    to the @{text letter} category, since it is already used differently
    18.1 --- a/src/Doc/System/Basics.thy	Thu Oct 30 23:14:11 2014 +0100
    18.2 +++ b/src/Doc/System/Basics.thy	Fri Oct 31 11:18:17 2014 +0100
    18.3 @@ -363,7 +363,6 @@
    18.4    Options are:
    18.5      -I           startup Isar interaction mode
    18.6      -O           system options from given YXML file
    18.7 -    -P           startup Proof General interaction mode
    18.8      -S           secure mode -- disallow critical operations
    18.9      -T ADDR      startup process wrapper, with socket address
   18.10      -W IN:OUT    startup process wrapper, with input/output fifos
   18.11 @@ -437,8 +436,6 @@
   18.12  
   18.13    \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
   18.14    interaction mode on startup, instead of the primitive ML top-level.
   18.15 -  The @{verbatim "-P"} option configures the top-level loop for
   18.16 -  interaction with the Proof General user interface.
   18.17  
   18.18    \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
   18.19    Isabelle enter a special process wrapper for interaction via
    19.1 --- a/src/Doc/Tutorial/Documents/Documents.thy	Thu Oct 30 23:14:11 2014 +0100
    19.2 +++ b/src/Doc/Tutorial/Documents/Documents.thy	Fri Oct 31 11:18:17 2014 +0100
    19.3 @@ -102,9 +102,8 @@
    19.4    Here $ident$ is any sequence of letters. 
    19.5    This results in an infinite store of symbols, whose
    19.6    interpretation is left to further front-end tools.  For example, the
    19.7 -  user-interface of Proof~General + X-Symbol and the Isabelle document
    19.8 -  processor (see \S\ref{sec:document-preparation}) display the
    19.9 -  \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
   19.10 +  Isabelle document processor (see \S\ref{sec:document-preparation})
   19.11 +  display the \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
   19.12  
   19.13    A list of standard Isabelle symbols is given in
   19.14    @{cite "isabelle-isar-ref"}.  You may introduce your own
   19.15 @@ -147,12 +146,7 @@
   19.16  (*>*)
   19.17  
   19.18  text {*
   19.19 -  \noindent Proof~General provides several input methods to enter
   19.20 -  @{text \<oplus>} in the text.  If all fails one may just type a named
   19.21 -  entity \verb,\,\verb,<oplus>, by hand; the corresponding symbol will
   19.22 -  be displayed after further input.
   19.23 -
   19.24 -  More flexible is to provide alternative syntax forms
   19.25 +  It is possible to provide alternative syntax forms
   19.26    through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}.  By
   19.27    convention, the mode of ``$xsymbols$'' is enabled whenever
   19.28    Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
    20.1 --- a/src/Doc/Tutorial/Types/Overloading.thy	Thu Oct 30 23:14:11 2014 +0100
    20.2 +++ b/src/Doc/Tutorial/Types/Overloading.thy	Fri Oct 31 11:18:17 2014 +0100
    20.3 @@ -37,8 +37,7 @@
    20.4  suffix @{text "_nat"}; by default, the local name of a class operation
    20.5  @{text f} to be instantiated on type constructor @{text \<kappa>} is mangled
    20.6  as @{text f_\<kappa>}.  In case of uncertainty, these names may be inspected
    20.7 -using the @{command "print_context"} command or the corresponding
    20.8 -ProofGeneral button.
    20.9 +using the @{command "print_context"} command.
   20.10  
   20.11  Although class @{class [source] plus} has no axioms, the instantiation must be
   20.12  formally concluded by a (trivial) instantiation proof ``..'': *}
    21.1 --- a/src/HOL/ROOT	Thu Oct 30 23:14:11 2014 +0100
    21.2 +++ b/src/HOL/ROOT	Fri Oct 31 11:18:17 2014 +0100
    21.3 @@ -600,7 +600,6 @@
    21.4      Simps_Case_Conv_Examples
    21.5      ML
    21.6      SAT_Examples
    21.7 -    Nominal2_Dummy
    21.8      SOS
    21.9      SOS_Cert
   21.10    theories [skip_proofs = false]
    22.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Thu Oct 30 23:14:11 2014 +0100
    22.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Fri Oct 31 11:18:17 2014 +0100
    22.3 @@ -31,13 +31,6 @@
    22.4     its time slot with several other automatic tools. *)
    22.5  val auto_try_max_scopes = 6
    22.6  
    22.7 -val _ =
    22.8 -  ProofGeneral.preference_option ProofGeneral.category_tracing
    22.9 -    NONE
   22.10 -    @{system_option auto_nitpick}
   22.11 -    "auto-nitpick"
   22.12 -    "Run Nitpick automatically"
   22.13 -
   22.14  type raw_param = string * string list
   22.15  
   22.16  val default_default_params =
    23.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Oct 30 23:14:11 2014 +0100
    23.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Oct 31 11:18:17 2014 +0100
    23.3 @@ -38,13 +38,6 @@
    23.4  val running_learnersN = "running_learners"
    23.5  val refresh_tptpN = "refresh_tptp"
    23.6  
    23.7 -val _ =
    23.8 -  ProofGeneral.preference_option ProofGeneral.category_tracing
    23.9 -    NONE
   23.10 -    @{system_option auto_sledgehammer}
   23.11 -    "auto-sledgehammer"
   23.12 -    "Run Sledgehammer automatically"
   23.13 -
   23.14  (** Sledgehammer commands **)
   23.15  
   23.16  fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
   23.17 @@ -58,20 +51,6 @@
   23.18  
   23.19  val provers = Unsynchronized.ref ""
   23.20  
   23.21 -val _ =
   23.22 -  ProofGeneral.preference_string ProofGeneral.category_proof
   23.23 -    NONE
   23.24 -    provers
   23.25 -    "Sledgehammer: Provers"
   23.26 -    "Default automatic provers (separated by whitespace)"
   23.27 -
   23.28 -val _ =
   23.29 -  ProofGeneral.preference_option ProofGeneral.category_proof
   23.30 -    NONE
   23.31 -    @{system_option sledgehammer_timeout}
   23.32 -    "Sledgehammer: Time Limit"
   23.33 -    "ATPs will be interrupted after this time (in seconds)"
   23.34 -
   23.35  type raw_param = string * string list
   23.36  
   23.37  val default_default_params =
    24.1 --- a/src/HOL/Tools/try0.ML	Thu Oct 30 23:14:11 2014 +0100
    24.2 +++ b/src/HOL/Tools/try0.ML	Fri Oct 31 11:18:17 2014 +0100
    24.3 @@ -22,13 +22,6 @@
    24.4  
    24.5  datatype mode = Auto_Try | Try | Normal;
    24.6  
    24.7 -val _ =
    24.8 -  ProofGeneral.preference_option ProofGeneral.category_tracing
    24.9 -    NONE
   24.10 -    @{system_option auto_methods}
   24.11 -    "auto-try0"
   24.12 -    "Try standard proof methods";
   24.13 -
   24.14  val default_timeout = seconds 5.0;
   24.15  
   24.16  fun can_apply timeout_opt pre post tac st =
    25.1 --- a/src/HOL/ex/Nominal2_Dummy.thy	Thu Oct 30 23:14:11 2014 +0100
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,22 +0,0 @@
    25.4 -header \<open>Dummy theory to anticipate AFP/Nominal2 keywords\<close>  (* Proof General legacy *)
    25.5 -
    25.6 -theory Nominal2_Dummy
    25.7 -imports Main
    25.8 -keywords
    25.9 -  "nominal_datatype" :: thy_decl and
   25.10 -  "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and
   25.11 -  "atom_decl" "equivariance" :: thy_decl and
   25.12 -  "avoids" "binds"
   25.13 -begin
   25.14 -
   25.15 -ML \<open>
   25.16 -Outer_Syntax.command @{command_spec "nominal_datatype"} "dummy" Scan.fail;
   25.17 -Outer_Syntax.command @{command_spec "nominal_function"} "dummy" Scan.fail;
   25.18 -Outer_Syntax.command @{command_spec "nominal_inductive"} "dummy" Scan.fail;
   25.19 -Outer_Syntax.command @{command_spec "nominal_termination"} "dummy" Scan.fail;
   25.20 -Outer_Syntax.command @{command_spec "atom_decl"} "dummy" Scan.fail;
   25.21 -Outer_Syntax.command @{command_spec "equivariance"} "dummy" Scan.fail;
   25.22 -\<close>
   25.23 -
   25.24 -end
   25.25 -
    26.1 --- a/src/Pure/General/secure.ML	Thu Oct 30 23:14:11 2014 +0100
    26.2 +++ b/src/Pure/General/secure.ML	Fri Oct 31 11:18:17 2014 +0100
    26.3 @@ -13,7 +13,6 @@
    26.4    val use_text: use_context -> int * string -> bool -> string -> unit
    26.5    val use_file: use_context -> bool -> string -> unit
    26.6    val toplevel_pp: string list -> string -> unit
    26.7 -  val PG_setup: unit -> unit
    26.8    val commit: unit -> unit
    26.9  end;
   26.10  
   26.11 @@ -53,8 +52,5 @@
   26.12  
   26.13  fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
   26.14  
   26.15 -fun PG_setup () =
   26.16 -  use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
   26.17 -
   26.18  end;
   26.19  
    27.1 --- a/src/Pure/Pure.thy	Thu Oct 30 23:14:11 2014 +0100
    27.2 +++ b/src/Pure/Pure.thy	Fri Oct 31 11:18:17 2014 +0100
    27.3 @@ -100,9 +100,6 @@
    27.4    and "extract_type" "extract" :: thy_decl
    27.5    and "find_theorems" "find_consts" :: diag
    27.6    and "named_theorems" :: thy_decl
    27.7 -  and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
    27.8 -    "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"
    27.9 -    "ProofGeneral.inform_file_retracted" :: control
   27.10  begin
   27.11  
   27.12  ML_file "ML/ml_antiquotations.ML"
   27.13 @@ -117,7 +114,6 @@
   27.14  ML_file "Tools/class_deps.ML"
   27.15  ML_file "Tools/find_theorems.ML"
   27.16  ML_file "Tools/find_consts.ML"
   27.17 -ML_file "Tools/proof_general_pure.ML"
   27.18  ML_file "Tools/simplifier_trace.ML"
   27.19  ML_file "Tools/named_theorems.ML"
   27.20  
    28.1 --- a/src/Pure/ROOT	Thu Oct 30 23:14:11 2014 +0100
    28.2 +++ b/src/Pure/ROOT	Fri Oct 31 11:18:17 2014 +0100
    28.3 @@ -211,7 +211,6 @@
    28.4      "Tools/build.ML"
    28.5      "Tools/named_thms.ML"
    28.6      "Tools/plugin.ML"
    28.7 -    "Tools/proof_general.ML"
    28.8      "assumption.ML"
    28.9      "axclass.ML"
   28.10      "config.ML"
    29.1 --- a/src/Pure/ROOT.ML	Thu Oct 30 23:14:11 2014 +0100
    29.2 +++ b/src/Pure/ROOT.ML	Fri Oct 31 11:18:17 2014 +0100
    29.3 @@ -334,7 +334,6 @@
    29.4  
    29.5  use "Tools/build.ML";
    29.6  use "Tools/named_thms.ML";
    29.7 -use "Tools/proof_general.ML";
    29.8  
    29.9  structure Output: OUTPUT = Output;  (*seal system channels!*)
   29.10  
    30.1 --- a/src/Pure/Tools/keywords.scala	Thu Oct 30 23:14:11 2014 +0100
    30.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.3 @@ -1,179 +0,0 @@
    30.4 -/*  Title:      Pure/Tools/keywords.scala
    30.5 -    Author:     Makarius
    30.6 -
    30.7 -Generate keyword files for Emacs Proof General.
    30.8 -*/
    30.9 -
   30.10 -/*Proof General legacy*/
   30.11 -
   30.12 -package isabelle
   30.13 -
   30.14 -
   30.15 -import scala.collection.mutable
   30.16 -
   30.17 -
   30.18 -object Keywords
   30.19 -{
   30.20 -  /* keywords */
   30.21 -
   30.22 -  private val convert = Map(
   30.23 -    "thy_begin" -> "theory-begin",
   30.24 -    "thy_end" -> "theory-end",
   30.25 -    "thy_heading1" -> "theory-heading",
   30.26 -    "thy_heading2" -> "theory-heading",
   30.27 -    "thy_heading3" -> "theory-heading",
   30.28 -    "thy_heading4" -> "theory-heading",
   30.29 -    "thy_load" -> "theory-decl",
   30.30 -    "thy_decl" -> "theory-decl",
   30.31 -    "thy_decl_block" -> "theory-decl",
   30.32 -    "thy_goal" -> "theory-goal",
   30.33 -    "qed_script" -> "qed",
   30.34 -    "qed_block" -> "qed-block",
   30.35 -    "qed_global" -> "qed-global",
   30.36 -    "prf_heading2" -> "proof-heading",
   30.37 -    "prf_heading3" -> "proof-heading",
   30.38 -    "prf_heading4" -> "proof-heading",
   30.39 -    "prf_goal" -> "proof-goal",
   30.40 -    "prf_block" -> "proof-block",
   30.41 -    "prf_open" -> "proof-open",
   30.42 -    "prf_close" -> "proof-close",
   30.43 -    "prf_chain" -> "proof-chain",
   30.44 -    "prf_decl" -> "proof-decl",
   30.45 -    "prf_asm" -> "proof-asm",
   30.46 -    "prf_asm_goal" -> "proof-asm-goal",
   30.47 -    "prf_asm_goal_script" -> "proof-asm-goal",
   30.48 -    "prf_script" -> "proof-script"
   30.49 -  ).withDefault((s: String) => s)
   30.50 -
   30.51 -  private val emacs_kinds = List(
   30.52 -    "major",
   30.53 -    "minor",
   30.54 -    "control",
   30.55 -    "diag",
   30.56 -    "theory-begin",
   30.57 -    "theory-switch",
   30.58 -    "theory-end",
   30.59 -    "theory-heading",
   30.60 -    "theory-decl",
   30.61 -    "theory-script",
   30.62 -    "theory-goal",
   30.63 -    "qed",
   30.64 -    "qed-block",
   30.65 -    "qed-global",
   30.66 -    "proof-heading",
   30.67 -    "proof-goal",
   30.68 -    "proof-block",
   30.69 -    "proof-open",
   30.70 -    "proof-close",
   30.71 -    "proof-chain",
   30.72 -    "proof-decl",
   30.73 -    "proof-asm",
   30.74 -    "proof-asm-goal",
   30.75 -    "proof-script")
   30.76 -
   30.77 -  def keywords(
   30.78 -    options: Options,
   30.79 -    name: String = "",
   30.80 -    dirs: List[Path] = Nil,
   30.81 -    sessions: List[String] = Nil)
   30.82 -  {
   30.83 -    val relevant_sessions =
   30.84 -      for {
   30.85 -        (name, content) <-
   30.86 -          Build.session_dependencies(options, false, dirs, sessions).deps.toList
   30.87 -        keywords = content.keywords
   30.88 -        if !keywords.isEmpty
   30.89 -      } yield (name, keywords)
   30.90 -
   30.91 -    val keywords_raw =
   30.92 -      (Map.empty[String, Set[String]].withDefaultValue(Set.empty) /: relevant_sessions) {
   30.93 -        case (map, (_, ks)) =>
   30.94 -          (map /: ks) {
   30.95 -            case (m, (name, Some(((kind, _), _)), _)) =>
   30.96 -              m + (name -> (m(name) + convert(kind)))
   30.97 -            case (m, (name, None, _)) =>
   30.98 -              m + (name -> (m(name) + "minor"))
   30.99 -          }
  30.100 -      }
  30.101 -
  30.102 -    val keywords_unique =
  30.103 -      for ((name, kinds) <- keywords_raw) yield {
  30.104 -        kinds.toList match {
  30.105 -          case List(kind) => (name, kind)
  30.106 -          case _ =>
  30.107 -            (kinds - "minor").toList match {
  30.108 -              case List(kind) => (name, kind)
  30.109 -              case _ =>
  30.110 -                error("Inconsistent declaration of keyword " + quote(name) + ": " +
  30.111 -                  kinds.toList.sorted.mkString(" vs "))
  30.112 -            }
  30.113 -        }
  30.114 -      }
  30.115 -
  30.116 -    val output =
  30.117 -    {
  30.118 -      val out = new mutable.StringBuilder
  30.119 -
  30.120 -      out ++= ";;\n"
  30.121 -      out ++= ";; Keyword classification tables for Isabelle/Isar.\n"
  30.122 -      out ++= ";; Generated from " + relevant_sessions.map(_._1).sorted.mkString(" + ") + ".\n"
  30.123 -      out ++= ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"
  30.124 -      out ++= ";;\n"
  30.125 -
  30.126 -      for (kind <- emacs_kinds) {
  30.127 -        val names =
  30.128 -          (for {
  30.129 -            (name, k) <- keywords_unique.iterator
  30.130 -            if (if (kind == "major") k != "minor" else k == kind)
  30.131 -            if kind != "minor" || Symbol.is_ascii_identifier(name)
  30.132 -          } yield name).toList.sorted
  30.133 -
  30.134 -        out ++= "\n(defconst isar-keywords-" + kind
  30.135 -        out ++= "\n  '("
  30.136 -        out ++=
  30.137 -          names.map(name => quote("""[\.\*\+\?\[\]\^\$]""".r replaceAllIn (name, """\\\\$0""")))
  30.138 -            .mkString("\n    ")
  30.139 -        out ++= "))\n"
  30.140 -      }
  30.141 -
  30.142 -      out ++= "\n(provide 'isar-keywords)\n"
  30.143 -
  30.144 -      out.toString
  30.145 -    }
  30.146 -
  30.147 -    val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el"
  30.148 -    Output.writeln(file)
  30.149 -    File.write(Path.explode(file), output)
  30.150 -  }
  30.151 -
  30.152 -
  30.153 -  /* administrative update_keywords */
  30.154 -
  30.155 -  def update_keywords(options: Options)
  30.156 -  {
  30.157 -    val tree = Build.find_sessions(options)
  30.158 -
  30.159 -    def chapter(ch: String): List[String] =
  30.160 -      for ((name, info) <- tree.topological_order if info.chapter == ch) yield name
  30.161 -
  30.162 -    keywords(options, sessions = chapter("HOL"))
  30.163 -    keywords(options, name = "ZF", sessions = chapter("ZF"))
  30.164 -  }
  30.165 -
  30.166 -
  30.167 -  /* command line entry point */
  30.168 -
  30.169 -  def main(args: Array[String])
  30.170 -  {
  30.171 -    Command_Line.tool0 {
  30.172 -      args.toList match {
  30.173 -        case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) =>
  30.174 -          keywords(Options.init(), name, dirs.map(Path.explode), sessions)
  30.175 -        case "update_keywords" :: Nil =>
  30.176 -          update_keywords(Options.init())
  30.177 -        case _ => error("Bad arguments:\n" + cat_lines(args))
  30.178 -      }
  30.179 -    }
  30.180 -  }
  30.181 -}
  30.182 -
    31.1 --- a/src/Pure/Tools/proof_general.ML	Thu Oct 30 23:14:11 2014 +0100
    31.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.3 @@ -1,443 +0,0 @@
    31.4 -(*  Title:      Pure/Tools/proof_general.ML
    31.5 -    Author:     David Aspinall
    31.6 -    Author:     Makarius
    31.7 -
    31.8 -Isabelle/Isar configuration for Proof General / Emacs.
    31.9 -See also http://proofgeneral.inf.ed.ac.uk
   31.10 -*)
   31.11 -
   31.12 -(*Proof General legacy*)
   31.13 -
   31.14 -signature PROOF_GENERAL =
   31.15 -sig
   31.16 -  type category = string
   31.17 -  val category_display: category
   31.18 -  val category_advanced_display: category
   31.19 -  val category_tracing: category
   31.20 -  val category_proof: category
   31.21 -  type pgiptype = string
   31.22 -  val pgipbool: pgiptype
   31.23 -  val pgipint: pgiptype
   31.24 -  val pgipfloat: pgiptype
   31.25 -  val pgipstring: pgiptype
   31.26 -  val preference: category -> string option ->
   31.27 -    (unit -> string) -> (string -> unit) -> string -> string -> string -> unit
   31.28 -  val preference_bool: category -> string option ->
   31.29 -    bool Unsynchronized.ref -> string -> string -> unit
   31.30 -  val preference_int: category -> string option ->
   31.31 -    int Unsynchronized.ref -> string -> string -> unit
   31.32 -  val preference_real: category -> string option ->
   31.33 -    real Unsynchronized.ref -> string -> string -> unit
   31.34 -  val preference_string: category -> string option ->
   31.35 -    string Unsynchronized.ref -> string -> string -> unit
   31.36 -  val preference_option: category -> string option -> string -> string -> string -> unit
   31.37 -  val process_pgip: string -> unit
   31.38 -  val tell_clear_goals: unit -> unit
   31.39 -  val tell_clear_response: unit -> unit
   31.40 -  val inform_file_processed: string -> unit
   31.41 -  val inform_file_retracted: string -> unit
   31.42 -  val master_path: Path.T Unsynchronized.ref
   31.43 -  structure ThyLoad: sig val add_path: string -> unit end
   31.44 -  val thm_deps: bool Unsynchronized.ref
   31.45 -  val proof_generalN: string
   31.46 -  val init: unit -> unit
   31.47 -  val restart: unit -> unit
   31.48 -end;
   31.49 -
   31.50 -structure ProofGeneral: PROOF_GENERAL =
   31.51 -struct
   31.52 -
   31.53 -(** preferences **)
   31.54 -
   31.55 -(* type preference *)
   31.56 -
   31.57 -type category = string;
   31.58 -val category_display = "Display";
   31.59 -val category_advanced_display = "Advanced Display";
   31.60 -val category_tracing = "Tracing";
   31.61 -val category_proof = "Proof";
   31.62 -
   31.63 -type pgiptype = string;
   31.64 -val pgipbool = "pgipbool";
   31.65 -val pgipint = "pgipint";
   31.66 -val pgipfloat = "pgipint";  (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*)
   31.67 -val pgipstring = "pgipstring";
   31.68 -
   31.69 -type preference =
   31.70 - {category: string,
   31.71 -  override: string option,
   31.72 -  descr: string,
   31.73 -  pgiptype: pgiptype,
   31.74 -  get: unit -> string,
   31.75 -  set: string -> unit};
   31.76 -
   31.77 -
   31.78 -(* global preferences *)
   31.79 -
   31.80 -local
   31.81 -  val preferences =
   31.82 -    Synchronized.var "ProofGeneral.preferences" ([]: (string * preference) list);
   31.83 -in
   31.84 -
   31.85 -fun add_preference name pref =
   31.86 -  Synchronized.change preferences (fn prefs =>
   31.87 -   (if not (AList.defined (op =) prefs name) then ()
   31.88 -    else warning ("Redefining ProofGeneral preference: " ^ quote name);
   31.89 -    AList.update (op =) (name, pref) prefs));
   31.90 -
   31.91 -fun set_preference name value =
   31.92 -  (case AList.lookup (op =) (Synchronized.value preferences) name of
   31.93 -    SOME {set, ...} => set value
   31.94 -  | NONE => error ("Unknown ProofGeneral preference: " ^ quote name));
   31.95 -
   31.96 -fun all_preferences () =
   31.97 -  rev (Synchronized.value preferences)
   31.98 -  |> map (fn (name, {category, descr, pgiptype, get, ...}) =>
   31.99 -    (category, {name = name, descr = descr, default = get (), pgiptype = pgiptype}))
  31.100 -  |> AList.group (op =);
  31.101 -
  31.102 -fun init_preferences () =
  31.103 -  Synchronized.value preferences
  31.104 -  |> List.app (fn (_, {set, override = SOME value, ...}) => set value | _ => ());
  31.105 -
  31.106 -end;
  31.107 -
  31.108 -
  31.109 -
  31.110 -(* raw preferences *)
  31.111 -
  31.112 -fun preference category override get set typ name descr =
  31.113 -  add_preference name
  31.114 -    {category = category, override = override, descr = descr, pgiptype = typ, get = get, set = set};
  31.115 -
  31.116 -fun preference_ref category override read write typ r =
  31.117 -  preference category override (fn () => read (! r)) (fn x => r := write x) typ;
  31.118 -
  31.119 -fun preference_bool x y = preference_ref x y Markup.print_bool Markup.parse_bool pgipbool;
  31.120 -fun preference_int x y = preference_ref x y Markup.print_int Markup.parse_int pgipint;
  31.121 -fun preference_real x y = preference_ref x y Markup.print_real Markup.parse_real pgipfloat;
  31.122 -fun preference_string x y = preference_ref x y I I pgipstring;
  31.123 -
  31.124 -
  31.125 -(* system options *)
  31.126 -
  31.127 -fun preference_option category override option_name pgip_name descr =
  31.128 -  let
  31.129 -    val typ = Options.default_typ option_name;
  31.130 -    val pgiptype =
  31.131 -      if typ = Options.boolT then pgipbool
  31.132 -      else if typ = Options.intT then pgipint
  31.133 -      else if typ = Options.realT then pgipfloat
  31.134 -      else pgipstring;
  31.135 -  in
  31.136 -    add_preference pgip_name
  31.137 -     {category = category,
  31.138 -      override = override,
  31.139 -      descr = descr,
  31.140 -      pgiptype = pgiptype,
  31.141 -      get = fn () => Options.get_default option_name,
  31.142 -      set = Options.put_default option_name}
  31.143 -  end;
  31.144 -
  31.145 -
  31.146 -(* minimal PGIP support for <askprefs>, <haspref>, <setpref> *)
  31.147 -
  31.148 -local
  31.149 -
  31.150 -fun get_attr attrs name =
  31.151 -  (case Properties.get attrs name of
  31.152 -    SOME value => value
  31.153 -  | NONE => raise Fail ("Missing attribute: " ^ quote name));
  31.154 -
  31.155 -fun attr x y = [(x, y)] : XML.attributes;
  31.156 -
  31.157 -fun opt_attr _ NONE = []
  31.158 -  | opt_attr name (SOME value) = attr name value;
  31.159 -
  31.160 -val pgip_id = "dummy";
  31.161 -val pgip_serial = Counter.make ();
  31.162 -
  31.163 -fun output_pgip refid refseq content =
  31.164 -  XML.Elem (("pgip",
  31.165 -    attr "tag" "Isabelle/Isar" @
  31.166 -    attr "id" pgip_id @
  31.167 -    opt_attr "destid" refid @
  31.168 -    attr "class" "pg" @
  31.169 -    opt_attr "refid" refid @
  31.170 -    attr "refseq" refseq @
  31.171 -    attr "seq" (string_of_int (pgip_serial ()))), content)
  31.172 -  |> XML.string_of
  31.173 -  |> Output.urgent_message;
  31.174 -
  31.175 -
  31.176 -fun invalid_pgip () = raise Fail "Invalid PGIP packet";
  31.177 -
  31.178 -fun haspref {name, descr, default, pgiptype} =
  31.179 -  XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]),
  31.180 -    [XML.Elem ((pgiptype, []), [])]);
  31.181 -
  31.182 -fun process_element refid refseq (XML.Elem (("askprefs", _), _)) =
  31.183 -      all_preferences () |> List.app (fn (category, prefs) =>
  31.184 -        output_pgip refid refseq
  31.185 -          [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
  31.186 -  | process_element _ _ (XML.Elem (("setpref", attrs), data)) =
  31.187 -      let
  31.188 -        val name =
  31.189 -          (case Properties.get attrs "name" of
  31.190 -            SOME name => name
  31.191 -          | NONE => invalid_pgip ());
  31.192 -        val value = XML.content_of data;
  31.193 -      in set_preference name value end
  31.194 -  | process_element _ _ _ = invalid_pgip ();
  31.195 -
  31.196 -in
  31.197 -
  31.198 -fun process_pgip str =
  31.199 -  (case XML.parse str of
  31.200 -    XML.Elem (("pgip", attrs), pgips) =>
  31.201 -      let
  31.202 -        val class = get_attr attrs "class";
  31.203 -        val dest = Properties.get attrs "destid";
  31.204 -        val refid = Properties.get attrs "id";
  31.205 -        val refseq = get_attr attrs "seq";
  31.206 -        val processit =
  31.207 -          (case dest of
  31.208 -            NONE => class = "pa"
  31.209 -          | SOME id => id = pgip_id);
  31.210 -       in if processit then List.app (process_element refid refseq) pgips else () end
  31.211 -  | _ => invalid_pgip ())
  31.212 -  handle Fail msg => raise Fail (msg ^ "\n" ^ str);
  31.213 -
  31.214 -end;
  31.215 -
  31.216 -
  31.217 -(** messages **)
  31.218 -
  31.219 -(* render markup *)
  31.220 -
  31.221 -fun special ch = chr 1 ^ ch;
  31.222 -
  31.223 -local
  31.224 -
  31.225 -fun render_trees ts = fold render_tree ts
  31.226 -and render_tree t =
  31.227 -  (case XML.unwrap_elem t of
  31.228 -    SOME (_, ts) => render_trees ts
  31.229 -  | NONE =>
  31.230 -      (case t of
  31.231 -        XML.Text s => Buffer.add s
  31.232 -      | XML.Elem ((name, props), ts) =>
  31.233 -          let
  31.234 -            val (bg, en) =
  31.235 -              if null ts then Markup.no_output
  31.236 -              else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
  31.237 -              else if name = Markup.sendbackN then (special "W", special "X")
  31.238 -              else if name = Markup.intensifyN then (special "0", special "1")
  31.239 -              else if name = Markup.informationN then ("\n" ^ special "0", special "1")
  31.240 -              else if name = Markup.tfreeN then (special "C", special "A")
  31.241 -              else if name = Markup.tvarN then (special "D", special "A")
  31.242 -              else if name = Markup.freeN then (special "E", special "A")
  31.243 -              else if name = Markup.boundN then (special "F", special "A")
  31.244 -              else if name = Markup.varN then (special "G", special "A")
  31.245 -              else if name = Markup.skolemN then (special "H", special "A")
  31.246 -              else
  31.247 -                (case Markup.get_entity_kind (name, props) of
  31.248 -                  SOME kind =>
  31.249 -                    if kind = Markup.classN then (special "B", special "A")
  31.250 -                    else Markup.no_output
  31.251 -                | NONE => Markup.no_output);
  31.252 -          in Buffer.add bg #> render_trees ts #> Buffer.add en end));
  31.253 -
  31.254 -in
  31.255 -
  31.256 -fun render text =
  31.257 -  Buffer.content (render_trees (YXML.parse_body text) Buffer.empty);
  31.258 -
  31.259 -end;
  31.260 -
  31.261 -
  31.262 -(* hooks *)
  31.263 -
  31.264 -fun message bg en prfx body =
  31.265 -  (case render (implode body) of
  31.266 -    "" => ()
  31.267 -  | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
  31.268 -
  31.269 -fun setup_messages () =
  31.270 - (Output.writeln_fn := message "" "" "";
  31.271 -  Output.status_fn := (fn _ => ());
  31.272 -  Output.report_fn := (fn _ => ());
  31.273 -  Output.urgent_message_fn := message (special "I") (special "J") "";
  31.274 -  Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
  31.275 -  Output.warning_fn := message (special "K") (special "L") "### ";
  31.276 -  Output.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
  31.277 -  Output.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
  31.278 -
  31.279 -
  31.280 -(* notification *)
  31.281 -
  31.282 -fun emacs_notify s = message (special "I") (special "J") "" [s];
  31.283 -
  31.284 -fun tell_clear_goals () =
  31.285 -  emacs_notify "Proof General, please clear the goals buffer.";
  31.286 -
  31.287 -fun tell_clear_response () =
  31.288 -  emacs_notify "Proof General, please clear the response buffer.";
  31.289 -
  31.290 -fun tell_file_loaded path =
  31.291 -  emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
  31.292 -
  31.293 -fun tell_file_retracted path =
  31.294 -  emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
  31.295 -
  31.296 -
  31.297 -
  31.298 -(** theory loader **)
  31.299 -
  31.300 -(* global master path *)
  31.301 -
  31.302 -val master_path = Unsynchronized.ref Path.current;
  31.303 -
  31.304 -(*fake old ThyLoad -- with new semantics*)
  31.305 -structure ThyLoad =
  31.306 -struct
  31.307 -  fun add_path path = master_path := Path.explode path;
  31.308 -end;
  31.309 -
  31.310 -
  31.311 -(* actions *)
  31.312 -
  31.313 -local
  31.314 -
  31.315 -fun trace_action action name =
  31.316 -  if action = Thy_Info.Update then
  31.317 -    List.app tell_file_loaded (Thy_Info.loaded_files name)
  31.318 -  else if action = Thy_Info.Remove then
  31.319 -    List.app tell_file_retracted (Thy_Info.loaded_files name)
  31.320 -  else ();
  31.321 -
  31.322 -in
  31.323 -  fun setup_thy_loader () = Thy_Info.add_hook trace_action;
  31.324 -  fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
  31.325 -end;
  31.326 -
  31.327 -
  31.328 -(* get informed about files *)
  31.329 -
  31.330 -(*liberal low-level version*)
  31.331 -val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
  31.332 -
  31.333 -val inform_file_retracted = Thy_Info.kill_thy o thy_name;
  31.334 -
  31.335 -fun inform_file_processed file =
  31.336 -  let
  31.337 -    val name = thy_name file;
  31.338 -    val _ = name = "" andalso error ("Bad file name: " ^ quote file);
  31.339 -    val _ =
  31.340 -      Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
  31.341 -        handle ERROR msg =>
  31.342 -          (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
  31.343 -            tell_file_retracted (Resources.thy_path (Path.basic name)))
  31.344 -    val _ = Isar.init ();
  31.345 -  in () end;
  31.346 -
  31.347 -
  31.348 -
  31.349 -(** theorem dependencies **)
  31.350 -
  31.351 -(* thm_deps *)
  31.352 -
  31.353 -local
  31.354 -
  31.355 -fun add_proof_body (PBody {thms, ...}) =
  31.356 -  thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
  31.357 -
  31.358 -fun add_thm th =
  31.359 -  (case Thm.proof_body_of th of
  31.360 -    PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
  31.361 -      if Thm.has_name_hint th andalso Thm.get_name_hint th = name
  31.362 -      then add_proof_body (Future.join body)
  31.363 -      else I
  31.364 -  | body => add_proof_body body);
  31.365 -
  31.366 -in
  31.367 -
  31.368 -fun get_thm_deps ths =
  31.369 -  let
  31.370 -    (* FIXME proper derivation names!? *)
  31.371 -    val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
  31.372 -    val deps = Symtab.keys (fold add_thm ths Symtab.empty);
  31.373 -  in (names, deps) end;
  31.374 -
  31.375 -end;
  31.376 -
  31.377 -
  31.378 -(* report via hook *)
  31.379 -
  31.380 -val thm_deps = Unsynchronized.ref false;
  31.381 -
  31.382 -local
  31.383 -
  31.384 -val spaces_quote = space_implode " " o map quote;
  31.385 -
  31.386 -fun thm_deps_message (thms, deps) =
  31.387 -  emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
  31.388 -
  31.389 -in
  31.390 -
  31.391 -fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
  31.392 -  if ! thm_deps andalso can Toplevel.theory_of state andalso Toplevel.is_theory state'
  31.393 -  then
  31.394 -    let
  31.395 -      val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state);
  31.396 -      val facts = Global_Theory.facts_of (Toplevel.theory_of state');
  31.397 -      val (names, deps) = get_thm_deps (maps #2 (Facts.dest_static true [prev_facts] facts));
  31.398 -    in
  31.399 -      if null names orelse null deps then ()
  31.400 -      else thm_deps_message (spaces_quote names, spaces_quote deps)
  31.401 -    end
  31.402 -  else ());
  31.403 -
  31.404 -end;
  31.405 -
  31.406 -
  31.407 -
  31.408 -(** startup **)
  31.409 -
  31.410 -(* init *)
  31.411 -
  31.412 -val proof_generalN = "ProofGeneral";
  31.413 -
  31.414 -val initialized = Unsynchronized.ref false;
  31.415 -
  31.416 -fun init () =
  31.417 -  (if ! initialized then ()
  31.418 -   else
  31.419 -    (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
  31.420 -     Output.add_mode proof_generalN Output.default_output Output.default_escape;
  31.421 -     Markup.add_mode proof_generalN YXML.output_markup;
  31.422 -     setup_messages ();
  31.423 -     setup_thy_loader ();
  31.424 -     setup_present_hook ();
  31.425 -     initialized := true);
  31.426 -   init_preferences ();
  31.427 -   sync_thy_loader ();
  31.428 -   Unsynchronized.change print_mode (update (op =) proof_generalN);
  31.429 -   Secure.PG_setup ();
  31.430 -   Isar.toplevel_loop TextIO.stdIn
  31.431 -    {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
  31.432 -
  31.433 -
  31.434 -(* restart *)
  31.435 -
  31.436 -val welcome = Output.urgent_message o Session.welcome;
  31.437 -
  31.438 -fun restart () =
  31.439 - (sync_thy_loader ();
  31.440 -  tell_clear_goals ();
  31.441 -  tell_clear_response ();
  31.442 -  Isar.init ();
  31.443 -  welcome ());
  31.444 -
  31.445 -end;
  31.446 -
    32.1 --- a/src/Pure/build-jars	Thu Oct 30 23:14:11 2014 +0100
    32.2 +++ b/src/Pure/build-jars	Fri Oct 31 11:18:17 2014 +0100
    32.3 @@ -90,7 +90,6 @@
    32.4    Tools/build_doc.scala
    32.5    Tools/check_source.scala
    32.6    Tools/doc.scala
    32.7 -  Tools/keywords.scala
    32.8    Tools/main.scala
    32.9    Tools/ml_statistics.scala
   32.10    Tools/print_operation.scala
    33.1 --- a/src/Pure/pure_syn.ML	Thu Oct 30 23:14:11 2014 +0100
    33.2 +++ b/src/Pure/pure_syn.ML	Fri Oct 31 11:18:17 2014 +0100
    33.3 @@ -11,8 +11,7 @@
    33.4    Outer_Syntax.command
    33.5      (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
    33.6      (Thy_Header.args >> (fn header =>
    33.7 -      Toplevel.init_theory
    33.8 -        (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
    33.9 +      Toplevel.init_theory (fn () => Thy_Info.toplevel_begin_theory Path.current header)));
   33.10  
   33.11  val _ =
   33.12    Outer_Syntax.command
    34.1 --- a/src/Tools/quickcheck.ML	Thu Oct 30 23:14:11 2014 +0100
    34.2 +++ b/src/Tools/quickcheck.ML	Fri Oct 31 11:18:17 2014 +0100
    34.3 @@ -90,16 +90,6 @@
    34.4  val unknownN = "unknown";
    34.5  
    34.6  
    34.7 -(* preferences *)
    34.8 -
    34.9 -val _ =
   34.10 -  ProofGeneral.preference_option ProofGeneral.category_tracing
   34.11 -    NONE
   34.12 -    @{system_option auto_quickcheck}
   34.13 -    "auto-quickcheck"
   34.14 -    "Run Quickcheck automatically";
   34.15 -
   34.16 -
   34.17  (* quickcheck report *)
   34.18  
   34.19  datatype report = Report of
    35.1 --- a/src/Tools/solve_direct.ML	Thu Oct 30 23:14:11 2014 +0100
    35.2 +++ b/src/Tools/solve_direct.ML	Fri Oct 31 11:18:17 2014 +0100
    35.3 @@ -34,13 +34,6 @@
    35.4  
    35.5  val max_solutions = Unsynchronized.ref 5;
    35.6  
    35.7 -val _ =
    35.8 -  ProofGeneral.preference_option ProofGeneral.category_tracing
    35.9 -    NONE
   35.10 -    @{system_option auto_solve_direct}
   35.11 -    "auto-solve-direct"
   35.12 -    ("Run " ^ quote solve_directN ^ " automatically");
   35.13 -
   35.14  
   35.15  (* solve_direct command *)
   35.16  
    36.1 --- a/src/Tools/try.ML	Thu Oct 30 23:14:11 2014 +0100
    36.2 +++ b/src/Tools/try.ML	Fri Oct 31 11:18:17 2014 +0100
    36.3 @@ -27,16 +27,6 @@
    36.4  val tryN = "try"
    36.5  
    36.6  
    36.7 -(* preferences *)
    36.8 -
    36.9 -val _ =
   36.10 -  ProofGeneral.preference_option ProofGeneral.category_tracing
   36.11 -    (SOME "4.0")
   36.12 -    @{system_option auto_time_limit}
   36.13 -    "auto-try-time-limit"
   36.14 -    "Time limit for automatically tried tools (in seconds)"
   36.15 -
   36.16 -
   36.17  (* helpers *)
   36.18  
   36.19  fun serial_commas _ [] = ["??"]