1.1 --- a/lib/Tools/build_dialog	Thu Dec 06 16:07:09 2012 +0100
     1.2 +++ b/lib/Tools/build_dialog	Thu Dec 06 17:59:37 2012 +0100
     1.3 @@ -16,6 +16,7 @@
     1.4    echo
     1.5    echo "  Options are:"
     1.6    echo "    -C           check for existing image"
     1.7 +  echo "    -L OPTION    default logic via system option"
     1.8    echo "    -d DIR       include session directory"
     1.9    echo "    -s           system build mode: produce output in ISABELLE_HOME"
    1.10    echo
    1.11 @@ -34,15 +35,19 @@
    1.12  ## process command line
    1.13  
    1.14  CHECK_EXISTING=false
    1.15 +LOGIC_OPTION=""
    1.16  declare -a INCLUDE_DIRS=()
    1.17  SYSTEM_MODE=false
    1.18  
    1.19 -while getopts "Cd:s" OPT
    1.20 +while getopts "CL:d:s" OPT
    1.21  do
    1.22    case "$OPT" in
    1.23      C)
    1.24        CHECK_EXISTING="true"
    1.25        ;;
    1.26 +    L)
    1.27 +      LOGIC_OPTION="$OPTARG"
    1.28 +      ;;
    1.29      d)
    1.30        INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
    1.31        ;;
    1.32 @@ -65,27 +70,10 @@
    1.33  SESSION="$1"; shift
    1.34  
    1.35  
    1.36 -## existing image
    1.37 +## main
    1.38  
    1.39 -EXISTING=false
    1.40 -if [ "$CHECK_EXISTING" = true ]; then
    1.41 -  declare -a ISABELLE_PATHS=()
    1.42 -  splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}")
    1.43 +[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
    1.44  
    1.45 -  for DIR in "${ISABELLE_PATHS[@]}"
    1.46 -  do
    1.47 -    FILE="$DIR/$ML_IDENTIFIER/$SESSION"
    1.48 -    [ -f "$FILE" ] && EXISTING=true
    1.49 -  done
    1.50 -fi
    1.51 +"$ISABELLE_TOOL" java isabelle.Build_Dialog \
    1.52 +  "$CHECK_EXISTING" "$LOGIC_OPTION" "$SYSTEM_MODE" "$SESSION" "${INCLUDE_DIRS[@]}"
    1.53  
    1.54 -
    1.55 -## build
    1.56 -
    1.57 -if [ "$EXISTING" = false ]; then
    1.58 -  [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
    1.59 -
    1.60 -  "$ISABELLE_TOOL" java isabelle.Build_Dialog \
    1.61 -    "$SYSTEM_MODE" "$SESSION" "${INCLUDE_DIRS[@]}"
    1.62 -fi
    1.63 -

     2.1 --- a/src/Pure/System/build_dialog.scala	Thu Dec 06 16:07:09 2012 +0100
     2.2 +++ b/src/Pure/System/build_dialog.scala	Thu Dec 06 17:59:37 2012 +0100
     2.3 @@ -16,6 +16,7 @@
     2.4  
     2.5  object Build_Dialog extends SwingApplication
     2.6  {
     2.7 +  // FIXME avoid startup via GUI thread!?
     2.8    def startup(args: Array[String]) =
     2.9    {
    2.10      Platform.init_laf()
    2.11 @@ -23,13 +24,28 @@
    2.12      try {
    2.13        args.toList match {
    2.14          case
    2.15 +          Properties.Value.Boolean(check_existing) ::
    2.16 +          logic_option ::
    2.17            Properties.Value.Boolean(system_mode) ::
    2.18 -          session :: include_dirs =>
    2.19 -            val center = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
    2.20 -            val top = build_dialog(system_mode, include_dirs.map(Path.explode), session)
    2.21 -            top.pack()
    2.22 -            top.location = new Point(center.x - top.size.width / 2, center.y - top.size.height / 2)
    2.23 -            top.visible = true
    2.24 +          session_arg ::
    2.25 +          include_dirs =>
    2.26 +            val session =
    2.27 +              Isabelle_System.default_logic(session_arg,
    2.28 +                if (logic_option != "") Options.init().string(logic_option) else "")
    2.29 +
    2.30 +            val no_dialog =  // FIXME full up-to-date test!?
    2.31 +              check_existing &&
    2.32 +                Isabelle_System.find_logics_dirs().exists(dir =>
    2.33 +                  (dir + Path.basic(session)).is_file)
    2.34 +
    2.35 +            if (no_dialog) sys.exit(0)
    2.36 +            else {
    2.37 +              val center = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
    2.38 +              val top = build_dialog(system_mode, include_dirs.map(Path.explode), session)
    2.39 +              top.pack()
    2.40 +              top.location = new Point(center.x - top.size.width / 2, center.y - top.size.height / 2)
    2.41 +              top.visible = true
    2.42 +            }
    2.43          case _ => error("Bad arguments:\n" + cat_lines(args))
    2.44        }
    2.45      }

     3.1 --- a/src/Pure/System/isabelle_system.scala	Thu Dec 06 16:07:09 2012 +0100
     3.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Dec 06 17:59:37 2012 +0100
     3.3 @@ -273,7 +273,7 @@
     3.4      Path.split(getenv_strict("ISABELLE_COMPONENTS"))
     3.5  
     3.6  
     3.7 -  /* find logics */
     3.8 +  /* logic images */
     3.9  
    3.10    def find_logics_dirs(): List[Path] =
    3.11    {
    3.12 @@ -287,6 +287,14 @@
    3.13        files = dir.file.listFiles() if files != null
    3.14        file <- files.toList if file.isFile } yield file.getName).sorted
    3.15  
    3.16 +  def default_logic(args: String*): String =
    3.17 +  {
    3.18 +    args.find(_ != "") match {
    3.19 +      case Some(logic) => logic
    3.20 +      case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC")
    3.21 +    }
    3.22 +  }
    3.23 +
    3.24  
    3.25    /* fonts */
    3.26  

     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Thu Dec 06 16:07:09 2012 +0100
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Dec 06 17:59:37 2012 +0100
     4.3 @@ -68,7 +68,7 @@
     4.4    echo "    -f           fresh build"
     4.5    echo "    -j OPTION    add jEdit runtime option"
     4.6    echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
     4.7 -  echo "    -l NAME      logic session name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
     4.8 +  echo "    -l NAME      logic session name"
     4.9    echo "    -m MODE      add print mode for output"
    4.10    echo "    -s           system build mode for session image"
    4.11    echo
    4.12 @@ -99,7 +99,7 @@
    4.13  BUILD_ONLY=false
    4.14  BUILD_JARS="jars"
    4.15  JEDIT_SESSION_DIRS=""
    4.16 -JEDIT_LOGIC="$ISABELLE_LOGIC"
    4.17 +JEDIT_LOGIC=""
    4.18  JEDIT_PRINT_MODE=""
    4.19  
    4.20  function getoptions()
    4.21 @@ -313,7 +313,7 @@
    4.22  
    4.23  # build logic
    4.24  
    4.25 -"$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -C "$JEDIT_LOGIC"
    4.26 +"$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -C -L jedit_logic "$JEDIT_LOGIC"
    4.27  RC="$?"
    4.28  [ "$RC" = 0 ] || exit "$RC"
    4.29  

     5.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Thu Dec 06 16:07:09 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Thu Dec 06 17:59:37 2012 +0100
     5.3 @@ -15,26 +15,24 @@
     5.4  
     5.5  object Isabelle_Logic
     5.6  {
     5.7 -  private def default_logic(): String =
     5.8 -  {
     5.9 -    val logic = Isabelle_System.getenv("JEDIT_LOGIC")
    5.10 -    if (logic != "") logic
    5.11 -    else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
    5.12 -  }
    5.13 +  private val option_name = "jedit_logic"
    5.14 +
    5.15 +  private def jedit_logic(): String =
    5.16 +    Isabelle_System.default_logic(
    5.17 +      Isabelle_System.getenv("JEDIT_LOGIC"),
    5.18 +      PIDE.options.string(option_name))
    5.19  
    5.20    private class Logic_Entry(val name: String, val description: String)
    5.21    {
    5.22      override def toString = description
    5.23    }
    5.24  
    5.25 -  private val option_name = "jedit_logic"
    5.26 -
    5.27    def logic_selector(autosave: Boolean): Option_Component =
    5.28    {
    5.29      Swing_Thread.require()
    5.30  
    5.31      val entries =
    5.32 -      new Logic_Entry("", "default (" + default_logic() + ")") ::
    5.33 +      new Logic_Entry("", "default (" + jedit_logic() + ")") ::
    5.34          Isabelle_Logic.session_list().map(name => new Logic_Entry(name, name))
    5.35  
    5.36      val component = new ComboBox(entries) with Option_Component {
    5.37 @@ -63,12 +61,7 @@
    5.38    def session_args(): List[String] =
    5.39    {
    5.40      val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
    5.41 -    val logic =
    5.42 -      PIDE.options.string(option_name) match {
    5.43 -        case "" => default_logic()
    5.44 -        case logic => logic
    5.45 -      }
    5.46 -    modes ::: List(logic)
    5.47 +    modes ::: List(jedit_logic())
    5.48    }
    5.49  
    5.50    def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))