src/Pure/Tools/build_console.scala
author wenzelm
Sun Jul 20 17:54:01 2014 +0200 (2014-07-20)
changeset 57581 74bbe9317aa4
parent 57580 86b413b8f779
child 60518 a79f89a36dff
permissions -rw-r--r--
provide explicit options file -- 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           options_file ::
    44           Command_Line.Chunks(dirs, system_options) =>
    45             val options = (Options.init() /: system_options)(_ + _)
    46             File.write(Path.explode(options_file), YXML.string_of_body(options.encode))
    47 
    48             val progress = new Build.Console_Progress()
    49             progress.interrupt_handler {
    50               build_console(options, progress,
    51                 dirs.map(Path.explode(_)), no_build, system_mode, session)
    52             }
    53         case _ => error("Bad arguments:\n" + cat_lines(args))
    54       }
    55     }
    56   }
    57 }
    58