# HG changeset patch
# User wenzelm
# Date 1527507343 -7200
# Node ID 5321218147d353a0e683ba9c2170ff176675e7d1
# Parent  09270aa4088476ce709a20a92dd14a857c04cd7f
clarified signature;

diff -r 09270aa40884 -r 5321218147d3 src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Mon May 28 11:15:17 2018 +0200
+++ b/src/Pure/ML/ml_console.scala	Mon May 28 13:35:43 2018 +0200
@@ -50,19 +50,13 @@
       if (!more_args.isEmpty) getopts.usage()
 
 
-      // build
-      if (!no_build && !raw_ml_system &&
-          !Build.build(options, build_heap = true, no_build = true,
-            dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
-      {
+      // build logic
+      if (!no_build && !raw_ml_system) {
         val progress = new Console_Progress()
-        progress.echo("Build started for Isabelle/" + logic + " ...")
-        progress.interrupt_handler {
-          val res =
-            Build.build(options, progress = progress, build_heap = true,
-              dirs = dirs, system_mode = system_mode, sessions = List(logic))
-          if (!res.ok) sys.exit(res.rc)
-        }
+        val rc =
+          Build.build_logic(options, logic, build_heap = true, progress = progress,
+            dirs = dirs, system_mode = system_mode)
+        if (rc != 0) sys.exit(rc)
       }
 
       // process loop
diff -r 09270aa40884 -r 5321218147d3 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Mon May 28 11:15:17 2018 +0200
+++ b/src/Pure/System/progress.scala	Mon May 28 13:35:43 2018 +0200
@@ -23,6 +23,7 @@
     Timing.timeit(message, enabled, echo(_))(e)
 
   def stopped: Boolean = false
+  def interrupt_handler[A](e: => A): A = e
   def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
 
@@ -53,7 +54,8 @@
     if (verbose) echo(session + ": theory " + theory)
 
   @volatile private var is_stopped = false
-  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
+  override def interrupt_handler[A](e: => A): A =
+    POSIX_Interrupt.handler { is_stopped = true } { e }
   override def stopped: Boolean =
   {
     if (Thread.interrupted) is_stopped = true
diff -r 09270aa40884 -r 5321218147d3 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon May 28 11:15:17 2018 +0200
+++ b/src/Pure/Thy/export.scala	Mon May 28 13:35:43 2018 +0200
@@ -281,22 +281,16 @@
         case _ => getopts.usage()
       }
 
+    val progress = new Console_Progress()
+
 
     /* build */
 
-    val progress = new Console_Progress()
-
-    if (!no_build &&
-        !Build.build(options, no_build = true, dirs = dirs, system_mode = system_mode,
-          sessions = List(session_name)).ok)
-    {
-      progress.echo("Build started for Isabelle/" + session_name + " ...")
-      progress.interrupt_handler {
-        val res =
-          Build.build(options, progress = progress, dirs = dirs, system_mode = system_mode,
-            sessions = List(session_name))
-        if (!res.ok) sys.exit(res.rc)
-      }
+    if (!no_build) {
+      val rc =
+        Build.build_logic(options, session_name, progress = progress,
+          dirs = dirs, system_mode = system_mode)
+      if (rc != 0) sys.exit(rc)
     }
 
 
diff -r 09270aa40884 -r 5321218147d3 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon May 28 11:15:17 2018 +0200
+++ b/src/Pure/Tools/build.scala	Mon May 28 13:35:43 2018 +0200
@@ -822,4 +822,24 @@
 
     sys.exit(results.rc)
   })
+
+
+  /* build logic image */
+
+  def build_logic(options: Options, logic: String,
+    progress: Progress = No_Progress,
+    build_heap: Boolean = false,
+    dirs: List[Path] = Nil,
+    system_mode: Boolean = false): Int =
+  {
+    if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
+        system_mode = system_mode, sessions = List(logic)).ok) 0
+    else {
+      progress.echo("Build started for Isabelle/" + logic + " ...")
+      progress.interrupt_handler {
+        Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
+          system_mode = system_mode, sessions = List(logic)).rc
+      }
+    }
+  }
 }