ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);

--- a/Admin/components/components.sha1	Mon Jun 30 10:34:28 2014 +0200
+++ b/Admin/components/components.sha1	Mon Jun 30 10:53:37 2014 +0200
@@ -67,6 +67,7 @@
 8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
 847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
 8e0b2b432755ef11d964e20637d1bc567d1c0477  ProofGeneral-4.2-1.tar.gz
+51e1e0f399e934020565b2301358452c0bcc8a5e  ProofGeneral-4.2-2.tar.gz
 8472221c876a430cde325841ce52893328302712  ProofGeneral-4.2.tar.gz
 0885e1f1d8feaca78d2f204b6487e6eec6dfab4b  scala-2.10.0.tar.gz
 f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc  scala-2.10.1.tar.gz

--- a/Admin/components/main	Mon Jun 30 10:34:28 2014 +0200
+++ b/Admin/components/main	Mon Jun 30 10:53:37 2014 +0200
@@ -14,4 +14,3 @@
 z3-3.2-1
 z3-4.3.2pre-1
 xz-java-1.2-1
-ProofGeneral-4.2-1

--- a/Admin/components/optional	Mon Jun 30 10:34:28 2014 +0200
+++ b/Admin/components/optional	Mon Jun 30 10:53:37 2014 +0200
@@ -1,2 +1,3 @@
 #optional components that could impact build time significantly
 hol-light-bundle-0.5-126
+ProofGeneral-4.2-2

--- a/Admin/lib/Tools/makedist_bundle	Mon Jun 30 10:34:28 2014 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Mon Jun 30 10:53:37 2014 +0200
@@ -96,7 +96,7 @@
             COMPONENT="$REPLY"
             COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT"
             case "$COMPONENT" in
-              jedit_build* | ProofGeneral*) ;;
+              jedit_build*) ;;
               *)
                 echo "  component $COMPONENT"
                 CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz"

--- a/NEWS	Mon Jun 30 10:34:28 2014 +0200
+++ b/NEWS	Mon Jun 30 10:53:37 2014 +0200
@@ -872,6 +872,12 @@
 
 *** System ***
 
+* Proof General with its traditional helper scripts is now an optional
+Isabelle component, e.g. ProofGeneral-4.2-2 from the Isabelle
+component repository http://isabelle.in.tum.de/components/.  See also
+the "system" manual for general explanations about add-on components,
+notably those that are not bundled with the normal release.
+
 * Session ROOT specifications require explicit 'document_files' for
 robust dependencies on LaTeX sources.  Only these explicitly given
 files are copied to the document output directory, before document

--- a/lib/Tools/emacs	Mon Jun 30 10:34:28 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: Proof General / Emacs interface wrapper -- Proof General legacy
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## main
-
-[ -z "$PROOFGENERAL_HOME" ] && fail "Missing Proof General installation (PROOFGENERAL_HOME)"
-
-INTERFACE="$PROOFGENERAL_HOME/isar/interface"
-[ ! -x "$INTERFACE" ] && fail "Bad interface script: \"$INTERFACE\""
-
-#legacy settings
-export ISABELLE="$ISABELLE_PROCESS"
-export ISATOOL="$ISABELLE_TOOL"
-
-exec "$INTERFACE" "$@"

--- a/lib/Tools/findlogics	Mon Jun 30 10:34:28 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: collect heap names from ISABELLE_PATH -- Proof General legacy
-
-
-PRG=$(basename "$0")
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG"
-  echo
-  echo "  Collect heap file names from ISABELLE_PATH."
-  echo
-  exit 1
-}
-
-
-## main
-
-[ "$#" -ne 0 ] && usage
-
-declare -a LOGICS=()
-declare -a ISABELLE_PATHS=()
-
-splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}")
-
-for DIR in "${ISABELLE_PATHS[@]}"
-do
-  DIR="$DIR/$ML_IDENTIFIER"
-  for FILE in "$DIR"/*
-  do
-    if [ -f "$FILE" ]; then
-      NAME=$(basename "$FILE")
-      LOGICS["${#LOGICS[@]}"]="$NAME"
-    fi
-  done
-done
-
-echo $({ for L in "${LOGICS[@]}"; do echo "$L"; done; } | sort | uniq)

--- a/src/Doc/System/Misc.thy	Mon Jun 30 10:34:28 2014 +0200
+++ b/src/Doc/System/Misc.thy	Mon Jun 30 10:53:37 2014 +0200
@@ -309,41 +309,6 @@
 *}
 
 
-section {* Proof General / Emacs *}
-
-text {* The @{tool_def emacs} tool invokes a version of Emacs and
-  Proof General\footnote{@{url "http://proofgeneral.inf.ed.ac.uk/"}} within the
-  regular Isabelle settings environment (\secref{sec:settings}).  This
-  is more convenient than starting Emacs separately, loading the Proof
-  General LISP files, and then attempting to start Isabelle with
-  dynamic @{setting PATH} lookup etc., although it might fail if a
-  different version of Proof General is already part of the Emacs
-  installation of the operating system.
-
-  The actual interface script is part of the Proof General
-  distribution; its usage depends on the particular version.  There
-  are some options available, such as @{verbatim "-l"} for passing the
-  logic image to be used by default, or @{verbatim "-m"} to tune the
-  standard print mode of the prover process.  The following Isabelle
-  settings are particularly important for Proof General:
-
-  \begin{description}
-
-  \item[@{setting_def PROOFGENERAL_HOME}] points to the main
-  installation directory of the Proof General distribution.  This is
-  implicitly provided for versions of Proof General that are
-  distributed as Isabelle component, see also \secref{sec:components};
-  otherwise it needs to be configured manually.
-
-  \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
-  the command line of any invocation of the Proof General @{verbatim
-  interface} script.  This allows to provide persistent default
-  options for the invocation of \texttt{isabelle emacs}.
-
-  \end{description}
-*}
-
-
 section {* Shell commands within the settings environment \label{sec:tool-env} *}
 
 text {* The @{tool_def env} tool is a direct wrapper for the standard