--- a/NEWS Tue Nov 20 14:55:52 2012 +0100
+++ b/NEWS Tue Nov 20 15:18:11 2012 +0100
@@ -308,6 +308,9 @@
that are not bundled, or referenced from a bare-bones repository
version of Isabelle.
+* The "isabelle install" tool has now a simpler command-line. Minor
+INCOMPATIBILITY.
+
* Discontinued support for Poly/ML 5.2.1, which was the last version
without exception positions and advanced ML compiler/toplevel
configuration.
--- a/lib/Tools/install Tue Nov 20 14:55:52 2012 +0100
+++ b/lib/Tools/install Tue Nov 20 15:18:11 2012 +0100
@@ -10,14 +10,13 @@
function usage()
{
echo
- echo "Usage: isabelle $PRG [OPTIONS]"
+ echo "Usage: isabelle $PRG [OPTIONS] BINDIR"
echo
echo " Options are:"
echo " -d DISTDIR refer to DISTDIR as Isabelle distribution"
echo " (default ISABELLE_HOME)"
- echo " -p DIR install standalone binaries in DIR"
echo
- echo " Install Isabelle executables with absolute references to the current"
+ echo " Install Isabelle executables with absolute references to the"
echo " distribution directory."
echo
exit 1
@@ -34,21 +33,15 @@
# options
-NO_OPTS=true
-
DISTDIR="$ISABELLE_HOME"
BINDIR=""
-while getopts "d:p:" OPT
+while getopts "d:" OPT
do
- NO_OPTS=""
case "$OPT" in
d)
DISTDIR="$OPTARG"
;;
- p)
- BINDIR="$OPTARG"
- ;;
\?)
usage
;;
@@ -60,28 +53,25 @@
# args
-[ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage
+[ "$#" -ge 1 ] && { BINDIR="$1"; shift; }
+[ "$#" -ne 0 -o -z "$BINDIR" ] && usage
## main
-echo "referring to distribution at $DISTDIR"
-
+echo "referring to distribution at \"$DISTDIR\""
-# standalone binaries
-
-if [ -n "$BINDIR" ]; then
- mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
+mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
- for NAME in isabelle isabelle-process
- do
- BIN="$BINDIR/$NAME"
- DIST="$DISTDIR/bin/$NAME"
- echo "installing $BIN"
- rm -f "$BIN"
- echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"
- echo >> "$BIN"
- echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
- chmod +x "$BIN"
- done
-fi
+for NAME in isabelle isabelle-process
+do
+ BIN="$BINDIR/$NAME"
+ DIST="$DISTDIR/bin/$NAME"
+ echo "installing $BIN"
+ rm -f "$BIN"
+ echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"
+ echo >> "$BIN"
+ echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
+ chmod +x "$BIN"
+done
+
--- a/src/Doc/System/Misc.thy Tue Nov 20 14:55:52 2012 +0100
+++ b/src/Doc/System/Misc.thy Tue Nov 20 15:18:11 2012 +0100
@@ -180,31 +180,27 @@
@{setting PATH}. Other schemes of installation are supported by the
@{tool_def install} tool:
\begin{ttbox}
-Usage: isabelle install [OPTIONS]
+Usage: isabelle install [OPTIONS] BINDIR
Options are:
- -d DISTDIR use DISTDIR as Isabelle distribution
+ -d DISTDIR refer to DISTDIR as Isabelle distribution
(default ISABELLE_HOME)
- -p DIR install standalone binaries in DIR
- Install Isabelle executables with absolute references to the current
+ Install Isabelle executables with absolute references to the
distribution directory.
\end{ttbox}
The @{verbatim "-d"} option overrides the current Isabelle
distribution directory as determined by @{setting ISABELLE_HOME}.
- The @{verbatim "-p"} option installs executable wrapper scripts for
- @{executable "isabelle-process"}, @{executable isabelle}, containing
- proper absolute references to the Isabelle distribution directory.
- A typical @{verbatim DIR} specification would be some directory
- expected to be in the shell's @{setting PATH}, such as @{verbatim
- "$HOME/bin"}.
+ The @{text BINDIR} argument tells where executable wrapper scripts
+ for @{executable "isabelle-process"} and @{executable isabelle}
+ should be placed, which is typically a directory in the shell's
+ @{setting PATH}, such as @{verbatim "$HOME/bin"}.
- It is possible to make symbolic links of the main Isabelle
- executables, but making separate copies outside the Isabelle
- distribution directory will not work.
-*}
+ \medskip It is also possible to make symbolic links of the main
+ Isabelle executables manually, but making separate copies outside
+ the Isabelle distribution directory will not work! *}
section {* Creating instances of the Isabelle logo *}