# HG changeset patch # User wenzelm # Date 1354813177 -3600 # Node ID 87868964733c99e90ea5d9e8f8694ccdd029b025 # Parent 923f1e199f4f6ac68075d1f2d08fe106ebfc3609 more uniform default logic, using settings, options, args etc.; clarified build_dialog -C: imitate jEdit logic selection more precisely; diff -r 923f1e199f4f -r 87868964733c lib/Tools/build_dialog --- a/lib/Tools/build_dialog Thu Dec 06 16:07:09 2012 +0100 +++ b/lib/Tools/build_dialog Thu Dec 06 17:59:37 2012 +0100 @@ -16,6 +16,7 @@ echo echo " Options are:" echo " -C check for existing image" + echo " -L OPTION default logic via system option" echo " -d DIR include session directory" echo " -s system build mode: produce output in ISABELLE_HOME" echo @@ -34,15 +35,19 @@ ## process command line CHECK_EXISTING=false +LOGIC_OPTION="" declare -a INCLUDE_DIRS=() SYSTEM_MODE=false -while getopts "Cd:s" OPT +while getopts "CL:d:s" OPT do case "$OPT" in C) CHECK_EXISTING="true" ;; + L) + LOGIC_OPTION="$OPTARG" + ;; d) INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG" ;; @@ -65,27 +70,10 @@ SESSION="$1"; shift -## existing image +## main -EXISTING=false -if [ "$CHECK_EXISTING" = true ]; then - declare -a ISABELLE_PATHS=() - splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}") +[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } - for DIR in "${ISABELLE_PATHS[@]}" - do - FILE="$DIR/$ML_IDENTIFIER/$SESSION" - [ -f "$FILE" ] && EXISTING=true - done -fi - +"$ISABELLE_TOOL" java isabelle.Build_Dialog \ + "$CHECK_EXISTING" "$LOGIC_OPTION" "$SYSTEM_MODE" "$SESSION" "${INCLUDE_DIRS[@]}" -## build - -if [ "$EXISTING" = false ]; then - [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } - - "$ISABELLE_TOOL" java isabelle.Build_Dialog \ - "$SYSTEM_MODE" "$SESSION" "${INCLUDE_DIRS[@]}" -fi - diff -r 923f1e199f4f -r 87868964733c src/Pure/System/build_dialog.scala --- a/src/Pure/System/build_dialog.scala Thu Dec 06 16:07:09 2012 +0100 +++ b/src/Pure/System/build_dialog.scala Thu Dec 06 17:59:37 2012 +0100 @@ -16,6 +16,7 @@ object Build_Dialog extends SwingApplication { + // FIXME avoid startup via GUI thread!? def startup(args: Array[String]) = { Platform.init_laf() @@ -23,13 +24,28 @@ try { args.toList match { case + Properties.Value.Boolean(check_existing) :: + logic_option :: Properties.Value.Boolean(system_mode) :: - session :: include_dirs => - val center = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint() - val top = build_dialog(system_mode, include_dirs.map(Path.explode), session) - top.pack() - top.location = new Point(center.x - top.size.width / 2, center.y - top.size.height / 2) - top.visible = true + session_arg :: + include_dirs => + val session = + Isabelle_System.default_logic(session_arg, + if (logic_option != "") Options.init().string(logic_option) else "") + + val no_dialog = // FIXME full up-to-date test!? + check_existing && + Isabelle_System.find_logics_dirs().exists(dir => + (dir + Path.basic(session)).is_file) + + if (no_dialog) sys.exit(0) + else { + val center = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint() + val top = build_dialog(system_mode, include_dirs.map(Path.explode), session) + top.pack() + top.location = new Point(center.x - top.size.width / 2, center.y - top.size.height / 2) + top.visible = true + } case _ => error("Bad arguments:\n" + cat_lines(args)) } } diff -r 923f1e199f4f -r 87868964733c src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Dec 06 16:07:09 2012 +0100 +++ b/src/Pure/System/isabelle_system.scala Thu Dec 06 17:59:37 2012 +0100 @@ -273,7 +273,7 @@ Path.split(getenv_strict("ISABELLE_COMPONENTS")) - /* find logics */ + /* logic images */ def find_logics_dirs(): List[Path] = { @@ -287,6 +287,14 @@ files = dir.file.listFiles() if files != null file <- files.toList if file.isFile } yield file.getName).sorted + def default_logic(args: String*): String = + { + args.find(_ != "") match { + case Some(logic) => logic + case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC") + } + } + /* fonts */ diff -r 923f1e199f4f -r 87868964733c src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Thu Dec 06 16:07:09 2012 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Dec 06 17:59:37 2012 +0100 @@ -68,7 +68,7 @@ echo " -f fresh build" echo " -j OPTION add jEdit runtime option" echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" - echo " -l NAME logic session name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)" + echo " -l NAME logic session name" echo " -m MODE add print mode for output" echo " -s system build mode for session image" echo @@ -99,7 +99,7 @@ BUILD_ONLY=false BUILD_JARS="jars" JEDIT_SESSION_DIRS="" -JEDIT_LOGIC="$ISABELLE_LOGIC" +JEDIT_LOGIC="" JEDIT_PRINT_MODE="" function getoptions() @@ -313,7 +313,7 @@ # build logic -"$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -C "$JEDIT_LOGIC" +"$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -C -L jedit_logic "$JEDIT_LOGIC" RC="$?" [ "$RC" = 0 ] || exit "$RC" diff -r 923f1e199f4f -r 87868964733c src/Tools/jEdit/src/isabelle_logic.scala --- a/src/Tools/jEdit/src/isabelle_logic.scala Thu Dec 06 16:07:09 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Thu Dec 06 17:59:37 2012 +0100 @@ -15,26 +15,24 @@ object Isabelle_Logic { - private def default_logic(): String = - { - val logic = Isabelle_System.getenv("JEDIT_LOGIC") - if (logic != "") logic - else Isabelle_System.getenv_strict("ISABELLE_LOGIC") - } + private val option_name = "jedit_logic" + + private def jedit_logic(): String = + Isabelle_System.default_logic( + Isabelle_System.getenv("JEDIT_LOGIC"), + PIDE.options.string(option_name)) private class Logic_Entry(val name: String, val description: String) { override def toString = description } - private val option_name = "jedit_logic" - def logic_selector(autosave: Boolean): Option_Component = { Swing_Thread.require() val entries = - new Logic_Entry("", "default (" + default_logic() + ")") :: + new Logic_Entry("", "default (" + jedit_logic() + ")") :: Isabelle_Logic.session_list().map(name => new Logic_Entry(name, name)) val component = new ComboBox(entries) with Option_Component { @@ -63,12 +61,7 @@ def session_args(): List[String] = { val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _) - val logic = - PIDE.options.string(option_name) match { - case "" => default_logic() - case logic => logic - } - modes ::: List(logic) + modes ::: List(jedit_logic()) } def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))