# HG changeset patch
# User wenzelm
# Date 1355573695 -3600
# Node ID 1b01a57d27499fd86939788160742ac5a8cf3898
# Parent  00bdc48c5f71a1a5ac94cdf80663d11b811b577e
clarified build_dialog command line;

diff -r 00bdc48c5f71 -r 1b01a57d2749 lib/Tools/build_dialog
--- 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[@]}"
 
diff -r 00bdc48c5f71 -r 1b01a57d2749 src/Doc/System/Sessions.thy
--- 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
diff -r 00bdc48c5f71 -r 1b01a57d2749 src/Pure/System/build_dialog.scala
--- 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))))
 
diff -r 00bdc48c5f71 -r 1b01a57d2749 src/Tools/jEdit/lib/Tools/jedit
--- 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