clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
added jedit option -n to bypass build_dialog;

--- a/lib/Tools/build_dialog	Thu Dec 06 20:26:14 2012 +0100
+++ b/lib/Tools/build_dialog	Thu Dec 06 21:16:46 2012 +0100
@@ -15,7 +15,6 @@
   echo "Usage: isabelle $PRG [OPTIONS] LOGIC"
   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"
@@ -34,17 +33,13 @@
 
 ## process command line
 
-CHECK_EXISTING=false
 LOGIC_OPTION=""
 declare -a INCLUDE_DIRS=()
 SYSTEM_MODE=false
 
-while getopts "CL:d:s" OPT
+while getopts "L:d:s" OPT
 do
   case "$OPT" in
-    C)
-      CHECK_EXISTING="true"
-      ;;
     L)
       LOGIC_OPTION="$OPTARG"
       ;;
@@ -75,5 +70,5 @@
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
 "$ISABELLE_TOOL" java isabelle.Build_Dialog \
-  "$CHECK_EXISTING" "$LOGIC_OPTION" "$SYSTEM_MODE" "$LOGIC" "${INCLUDE_DIRS[@]}"
+  "$LOGIC_OPTION" "$SYSTEM_MODE" "$LOGIC" "${INCLUDE_DIRS[@]}"
 

--- a/src/Pure/System/build_dialog.scala	Thu Dec 06 20:26:14 2012 +0100
+++ b/src/Pure/System/build_dialog.scala	Thu Dec 06 21:16:46 2012 +0100
@@ -21,29 +21,24 @@
     try {
       args.toList match {
         case
-          Properties.Value.Boolean(check_existing) ::
           logic_option ::
           Properties.Value.Boolean(system_mode) ::
           logic ::
           include_dirs =>
-            val dirs = include_dirs.map(Path.explode)
+            val more_dirs = include_dirs.map(s => ((false, Path.explode(s))))
 
             val options = Options.init()
             val session =
               Isabelle_System.default_logic(logic,
                 if (logic_option != "") options.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)
+            if (Build.build(Build.Ignore_Progress, options, no_build = true,
+                more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0)
             else
               Swing_Thread.later {
                 Platform.init_laf()
 
-                val top = build_dialog(options, system_mode, dirs, session)
+                val top = build_dialog(options, system_mode, more_dirs, session)
                 top.pack()
 
                 val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
@@ -66,7 +61,7 @@
   def build_dialog(
     options: Options,
     system_mode: Boolean,
-    dirs: List[Path],
+    more_dirs: List[(Boolean, Path)],
     session: String): MainFrame = new MainFrame
   {
     /* GUI state */
@@ -126,7 +121,7 @@
       val (out, rc) =
         try {
           ("",
-            Build.build(progress, options, build_heap = true, more_dirs = dirs.map((false, _)),
+            Build.build(progress, options, build_heap = true, more_dirs = more_dirs,
               system_mode = system_mode, sessions = List(session)))
         }
         catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }

--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Dec 06 20:26:14 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Dec 06 21:16:46 2012 +0100
@@ -70,6 +70,7 @@
   echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
   echo "    -l NAME      logic session name"
   echo "    -m MODE      add print mode for output"
+  echo "    -n           no build dialog for session image on startup"
   echo "    -s           system build mode for session image"
   echo
   echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
@@ -101,11 +102,12 @@
 JEDIT_SESSION_DIRS=""
 JEDIT_LOGIC=""
 JEDIT_PRINT_MODE=""
+NO_BUILD="false"
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "J:bd:fj:l:m:s" OPT
+  while getopts "J:bd:fj:l:m:ns" OPT
   do
     case "$OPT" in
       J)
@@ -139,6 +141,9 @@
           JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
         fi
         ;;
+      n)
+        NO_BUILD="true"
+        ;;
       s)
         BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-s"
         ;;
@@ -313,9 +318,11 @@
 
 # build logic
 
-"$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -C -L jedit_logic "$JEDIT_LOGIC"
-RC="$?"
-[ "$RC" = 0 ] || exit "$RC"
+if [ "$NO_BUILD" = false ]; then
+  "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -L jedit_logic "$JEDIT_LOGIC"
+  RC="$?"
+  [ "$RC" = 0 ] || exit "$RC"
+fi
 
 
 # main