1.1 --- a/lib/Tools/build	Thu Jul 26 12:32:25 2012 +0200
     1.2 +++ b/lib/Tools/build	Thu Jul 26 12:59:09 2012 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    echo
     1.5    echo "  Options are:"
     1.6    echo "    -a           all sessions"
     1.7 -  echo "    -b           build target images"
     1.8 +  echo "    -b           build heap images"
     1.9    echo "    -d DIR       include session directory with ROOT file"
    1.10    echo "    -g NAME      include session group NAME"
    1.11    echo "    -j INT       maximum number of jobs (default 1)"
    1.12 @@ -58,7 +58,7 @@
    1.13  ## process command line
    1.14  
    1.15  ALL_SESSIONS=false
    1.16 -BUILD_IMAGES=false
    1.17 +BUILD_HEAP=false
    1.18  declare -a MORE_DIRS=()
    1.19  declare -a SESSION_GROUPS=()
    1.20  MAX_JOBS=1
    1.21 @@ -75,7 +75,7 @@
    1.22        ALL_SESSIONS="true"
    1.23        ;;
    1.24      b)
    1.25 -      BUILD_IMAGES="true"
    1.26 +      BUILD_HEAP="true"
    1.27        ;;
    1.28      d)
    1.29        MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
    1.30 @@ -126,7 +126,7 @@
    1.31  fi
    1.32  
    1.33  "$ISABELLE_TOOL" java isabelle.Build \
    1.34 -  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \
    1.35 +  "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \
    1.36    "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
    1.37  RC="$?"
    1.38  

     2.1 --- a/src/Pure/System/build.ML	Thu Jul 26 12:32:25 2012 +0200
     2.2 +++ b/src/Pure/System/build.ML	Thu Jul 26 12:59:09 2012 +0200
     2.3 @@ -50,7 +50,7 @@
     2.4  
     2.5  fun build args_file =
     2.6    let
     2.7 -    val (save, (options, (timing, (verbose, (browser_info, (parent_base_name,
     2.8 +    val (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
     2.9          (name, (base_name, theories)))))))) =
    2.10        File.read (Path.explode args_file) |> YXML.parse_body |>
    2.11          let open XML.Decode in
    2.12 @@ -59,7 +59,7 @@
    2.13          end;
    2.14  
    2.15      val _ =
    2.16 -      Session.init save false
    2.17 +      Session.init do_output false
    2.18          (Options.bool options "browser_info") browser_info
    2.19          (Options.string options "document")
    2.20          (Options.bool options "document_graph")
    2.21 @@ -70,7 +70,7 @@
    2.22          verbose;
    2.23      val _ = Session.with_timing name timing (List.app use_theories) theories;
    2.24      val _ = Session.finish ();
    2.25 -    val _ = if save then () else quit ();
    2.26 +    val _ = if do_output then () else quit ();
    2.27    in () end
    2.28    handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    2.29  

     3.1 --- a/src/Pure/System/build.scala	Thu Jul 26 12:32:25 2012 +0200
     3.2 +++ b/src/Pure/System/build.scala	Thu Jul 26 12:59:09 2012 +0200
     3.3 @@ -320,7 +320,7 @@
     3.4    /* jobs */
     3.5  
     3.6    private class Job(cwd: JFile, env: Map[String, String], script: String, args: String,
     3.7 -    val output_path: Option[Path])
     3.8 +    output: Path, do_output: Boolean)
     3.9    {
    3.10      private val args_file = File.tmp_file("args")
    3.11      private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
    3.12 @@ -332,9 +332,10 @@
    3.13      def terminate: Unit = thread.interrupt
    3.14      def is_finished: Boolean = result.is_finished
    3.15      def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
    3.16 +    def output_path: Option[Path] = if (do_output) Some(output) else None
    3.17    }
    3.18  
    3.19 -  private def start_job(name: String, info: Session.Info, output_path: Option[Path],
    3.20 +  private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean,
    3.21      options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job =
    3.22    {
    3.23      // global browser info dir
    3.24 @@ -352,21 +353,26 @@
    3.25      val parent = info.parent.getOrElse("")
    3.26      val parent_base_name = info.parent_base_name.getOrElse("")
    3.27  
    3.28 -    val output =
    3.29 -      output_path match { case Some(p) => Isabelle_System.standard_path(p) case None => "" }
    3.30 -
    3.31      val cwd = info.dir.file
    3.32 -    val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output)
    3.33 +    val env =
    3.34 +      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output))
    3.35      val script =
    3.36 -      if (is_pure(name)) "./build " + name + " \"$OUTPUT\""
    3.37 +      if (is_pure(name)) {
    3.38 +        if (do_output) "./build " + name + " \"$OUTPUT\""
    3.39 +        else """ rm -f "$OUTPUT"; ./build """ + name
    3.40 +      }
    3.41        else {
    3.42          """
    3.43          . "$ISABELLE_HOME/lib/scripts/timestart.bash"
    3.44          """ +
    3.45 -          (if (output_path.isDefined)
    3.46 -            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """
    3.47 +          (if (do_output)
    3.48 +            """
    3.49 +            "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
    3.50 +            """
    3.51            else
    3.52 -            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
    3.53 +            """
    3.54 +            rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
    3.55 +            """) +
    3.56          """
    3.57          RC="$?"
    3.58  
    3.59 @@ -384,10 +390,10 @@
    3.60        import XML.Encode._
    3.61            pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
    3.62              pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))(
    3.63 -          (output_path.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name,
    3.64 +          (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
    3.65              (name, (info.base_name, info.theories)))))))))
    3.66      }
    3.67 -    new Job(cwd, env, script, YXML.string_of_body(args_xml), output_path)
    3.68 +    new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output)
    3.69    }
    3.70  
    3.71  
    3.72 @@ -431,7 +437,7 @@
    3.73  
    3.74    def build(
    3.75      all_sessions: Boolean = false,
    3.76 -    build_images: Boolean = false,
    3.77 +    build_heap: Boolean = false,
    3.78      more_dirs: List[Path] = Nil,
    3.79      session_groups: List[String] = Nil,
    3.80      max_jobs: Int = 1,
    3.81 @@ -496,17 +502,15 @@
    3.82        { // check/start next job
    3.83          pending.dequeue(running.isDefinedAt(_)) match {
    3.84            case Some((name, info)) =>
    3.85 -            val output =
    3.86 -              if (build_images || queue.is_inner(name))
    3.87 -                Some(output_dir + Path.basic(name))
    3.88 -              else None
    3.89 +            val output = output_dir + Path.basic(name)
    3.90 +            val do_output = build_heap || queue.is_inner(name)
    3.91  
    3.92              val current =
    3.93              {
    3.94                input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
    3.95                  case Some(dir) =>
    3.96                    check_stamps(dir, name) match {
    3.97 -                    case Some((s, h)) => s == make_stamp(name) && (h || output.isEmpty)
    3.98 +                    case Some((s, h)) => s == make_stamp(name) && (h || !do_output)
    3.99                      case None => false
   3.100                    }
   3.101                  case None => false
   3.102 @@ -515,8 +519,9 @@
   3.103              if (current || no_build)
   3.104                loop(pending - name, running, results + (name -> (if (current) 0 else 1)))
   3.105              else if (info.parent.map(results(_)).forall(_ == 0)) {
   3.106 -              echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
   3.107 -              val job = start_job(name, info, output, info.options, timing, verbose, browser_info)
   3.108 +              echo((if (do_output) "Building " else "Running ") + name + " ...")
   3.109 +              val job =
   3.110 +                start_job(name, info, output, do_output, info.options, timing, verbose, browser_info)
   3.111                loop(pending, running + (name -> job), results)
   3.112              }
   3.113              else {
   3.114 @@ -547,14 +552,14 @@
   3.115        args.toList match {
   3.116          case
   3.117            Properties.Value.Boolean(all_sessions) ::
   3.118 -          Properties.Value.Boolean(build_images) ::
   3.119 +          Properties.Value.Boolean(build_heap) ::
   3.120            Properties.Value.Int(max_jobs) ::
   3.121            Properties.Value.Boolean(no_build) ::
   3.122            Properties.Value.Boolean(system_mode) ::
   3.123            Properties.Value.Boolean(timing) ::
   3.124            Properties.Value.Boolean(verbose) ::
   3.125            Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
   3.126 -            build(all_sessions, build_images, more_dirs.map(Path.explode), session_groups,
   3.127 +            build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
   3.128                max_jobs, no_build, build_options, system_mode, timing, verbose, sessions)
   3.129          case _ => error("Bad arguments:\n" + cat_lines(args))
   3.130        }

     4.1 --- a/src/Pure/build	Thu Jul 26 12:32:25 2012 +0200
     4.2 +++ b/src/Pure/build	Thu Jul 26 12:59:09 2012 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  function usage()
     4.5  {
     4.6    echo
     4.7 -  echo "Usage: $PRG TARGET OUTPUT"
     4.8 +  echo "Usage: $PRG TARGET [OUTPUT]"
     4.9    echo
    4.10    exit 1
    4.11  }
    4.12 @@ -30,7 +30,10 @@
    4.13  
    4.14  # args
    4.15  
    4.16 -if [ "$#" -eq 2 ]; then
    4.17 +if [ "$#" -eq 1 ]; then
    4.18 +  TARGET="$1"; shift
    4.19 +  OUTPUT=""; shift
    4.20 +elif [ "$#" -eq 2 ]; then
    4.21    TARGET="$1"; shift
    4.22    OUTPUT="$1"; shift
    4.23  else