fewer options;
authorwenzelm
Fri Jul 27 13:15:12 2012 +0200 (2012-07-27)
changeset 48545c168bc64f2a8
parent 48544 8c26657e73c3
child 48546 f81cf2fcd3a0
fewer options;
lib/Tools/build
src/Pure/System/build.ML
src/Pure/System/build.scala
     1.1 --- a/lib/Tools/build	Fri Jul 27 13:08:46 2012 +0200
     1.2 +++ b/lib/Tools/build	Fri Jul 27 13:15:12 2012 +0200
     1.3 @@ -34,7 +34,6 @@
     1.4    echo "    -n           no build -- test dependencies only"
     1.5    echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
     1.6    echo "    -s           system build mode: produce output in ISABELLE_HOME"
     1.7 -  echo "    -t           inner session timing"
     1.8    echo "    -v           verbose"
     1.9    echo
    1.10    echo "  Build and manage Isabelle sessions, depending on implicit"
    1.11 @@ -65,10 +64,9 @@
    1.12  NO_BUILD=false
    1.13  eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    1.14  SYSTEM_MODE=false
    1.15 -TIMING=false
    1.16  VERBOSE=false
    1.17  
    1.18 -while getopts "abd:g:j:no:stv" OPT
    1.19 +while getopts "abd:g:j:no:sv" OPT
    1.20  do
    1.21    case "$OPT" in
    1.22      a)
    1.23 @@ -96,9 +94,6 @@
    1.24      s)
    1.25        SYSTEM_MODE="true"
    1.26        ;;
    1.27 -    t)
    1.28 -      TIMING="true"
    1.29 -      ;;
    1.30      v)
    1.31        VERBOSE="true"
    1.32        ;;
    1.33 @@ -126,7 +121,7 @@
    1.34  fi
    1.35  
    1.36  "$ISABELLE_TOOL" java isabelle.Build \
    1.37 -  "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \
    1.38 +  "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
    1.39    "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
    1.40  RC="$?"
    1.41  
     2.1 --- a/src/Pure/System/build.ML	Fri Jul 27 13:08:46 2012 +0200
     2.2 +++ b/src/Pure/System/build.ML	Fri Jul 27 13:15:12 2012 +0200
     2.3 @@ -56,12 +56,12 @@
     2.4  
     2.5  fun build args_file =
     2.6    let
     2.7 -    val (do_output, (options, (timing, (verbose, (browser_info, (parent_name,
     2.8 -        (name, theories))))))) =
     2.9 +    val (do_output, (options, (verbose, (browser_info, (parent_name,
    2.10 +        (name, theories)))))) =
    2.11        File.read (Path.explode args_file) |> YXML.parse_body |>
    2.12          let open XML.Decode in
    2.13 -          pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
    2.14 -            (pair string ((list (pair Options.decode (list string))))))))))
    2.15 +          pair bool (pair Options.decode (pair bool (pair string (pair string
    2.16 +            (pair string ((list (pair Options.decode (list string)))))))))
    2.17          end;
    2.18  
    2.19      val _ =
    2.20 @@ -74,7 +74,7 @@
    2.21          (Options.string options "document_dump",
    2.22            Present.dump_mode (Options.string options "document_dump_mode"))
    2.23          "" verbose;
    2.24 -    val _ = Session.with_timing name timing (List.app use_theories) theories;
    2.25 +    val _ = Session.with_timing name verbose (List.app use_theories) theories;
    2.26      val _ = Session.finish ();
    2.27      val _ = if do_output then () else quit ();
    2.28    in () end
     3.1 --- a/src/Pure/System/build.scala	Fri Jul 27 13:08:46 2012 +0200
     3.2 +++ b/src/Pure/System/build.scala	Fri Jul 27 13:15:12 2012 +0200
     3.3 @@ -334,7 +334,7 @@
     3.4    }
     3.5  
     3.6    private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean,
     3.7 -    options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job =
     3.8 +    options: Options, verbose: Boolean, browser_info: Path): Job =
     3.9    {
    3.10      // global browser info dir
    3.11      if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
    3.12 @@ -385,10 +385,10 @@
    3.13      val args_xml =
    3.14      {
    3.15        import XML.Encode._
    3.16 -          pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
    3.17 -            pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
    3.18 -          (do_output, (options, (timing, (verbose, (browser_info, (parent,
    3.19 -            (name, info.theories))))))))
    3.20 +          pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
    3.21 +            pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
    3.22 +          (do_output, (options, (verbose, (browser_info, (parent,
    3.23 +            (name, info.theories)))))))
    3.24      }
    3.25      new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output)
    3.26    }
    3.27 @@ -441,7 +441,6 @@
    3.28      no_build: Boolean = false,
    3.29      build_options: List[String] = Nil,
    3.30      system_mode: Boolean = false,
    3.31 -    timing: Boolean = false,
    3.32      verbose: Boolean = false,
    3.33      sessions: List[String] = Nil): Int =
    3.34    {
    3.35 @@ -526,7 +525,7 @@
    3.36              else if (parent_ok) {
    3.37                echo((if (do_output) "Building " else "Running ") + name + " ...")
    3.38                val job =
    3.39 -                start_job(name, info, output, do_output, info.options, timing, verbose, browser_info)
    3.40 +                start_job(name, info, output, do_output, info.options, verbose, browser_info)
    3.41                loop(pending, running + (name -> job), results)
    3.42              }
    3.43              else {
    3.44 @@ -561,11 +560,10 @@
    3.45            Properties.Value.Int(max_jobs) ::
    3.46            Properties.Value.Boolean(no_build) ::
    3.47            Properties.Value.Boolean(system_mode) ::
    3.48 -          Properties.Value.Boolean(timing) ::
    3.49            Properties.Value.Boolean(verbose) ::
    3.50            Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
    3.51              build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
    3.52 -              max_jobs, no_build, build_options, system_mode, timing, verbose, sessions)
    3.53 +              max_jobs, no_build, build_options, system_mode, verbose, sessions)
    3.54          case _ => error("Bad arguments:\n" + cat_lines(args))
    3.55        }
    3.56      }