ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);
authorwenzelm
Mon Jun 30 10:53:37 2014 +0200 (2014-06-30)
changeset 57443577f029fde39
parent 57442 2373b4c61111
child 57444 a26c39b95cee
ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);
Admin/components/components.sha1
Admin/components/main
Admin/components/optional
Admin/lib/Tools/makedist_bundle
NEWS
lib/Tools/emacs
lib/Tools/findlogics
src/Doc/System/Misc.thy
     1.1 --- a/Admin/components/components.sha1	Mon Jun 30 10:34:28 2014 +0200
     1.2 +++ b/Admin/components/components.sha1	Mon Jun 30 10:53:37 2014 +0200
     1.3 @@ -67,6 +67,7 @@
     1.4  8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
     1.5  847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
     1.6  8e0b2b432755ef11d964e20637d1bc567d1c0477  ProofGeneral-4.2-1.tar.gz
     1.7 +51e1e0f399e934020565b2301358452c0bcc8a5e  ProofGeneral-4.2-2.tar.gz
     1.8  8472221c876a430cde325841ce52893328302712  ProofGeneral-4.2.tar.gz
     1.9  0885e1f1d8feaca78d2f204b6487e6eec6dfab4b  scala-2.10.0.tar.gz
    1.10  f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc  scala-2.10.1.tar.gz
     2.1 --- a/Admin/components/main	Mon Jun 30 10:34:28 2014 +0200
     2.2 +++ b/Admin/components/main	Mon Jun 30 10:53:37 2014 +0200
     2.3 @@ -14,4 +14,3 @@
     2.4  z3-3.2-1
     2.5  z3-4.3.2pre-1
     2.6  xz-java-1.2-1
     2.7 -ProofGeneral-4.2-1
     3.1 --- a/Admin/components/optional	Mon Jun 30 10:34:28 2014 +0200
     3.2 +++ b/Admin/components/optional	Mon Jun 30 10:53:37 2014 +0200
     3.3 @@ -1,2 +1,3 @@
     3.4  #optional components that could impact build time significantly
     3.5  hol-light-bundle-0.5-126
     3.6 +ProofGeneral-4.2-2
     4.1 --- a/Admin/lib/Tools/makedist_bundle	Mon Jun 30 10:34:28 2014 +0200
     4.2 +++ b/Admin/lib/Tools/makedist_bundle	Mon Jun 30 10:53:37 2014 +0200
     4.3 @@ -96,7 +96,7 @@
     4.4              COMPONENT="$REPLY"
     4.5              COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT"
     4.6              case "$COMPONENT" in
     4.7 -              jedit_build* | ProofGeneral*) ;;
     4.8 +              jedit_build*) ;;
     4.9                *)
    4.10                  echo "  component $COMPONENT"
    4.11                  CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz"
     5.1 --- a/NEWS	Mon Jun 30 10:34:28 2014 +0200
     5.2 +++ b/NEWS	Mon Jun 30 10:53:37 2014 +0200
     5.3 @@ -872,6 +872,12 @@
     5.4  
     5.5  *** System ***
     5.6  
     5.7 +* Proof General with its traditional helper scripts is now an optional
     5.8 +Isabelle component, e.g. ProofGeneral-4.2-2 from the Isabelle
     5.9 +component repository http://isabelle.in.tum.de/components/.  See also
    5.10 +the "system" manual for general explanations about add-on components,
    5.11 +notably those that are not bundled with the normal release.
    5.12 +
    5.13  * Session ROOT specifications require explicit 'document_files' for
    5.14  robust dependencies on LaTeX sources.  Only these explicitly given
    5.15  files are copied to the document output directory, before document
     6.1 --- a/lib/Tools/emacs	Mon Jun 30 10:34:28 2014 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,28 +0,0 @@
     6.4 -#!/usr/bin/env bash
     6.5 -#
     6.6 -# Author: Makarius
     6.7 -#
     6.8 -# DESCRIPTION: Proof General / Emacs interface wrapper -- Proof General legacy
     6.9 -
    6.10 -
    6.11 -## diagnostics
    6.12 -
    6.13 -function fail()
    6.14 -{
    6.15 -  echo "$1" >&2
    6.16 -  exit 2
    6.17 -}
    6.18 -
    6.19 -
    6.20 -## main
    6.21 -
    6.22 -[ -z "$PROOFGENERAL_HOME" ] && fail "Missing Proof General installation (PROOFGENERAL_HOME)"
    6.23 -
    6.24 -INTERFACE="$PROOFGENERAL_HOME/isar/interface"
    6.25 -[ ! -x "$INTERFACE" ] && fail "Bad interface script: \"$INTERFACE\""
    6.26 -
    6.27 -#legacy settings
    6.28 -export ISABELLE="$ISABELLE_PROCESS"
    6.29 -export ISATOOL="$ISABELLE_TOOL"
    6.30 -
    6.31 -exec "$INTERFACE" "$@"
     7.1 --- a/lib/Tools/findlogics	Mon Jun 30 10:34:28 2014 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,42 +0,0 @@
     7.4 -#!/usr/bin/env bash
     7.5 -#
     7.6 -# Author: Markus Wenzel, TU Muenchen
     7.7 -#
     7.8 -# DESCRIPTION: collect heap names from ISABELLE_PATH -- Proof General legacy
     7.9 -
    7.10 -
    7.11 -PRG=$(basename "$0")
    7.12 -
    7.13 -function usage()
    7.14 -{
    7.15 -  echo
    7.16 -  echo "Usage: isabelle $PRG"
    7.17 -  echo
    7.18 -  echo "  Collect heap file names from ISABELLE_PATH."
    7.19 -  echo
    7.20 -  exit 1
    7.21 -}
    7.22 -
    7.23 -
    7.24 -## main
    7.25 -
    7.26 -[ "$#" -ne 0 ] && usage
    7.27 -
    7.28 -declare -a LOGICS=()
    7.29 -declare -a ISABELLE_PATHS=()
    7.30 -
    7.31 -splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}")
    7.32 -
    7.33 -for DIR in "${ISABELLE_PATHS[@]}"
    7.34 -do
    7.35 -  DIR="$DIR/$ML_IDENTIFIER"
    7.36 -  for FILE in "$DIR"/*
    7.37 -  do
    7.38 -    if [ -f "$FILE" ]; then
    7.39 -      NAME=$(basename "$FILE")
    7.40 -      LOGICS["${#LOGICS[@]}"]="$NAME"
    7.41 -    fi
    7.42 -  done
    7.43 -done
    7.44 -
    7.45 -echo $({ for L in "${LOGICS[@]}"; do echo "$L"; done; } | sort | uniq)
     8.1 --- a/src/Doc/System/Misc.thy	Mon Jun 30 10:34:28 2014 +0200
     8.2 +++ b/src/Doc/System/Misc.thy	Mon Jun 30 10:53:37 2014 +0200
     8.3 @@ -309,41 +309,6 @@
     8.4  *}
     8.5  
     8.6  
     8.7 -section {* Proof General / Emacs *}
     8.8 -
     8.9 -text {* The @{tool_def emacs} tool invokes a version of Emacs and
    8.10 -  Proof General\footnote{@{url "http://proofgeneral.inf.ed.ac.uk/"}} within the
    8.11 -  regular Isabelle settings environment (\secref{sec:settings}).  This
    8.12 -  is more convenient than starting Emacs separately, loading the Proof
    8.13 -  General LISP files, and then attempting to start Isabelle with
    8.14 -  dynamic @{setting PATH} lookup etc., although it might fail if a
    8.15 -  different version of Proof General is already part of the Emacs
    8.16 -  installation of the operating system.
    8.17 -
    8.18 -  The actual interface script is part of the Proof General
    8.19 -  distribution; its usage depends on the particular version.  There
    8.20 -  are some options available, such as @{verbatim "-l"} for passing the
    8.21 -  logic image to be used by default, or @{verbatim "-m"} to tune the
    8.22 -  standard print mode of the prover process.  The following Isabelle
    8.23 -  settings are particularly important for Proof General:
    8.24 -
    8.25 -  \begin{description}
    8.26 -
    8.27 -  \item[@{setting_def PROOFGENERAL_HOME}] points to the main
    8.28 -  installation directory of the Proof General distribution.  This is
    8.29 -  implicitly provided for versions of Proof General that are
    8.30 -  distributed as Isabelle component, see also \secref{sec:components};
    8.31 -  otherwise it needs to be configured manually.
    8.32 -
    8.33 -  \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
    8.34 -  the command line of any invocation of the Proof General @{verbatim
    8.35 -  interface} script.  This allows to provide persistent default
    8.36 -  options for the invocation of \texttt{isabelle emacs}.
    8.37 -
    8.38 -  \end{description}
    8.39 -*}
    8.40 -
    8.41 -
    8.42  section {* Shell commands within the settings environment \label{sec:tool-env} *}
    8.43  
    8.44  text {* The @{tool_def env} tool is a direct wrapper for the standard