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