src/Pure/Tools/build_console.scala
author wenzelm
Sun Jul 20 17:21:14 2014 +0200 (2014-07-20)
changeset 57580 86b413b8f779
child 57581 74bbe9317aa4
permissions -rw-r--r--
check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;
     1 /*  Title:      Pure/Tools/build_console.scala
     2     Author:     Makarius
     3 
     4 Check and build Isabelle session for console tool.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Build_Console
    11 {
    12   /* build_console */
    13 
    14   def build_console(
    15     options: Options,
    16     progress: Build.Progress = Build.Ignore_Progress,
    17     dirs: List[Path] = Nil,
    18     no_build: Boolean = false,
    19     system_mode: Boolean = false,
    20     session: String): Int =
    21   {
    22     if (no_build ||
    23         Build.build(options = options, build_heap = true, no_build = true,
    24           dirs = dirs, sessions = List(session)) == 0) 0
    25     else {
    26       progress.echo("Build started for Isabelle/" + session + " ...")
    27       Build.build(options = options, progress = progress, build_heap = true,
    28         dirs = dirs, system_mode = system_mode, sessions = List(session))
    29     }
    30   }
    31 
    32 
    33   /* command line entry point */
    34 
    35   def main(args: Array[String])
    36   {
    37     Command_Line.tool {
    38       args.toList match {
    39         case
    40           session ::
    41           Properties.Value.Boolean(no_build) ::
    42           Properties.Value.Boolean(system_mode) ::
    43           Command_Line.Chunks(dirs, build_options) =>
    44             val options = (Options.init() /: build_options)(_ + _)
    45             val progress = new Build.Console_Progress()
    46             progress.interrupt_handler {
    47               build_console(options, progress,
    48                 dirs.map(Path.explode(_)), no_build, system_mode, session)
    49             }
    50         case _ => error("Bad arguments:\n" + cat_lines(args))
    51       }
    52     }
    53   }
    54 }
    55