# HG changeset patch
# User wenzelm
# Date 1405869674 -7200
# Node ID 86b413b8f779522f62e2099349017f26a3611657
# Parent  c1e24d017918dcac97a614791d089630eafe6b37
check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;

diff -r c1e24d017918 -r 86b413b8f779 lib/Tools/console
--- a/lib/Tools/console	Sat Jul 19 21:32:54 2014 +0200
+++ b/lib/Tools/console	Sun Jul 20 17:21:14 2014 +0200
@@ -31,17 +31,18 @@
 # options
 
 declare -a ISABELLE_OPTIONS=()
+
+declare -a INCLUDE_DIRS=()
+LOGIC="$ISABELLE_LOGIC"
+NO_BUILD="false"
 declare -a BUILD_OPTIONS=()
-
-LOGIC="$ISABELLE_LOGIC"
-DO_BUILD="true"
+SYSTEM_MODE="false"
 
 while getopts "d:l:m:no:s" OPT
 do
   case "$OPT" in
     d)
-      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="-d"
-      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
+      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
       ;;
     l)
       LOGIC="$OPTARG"
@@ -51,16 +52,15 @@
       ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
       ;;
     n)
-      DO_BUILD="false"
+      NO_BUILD="true"
       ;;
     o)
       ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-o"
       ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
-      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="-o"
       BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
       ;;
     s)
-      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="-s"
+      SYSTEM_MODE="true"
       ;;
     \?)
       usage
@@ -78,14 +78,13 @@
 
 ## main
 
-if [ "$DO_BUILD" = true ]
-then
-  "$ISABELLE_TOOL" build -b -n "${BUILD_OPTIONS[@]}" "$LOGIC" >/dev/null 2>/dev/null ||
-  {
-    echo "Build started for Isabelle/$LOGIC"
-    "$ISABELLE_TOOL" build -b "${BUILD_OPTIONS[@]}" "$LOGIC" || exit "$?"
-  }
-fi
+isabelle_admin_build jars || exit $?
+
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
+
+"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
+  "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" \
+  "${INCLUDE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" || exit "$?"
 
 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
 then
diff -r c1e24d017918 -r 86b413b8f779 src/Pure/Tools/build_console.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/build_console.scala	Sun Jul 20 17:21:14 2014 +0200
@@ -0,0 +1,55 @@
+/*  Title:      Pure/Tools/build_console.scala
+    Author:     Makarius
+
+Check and build Isabelle session for console tool.
+*/
+
+package isabelle
+
+
+object Build_Console
+{
+  /* build_console */
+
+  def build_console(
+    options: Options,
+    progress: Build.Progress = Build.Ignore_Progress,
+    dirs: List[Path] = Nil,
+    no_build: Boolean = false,
+    system_mode: Boolean = false,
+    session: String): Int =
+  {
+    if (no_build ||
+        Build.build(options = options, build_heap = true, no_build = true,
+          dirs = dirs, sessions = List(session)) == 0) 0
+    else {
+      progress.echo("Build started for Isabelle/" + session + " ...")
+      Build.build(options = options, progress = progress, build_heap = true,
+        dirs = dirs, system_mode = system_mode, sessions = List(session))
+    }
+  }
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool {
+      args.toList match {
+        case
+          session ::
+          Properties.Value.Boolean(no_build) ::
+          Properties.Value.Boolean(system_mode) ::
+          Command_Line.Chunks(dirs, build_options) =>
+            val options = (Options.init() /: build_options)(_ + _)
+            val progress = new Build.Console_Progress()
+            progress.interrupt_handler {
+              build_console(options, progress,
+                dirs.map(Path.explode(_)), no_build, system_mode, session)
+            }
+        case _ => error("Bad arguments:\n" + cat_lines(args))
+      }
+    }
+  }
+}
+
diff -r c1e24d017918 -r 86b413b8f779 src/Pure/build-jars
--- a/src/Pure/build-jars	Sat Jul 19 21:32:54 2014 +0200
+++ b/src/Pure/build-jars	Sun Jul 20 17:21:14 2014 +0200
@@ -86,6 +86,7 @@
   Tools/check_source.scala
   Tools/build.scala
   Tools/build_doc.scala
+  Tools/build_console.scala
   Tools/doc.scala
   Tools/keywords.scala
   Tools/main.scala