clarified signature;
authorwenzelm
Mon May 28 13:35:43 2018 +0200 (13 months ago)
changeset 683055321218147d3
parent 68304 09270aa40884
child 68306 d575281e18d0
clarified signature;
src/Pure/ML/ml_console.scala
src/Pure/System/progress.scala
src/Pure/Thy/export.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/ML/ml_console.scala	Mon May 28 11:15:17 2018 +0200
     1.2 +++ b/src/Pure/ML/ml_console.scala	Mon May 28 13:35:43 2018 +0200
     1.3 @@ -50,19 +50,13 @@
     1.4        if (!more_args.isEmpty) getopts.usage()
     1.5  
     1.6  
     1.7 -      // build
     1.8 -      if (!no_build && !raw_ml_system &&
     1.9 -          !Build.build(options, build_heap = true, no_build = true,
    1.10 -            dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
    1.11 -      {
    1.12 +      // build logic
    1.13 +      if (!no_build && !raw_ml_system) {
    1.14          val progress = new Console_Progress()
    1.15 -        progress.echo("Build started for Isabelle/" + logic + " ...")
    1.16 -        progress.interrupt_handler {
    1.17 -          val res =
    1.18 -            Build.build(options, progress = progress, build_heap = true,
    1.19 -              dirs = dirs, system_mode = system_mode, sessions = List(logic))
    1.20 -          if (!res.ok) sys.exit(res.rc)
    1.21 -        }
    1.22 +        val rc =
    1.23 +          Build.build_logic(options, logic, build_heap = true, progress = progress,
    1.24 +            dirs = dirs, system_mode = system_mode)
    1.25 +        if (rc != 0) sys.exit(rc)
    1.26        }
    1.27  
    1.28        // process loop
     2.1 --- a/src/Pure/System/progress.scala	Mon May 28 11:15:17 2018 +0200
     2.2 +++ b/src/Pure/System/progress.scala	Mon May 28 13:35:43 2018 +0200
     2.3 @@ -23,6 +23,7 @@
     2.4      Timing.timeit(message, enabled, echo(_))(e)
     2.5  
     2.6    def stopped: Boolean = false
     2.7 +  def interrupt_handler[A](e: => A): A = e
     2.8    def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
     2.9    override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
    2.10  
    2.11 @@ -53,7 +54,8 @@
    2.12      if (verbose) echo(session + ": theory " + theory)
    2.13  
    2.14    @volatile private var is_stopped = false
    2.15 -  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
    2.16 +  override def interrupt_handler[A](e: => A): A =
    2.17 +    POSIX_Interrupt.handler { is_stopped = true } { e }
    2.18    override def stopped: Boolean =
    2.19    {
    2.20      if (Thread.interrupted) is_stopped = true
     3.1 --- a/src/Pure/Thy/export.scala	Mon May 28 11:15:17 2018 +0200
     3.2 +++ b/src/Pure/Thy/export.scala	Mon May 28 13:35:43 2018 +0200
     3.3 @@ -281,22 +281,16 @@
     3.4          case _ => getopts.usage()
     3.5        }
     3.6  
     3.7 +    val progress = new Console_Progress()
     3.8 +
     3.9  
    3.10      /* build */
    3.11  
    3.12 -    val progress = new Console_Progress()
    3.13 -
    3.14 -    if (!no_build &&
    3.15 -        !Build.build(options, no_build = true, dirs = dirs, system_mode = system_mode,
    3.16 -          sessions = List(session_name)).ok)
    3.17 -    {
    3.18 -      progress.echo("Build started for Isabelle/" + session_name + " ...")
    3.19 -      progress.interrupt_handler {
    3.20 -        val res =
    3.21 -          Build.build(options, progress = progress, dirs = dirs, system_mode = system_mode,
    3.22 -            sessions = List(session_name))
    3.23 -        if (!res.ok) sys.exit(res.rc)
    3.24 -      }
    3.25 +    if (!no_build) {
    3.26 +      val rc =
    3.27 +        Build.build_logic(options, session_name, progress = progress,
    3.28 +          dirs = dirs, system_mode = system_mode)
    3.29 +      if (rc != 0) sys.exit(rc)
    3.30      }
    3.31  
    3.32  
     4.1 --- a/src/Pure/Tools/build.scala	Mon May 28 11:15:17 2018 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Mon May 28 13:35:43 2018 +0200
     4.3 @@ -822,4 +822,24 @@
     4.4  
     4.5      sys.exit(results.rc)
     4.6    })
     4.7 +
     4.8 +
     4.9 +  /* build logic image */
    4.10 +
    4.11 +  def build_logic(options: Options, logic: String,
    4.12 +    progress: Progress = No_Progress,
    4.13 +    build_heap: Boolean = false,
    4.14 +    dirs: List[Path] = Nil,
    4.15 +    system_mode: Boolean = false): Int =
    4.16 +  {
    4.17 +    if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
    4.18 +        system_mode = system_mode, sessions = List(logic)).ok) 0
    4.19 +    else {
    4.20 +      progress.echo("Build started for Isabelle/" + logic + " ...")
    4.21 +      progress.interrupt_handler {
    4.22 +        Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
    4.23 +          system_mode = system_mode, sessions = List(logic)).rc
    4.24 +      }
    4.25 +    }
    4.26 +  }
    4.27  }