--- a/lib/Tools/build_dialog Sat Dec 15 12:55:11 2012 +0100
+++ b/lib/Tools/build_dialog Sat Dec 15 13:14:55 2012 +0100
@@ -12,14 +12,15 @@
function usage()
{
echo
- echo "Usage: isabelle $PRG [OPTIONS] LOGIC"
+ echo "Usage: isabelle $PRG [OPTIONS]"
echo
echo " Options are:"
echo " -L OPTION default logic via system option"
echo " -d DIR include session directory"
+ echo " -l NAME logic session name"
echo " -s system build mode: produce output in ISABELLE_HOME"
echo
- echo " Build Isabelle session image LOGIC via GUI dialog."
+ echo " Build Isabelle logic session image via GUI dialog (default: $ISABELLE_LOGIC)."
echo
exit 1
}
@@ -35,9 +36,10 @@
LOGIC_OPTION=""
declare -a INCLUDE_DIRS=()
+LOGIC=""
SYSTEM_MODE=false
-while getopts "L:d:s" OPT
+while getopts "L:d:l:s" OPT
do
case "$OPT" in
L)
@@ -46,6 +48,9 @@
d)
INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
;;
+ l)
+ LOGIC="$OPTARG"
+ ;;
s)
SYSTEM_MODE="true"
;;
@@ -60,9 +65,7 @@
# args
-[ "$#" -ne 1 ] && usage
-
-LOGIC="$1"; shift
+[ "$#" -ne 0 ] && usage
## main
@@ -70,5 +73,5 @@
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
"$ISABELLE_TOOL" java isabelle.Build_Dialog \
- "$LOGIC_OPTION" "$SYSTEM_MODE" "$LOGIC" "${INCLUDE_DIRS[@]}"
+ "$LOGIC_OPTION" "$LOGIC" "$SYSTEM_MODE" "${INCLUDE_DIRS[@]}"
--- a/src/Doc/System/Sessions.thy Sat Dec 15 12:55:11 2012 +0100
+++ b/src/Doc/System/Sessions.thy Sat Dec 15 13:14:55 2012 +0100
@@ -348,16 +348,18 @@
Options are:
-L OPTION default logic via system option
-d DIR include session directory
+ -l NAME logic session name
-s system build mode: produce output in ISABELLE_HOME
- Build Isabelle session image LOGIC via GUI dialog.
+ Build Isabelle logic session image via GUI dialog (default: \$ISABELLE_LOGIC).
\end{ttbox}
- \medskip Option @{verbatim "-L"} specifies a system option name as
- fall-back, if the specified @{text "LOGIC"} name is empty.
+ \medskip Option @{verbatim "-l"} specifies an explicit logic session
+ name. Option @{verbatim "-L"} specifies a system option name as
+ fall-back to determine the logic session name. If both are omitted
+ or have empty value, @{setting ISABELLE_LOGIC} is used as default.
\medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same
- meaning as for the command-line @{tool build} tool itself.
-*}
+ meaning as for the command-line @{tool build} tool itself. *}
end
--- a/src/Pure/System/build_dialog.scala Sat Dec 15 12:55:11 2012 +0100
+++ b/src/Pure/System/build_dialog.scala Sat Dec 15 13:14:55 2012 +0100
@@ -23,8 +23,8 @@
args.toList match {
case
logic_option ::
+ logic ::
Properties.Value.Boolean(system_mode) ::
- logic ::
include_dirs =>
val more_dirs = include_dirs.map(s => ((false, Path.explode(s))))
--- a/src/Tools/jEdit/lib/Tools/jedit Sat Dec 15 12:55:11 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Dec 15 13:14:55 2012 +0100
@@ -97,7 +97,7 @@
# options
-declare -a BUILD_DIALOG_OPTIONS=()
+declare -a BUILD_DIALOG_OPTIONS=(-L jedit_logic)
BUILD_ONLY=false
BUILD_JARS="jars"
@@ -134,6 +134,8 @@
ARGS["${#ARGS[@]}"]="$OPTARG"
;;
l)
+ BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-l"
+ BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG"
JEDIT_LOGIC="$OPTARG"
;;
m)
@@ -328,7 +330,7 @@
if [ "$BUILD_ONLY" = false ]; then
if [ "$NO_BUILD" = false ]; then
- "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -L jedit_logic "$JEDIT_LOGIC"
+ "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}"
RC="$?"
[ "$RC" = 0 ] || exit "$RC"
fi