prefer internal tool;
authorwenzelm
Sun Apr 03 22:42:15 2016 +0200 (2016-04-03)
changeset 6283329dfa2ed9343
parent 62832 c1410bcf6e87
child 62834 970cedec9748
prefer internal tool;
lib/Tools/build
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/build.scala
     1.1 --- a/lib/Tools/build	Sun Apr 03 22:36:11 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,20 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# Author: Makarius
     1.7 -#
     1.8 -# DESCRIPTION: build and manage Isabelle sessions
     1.9 -
    1.10 -isabelle_admin_build jars || exit $?
    1.11 -
    1.12 -case "$ISABELLE_JAVA_PLATFORM" in
    1.13 -  x86-*)
    1.14 -    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
    1.15 -    ;;
    1.16 -  x86_64-*)
    1.17 -    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
    1.18 -    ;;
    1.19 -esac
    1.20 -
    1.21 -eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
    1.22 -
    1.23 -exec isabelle java "${JAVA_ARGS[@]}" isabelle.Build "$@"
     2.1 --- a/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:36:11 2016 +0200
     2.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:42:15 2016 +0200
     2.3 @@ -68,6 +68,7 @@
     2.4              args => Command_Line.tool0 { isabelle_tool.body(args) }))
     2.5      }
     2.6  
     2.7 +  register(Build.isabelle_tool)
     2.8    register(Doc.isabelle_tool)
     2.9    register(Options.isabelle_tool)
    2.10  
     3.1 --- a/src/Pure/Tools/build.scala	Sun Apr 03 22:36:11 2016 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Sun Apr 03 22:42:15 2016 +0200
     3.3 @@ -685,43 +685,42 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* command line entry point */
     3.8 +  /* Isabelle tool wrapper */
     3.9  
    3.10 -  def main(args: Array[String])
    3.11 +  val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
    3.12    {
    3.13 -    Command_Line.tool {
    3.14 -      def show_settings(): String =
    3.15 -        cat_lines(List(
    3.16 -          "ISABELLE_BUILD_OPTIONS=" +
    3.17 -            quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
    3.18 -          "ISABELLE_BUILD_JAVA_OPTIONS=" +
    3.19 -            quote(Isabelle_System.getenv("ISABELLE_BUILD_JAVA_OPTIONS")),
    3.20 -          "",
    3.21 -          "ML_PLATFORM=" + quote(Isabelle_System.getenv("ML_PLATFORM")),
    3.22 -          "ML_HOME=" + quote(Isabelle_System.getenv("ML_HOME")),
    3.23 -          "ML_SYSTEM=" + quote(Isabelle_System.getenv("ML_SYSTEM")),
    3.24 -          "ML_OPTIONS=" + quote(Isabelle_System.getenv("ML_OPTIONS"))))
    3.25 +    def show_settings(): String =
    3.26 +      cat_lines(List(
    3.27 +        "ISABELLE_BUILD_OPTIONS=" +
    3.28 +          quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
    3.29 +        "ISABELLE_BUILD_JAVA_OPTIONS=" +
    3.30 +          quote(Isabelle_System.getenv("ISABELLE_BUILD_JAVA_OPTIONS")),
    3.31 +        "",
    3.32 +        "ML_PLATFORM=" + quote(Isabelle_System.getenv("ML_PLATFORM")),
    3.33 +        "ML_HOME=" + quote(Isabelle_System.getenv("ML_HOME")),
    3.34 +        "ML_SYSTEM=" + quote(Isabelle_System.getenv("ML_SYSTEM")),
    3.35 +        "ML_OPTIONS=" + quote(Isabelle_System.getenv("ML_OPTIONS"))))
    3.36  
    3.37 -      val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
    3.38 +    val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
    3.39  
    3.40 -      var select_dirs: List[Path] = Nil
    3.41 -      var requirements = false
    3.42 -      var exclude_session_groups: List[String] = Nil
    3.43 -      var all_sessions = false
    3.44 -      var build_heap = false
    3.45 -      var clean_build = false
    3.46 -      var dirs: List[Path] = Nil
    3.47 -      var session_groups: List[String] = Nil
    3.48 -      var max_jobs = 1
    3.49 -      var check_keywords: Set[String] = Set.empty
    3.50 -      var list_files = false
    3.51 -      var no_build = false
    3.52 -      var options = (Options.init() /: build_options)(_ + _)
    3.53 -      var system_mode = false
    3.54 -      var verbose = false
    3.55 -      var exclude_sessions: List[String] = Nil
    3.56 +    var select_dirs: List[Path] = Nil
    3.57 +    var requirements = false
    3.58 +    var exclude_session_groups: List[String] = Nil
    3.59 +    var all_sessions = false
    3.60 +    var build_heap = false
    3.61 +    var clean_build = false
    3.62 +    var dirs: List[Path] = Nil
    3.63 +    var session_groups: List[String] = Nil
    3.64 +    var max_jobs = 1
    3.65 +    var check_keywords: Set[String] = Set.empty
    3.66 +    var list_files = false
    3.67 +    var no_build = false
    3.68 +    var options = (Options.init() /: build_options)(_ + _)
    3.69 +    var system_mode = false
    3.70 +    var verbose = false
    3.71 +    var exclude_sessions: List[String] = Nil
    3.72  
    3.73 -      val getopts = Getopts("""
    3.74 +    val getopts = Getopts("""
    3.75  Usage: isabelle build [OPTIONS] [SESSIONS ...]
    3.76  
    3.77    Options are:
    3.78 @@ -745,58 +744,57 @@
    3.79    Build and manage Isabelle sessions, depending on implicit settings:
    3.80  
    3.81  """ + Library.prefix_lines("  ", show_settings()),
    3.82 -        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    3.83 -        "R" -> (_ => requirements = true),
    3.84 -        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    3.85 -        "a" -> (_ => all_sessions = true),
    3.86 -        "b" -> (_ => build_heap = true),
    3.87 -        "c" -> (_ => clean_build = true),
    3.88 -        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    3.89 -        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
    3.90 -        "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
    3.91 -        "k:" -> (arg => check_keywords = check_keywords + arg),
    3.92 -        "l" -> (_ => list_files = true),
    3.93 -        "n" -> (_ => no_build = true),
    3.94 -        "o:" -> (arg => options = options + arg),
    3.95 -        "s" -> (_ => system_mode = true),
    3.96 -        "v" -> (_ => verbose = true),
    3.97 -        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
    3.98 +      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    3.99 +      "R" -> (_ => requirements = true),
   3.100 +      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   3.101 +      "a" -> (_ => all_sessions = true),
   3.102 +      "b" -> (_ => build_heap = true),
   3.103 +      "c" -> (_ => clean_build = true),
   3.104 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   3.105 +      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   3.106 +      "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
   3.107 +      "k:" -> (arg => check_keywords = check_keywords + arg),
   3.108 +      "l" -> (_ => list_files = true),
   3.109 +      "n" -> (_ => no_build = true),
   3.110 +      "o:" -> (arg => options = options + arg),
   3.111 +      "s" -> (_ => system_mode = true),
   3.112 +      "v" -> (_ => verbose = true),
   3.113 +      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   3.114  
   3.115 -      val sessions = getopts(args)
   3.116 +    val sessions = getopts(args)
   3.117  
   3.118 -      val progress = new Console_Progress(verbose)
   3.119 +    val progress = new Console_Progress(verbose)
   3.120  
   3.121 -      if (verbose) {
   3.122 -        progress.echo(
   3.123 -          Library.trim_line(
   3.124 -            Isabelle_System.bash(
   3.125 -              """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
   3.126 -        progress.echo(show_settings() + "\n")
   3.127 -      }
   3.128 +    if (verbose) {
   3.129 +      progress.echo(
   3.130 +        Library.trim_line(
   3.131 +          Isabelle_System.bash(
   3.132 +            """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
   3.133 +      progress.echo(show_settings() + "\n")
   3.134 +    }
   3.135  
   3.136 -      val start_time = Time.now()
   3.137 -      val results =
   3.138 -        progress.interrupt_handler {
   3.139 -          build(options, progress, requirements, all_sessions, build_heap, clean_build,
   3.140 -            dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
   3.141 -            check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
   3.142 -        }
   3.143 -      val elapsed_time = Time.now() - start_time
   3.144 +    val start_time = Time.now()
   3.145 +    val results =
   3.146 +      progress.interrupt_handler {
   3.147 +        build(options, progress, requirements, all_sessions, build_heap, clean_build,
   3.148 +          dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
   3.149 +          check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
   3.150 +      }
   3.151 +    val elapsed_time = Time.now() - start_time
   3.152  
   3.153 -      if (verbose) {
   3.154 -        progress.echo("\n" +
   3.155 -          Library.trim_line(
   3.156 -            Isabelle_System.bash("""echo -n "Finished at "; date""").out))
   3.157 -      }
   3.158 +    if (verbose) {
   3.159 +      progress.echo("\n" +
   3.160 +        Library.trim_line(
   3.161 +          Isabelle_System.bash("""echo -n "Finished at "; date""").out))
   3.162 +    }
   3.163  
   3.164 -      val total_timing =
   3.165 -        (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   3.166 -          copy(elapsed = elapsed_time)
   3.167 -      progress.echo(total_timing.message_resources)
   3.168 +    val total_timing =
   3.169 +      (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   3.170 +        copy(elapsed = elapsed_time)
   3.171 +    progress.echo(total_timing.message_resources)
   3.172  
   3.173 -      results.rc
   3.174 -    }
   3.175 -  }
   3.176 +    sys.exit(results.rc)
   3.177 +  })
   3.178  
   3.179  
   3.180    /* PIDE protocol */