more uniform default logic, using settings, options, args etc.;
clarified build_dialog -C: imitate jEdit logic selection more precisely;
--- 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
-
--- 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))
}
}
--- 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 */
--- 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"
--- 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"))