1.1 --- a/lib/Tools/build	Mon Jul 23 15:44:42 2012 +0200
     1.2 +++ b/lib/Tools/build	Mon Jul 23 15:59:14 2012 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    echo "    -j INT       maximum number of jobs (default 1)"
     1.5    echo "    -l           list sessions only"
     1.6    echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
     1.7 +  echo "    -s           system build mode: produce output in ISABELLE_HOME"
     1.8    echo "    -v           verbose"
     1.9    echo
    1.10    echo "  Build and manage Isabelle sessions, depending on implicit"
    1.11 @@ -52,12 +53,13 @@
    1.12  BUILD_IMAGES=false
    1.13  MAX_JOBS=1
    1.14  LIST_ONLY=false
    1.15 +SYSTEM_MODE=false
    1.16  VERBOSE=false
    1.17  
    1.18  declare -a MORE_DIRS=()
    1.19  eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    1.20  
    1.21 -while getopts "abd:j:lo:v" OPT
    1.22 +while getopts "abd:j:lo:sv" OPT
    1.23  do
    1.24    case "$OPT" in
    1.25      a)
    1.26 @@ -79,6 +81,9 @@
    1.27      o)
    1.28        BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
    1.29        ;;
    1.30 +    s)
    1.31 +      SYSTEM_MODE="true"
    1.32 +      ;;
    1.33      v)
    1.34        VERBOSE="true"
    1.35        ;;
    1.36 @@ -96,5 +101,5 @@
    1.37  [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
    1.38  
    1.39  exec "$ISABELLE_TOOL" java isabelle.Build \
    1.40 -  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$VERBOSE" \
    1.41 +  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$VERBOSE" \
    1.42    "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"

     2.1 --- a/src/Pure/System/build.scala	Mon Jul 23 15:44:42 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Mon Jul 23 15:59:14 2012 +0200
     2.3 @@ -340,20 +340,20 @@
     2.4      def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
     2.5    }
     2.6  
     2.7 -  private def start_job(save: Boolean, name: String, info: Session.Info): Job =
     2.8 +  private def start_job(name: String, info: Session.Info, output: Option[String]): Job =
     2.9    {
    2.10      val parent = info.parent.getOrElse("")
    2.11  
    2.12      val cwd = info.dir.file
    2.13 -    val env = Map("INPUT" -> parent, "TARGET" -> name)
    2.14 +    val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse(""))
    2.15      val script =
    2.16 -      if (is_pure(name)) "./build " + (if (save) "-b " else "") + name
    2.17 +      if (is_pure(name)) "./build " + name + " \"$OUTPUT\""
    2.18        else {
    2.19          """
    2.20          . "$ISABELLE_HOME/lib/scripts/timestart.bash"
    2.21          """ +
    2.22 -          (if (save)
    2.23 -            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
    2.24 +          (if (output.isDefined)
    2.25 +            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """
    2.26            else
    2.27              """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
    2.28          """
    2.29 @@ -372,7 +372,7 @@
    2.30      {
    2.31        import XML.Encode._
    2.32        pair(bool, pair(string, pair(string, list(string))))(
    2.33 -        save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
    2.34 +        output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
    2.35      }
    2.36      new Job(cwd, env, script, YXML.string_of_body(args_xml))
    2.37    }
    2.38 @@ -384,29 +384,31 @@
    2.39    private def sleep(): Unit = Thread.sleep(500)
    2.40  
    2.41    def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
    2.42 -    list_only: Boolean, verbose: Boolean,
    2.43 +    list_only: Boolean, system_mode: Boolean, verbose: Boolean,
    2.44      more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
    2.45    {
    2.46      val options = (Options.init() /: more_options)(_.define_simple(_))
    2.47      val queue = find_sessions(options, all_sessions, sessions, more_dirs)
    2.48      val deps = dependencies(queue)
    2.49  
    2.50 +    val (output_dir, browser_info) =
    2.51 +      if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info"))
    2.52 +      else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO"))
    2.53  
    2.54      // prepare browser info dir
    2.55 -    if (options.bool("browser_info") &&
    2.56 -      !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
    2.57 +    if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
    2.58      {
    2.59 -      Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
    2.60 -      File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
    2.61 -        Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
    2.62 -      File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
    2.63 -        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
    2.64 -        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
    2.65 -        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
    2.66 +      browser_info.file.mkdirs()
    2.67 +      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
    2.68 +        browser_info + Path.explode("isabelle.gif"))
    2.69 +      File.write(browser_info + Path.explode("index.html"),
    2.70 +        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
    2.71 +        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
    2.72 +        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
    2.73      }
    2.74  
    2.75      // prepare log dir
    2.76 -    val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
    2.77 +    val log_dir = output_dir + Path.explode("log")
    2.78      log_dir.file.mkdirs()
    2.79  
    2.80      // scheduler loop
    2.81 @@ -447,9 +449,12 @@
    2.82                loop(pending - name, running, results + (name -> 0))
    2.83              }
    2.84              else if (info.parent.map(results(_)).forall(_ == 0)) {
    2.85 -              val save = build_images || queue.is_inner(name)
    2.86 -              echo((if (save) "Building " else "Running ") + name + " ...")
    2.87 -              val job = start_job(save, name, info)
    2.88 +              val output =
    2.89 +                if (build_images || queue.is_inner(name))
    2.90 +                  Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
    2.91 +                else None
    2.92 +              echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
    2.93 +              val job = start_job(name, info, output)
    2.94                loop(pending, running + (name -> job), results)
    2.95              }
    2.96              else {
    2.97 @@ -477,10 +482,11 @@
    2.98            Properties.Value.Boolean(build_images) ::
    2.99            Properties.Value.Int(max_jobs) ::
   2.100            Properties.Value.Boolean(list_only) ::
   2.101 +          Properties.Value.Boolean(system_mode) ::
   2.102            Properties.Value.Boolean(verbose) ::
   2.103            Command_Line.Chunks(more_dirs, options, sessions) =>
   2.104 -            build(all_sessions, build_images, max_jobs, list_only, verbose,
   2.105 -              more_dirs.map(Path.explode), options, sessions)
   2.106 +            build(all_sessions, build_images, max_jobs, list_only, system_mode,
   2.107 +              verbose, more_dirs.map(Path.explode), options, sessions)
   2.108          case _ => error("Bad arguments:\n" + cat_lines(args))
   2.109        }
   2.110      }

     3.1 --- a/src/Pure/build	Mon Jul 23 15:44:42 2012 +0200
     3.2 +++ b/src/Pure/build	Mon Jul 23 15:59:14 2012 +0200
     3.3 @@ -12,12 +12,7 @@
     3.4  function usage()
     3.5  {
     3.6    echo
     3.7 -  echo "Usage: $PRG [OPTIONS] TARGET"
     3.8 -  echo
     3.9 -  echo "  Options are:"
    3.10 -  echo "    -b           build target images"
    3.11 -  echo
    3.12 -  echo "  Build Isabelle/ML TARGET: RAW or Pure"
    3.13 +  echo "Usage: $PRG TARGET OUTPUT"
    3.14    echo
    3.15    exit 1
    3.16  }
    3.17 @@ -33,32 +28,14 @@
    3.18  
    3.19  ## process command line
    3.20  
    3.21 -# options
    3.22 -
    3.23 -BUILD_IMAGES=false
    3.24 -
    3.25 -while getopts "b" OPT
    3.26 -do
    3.27 -  case "$OPT" in
    3.28 -    b)
    3.29 -      BUILD_IMAGES="true"
    3.30 -      ;;
    3.31 -    \?)
    3.32 -      usage
    3.33 -      ;;
    3.34 -  esac
    3.35 -done
    3.36 -
    3.37 -shift $(($OPTIND - 1))
    3.38 -
    3.39 -
    3.40  # args
    3.41  
    3.42 -TARGET="Pure"
    3.43 -[ "$#" -ge 1 ] && { TARGET="$1"; shift; }
    3.44 -[ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\""
    3.45 -
    3.46 -[ "$#" -eq 0 ] || usage
    3.47 +if [ "$#" -eq 2 ]; then
    3.48 +  TARGET="$1"; shift
    3.49 +  OUTPUT="$1"; shift
    3.50 +else
    3.51 +  usage
    3.52 +fi
    3.53  
    3.54  
    3.55  ## main
    3.56 @@ -79,7 +56,7 @@
    3.57  . "$ISABELLE_HOME/lib/scripts/timestart.bash"
    3.58  
    3.59  if [ "$TARGET" = RAW ]; then
    3.60 -  if [ "$BUILD_IMAGES" = false ]; then
    3.61 +  if [ -z "$OUTPUT" ]; then
    3.62      "$ISABELLE_PROCESS" \
    3.63        -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
    3.64        -q RAW_ML_SYSTEM
    3.65 @@ -88,10 +65,10 @@
    3.66        -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
    3.67        -e "structure Isar = struct fun main () = () end;" \
    3.68        -e "ml_prompts \"ML> \" \"ML# \";" \
    3.69 -      -q -w RAW_ML_SYSTEM RAW
    3.70 +      -q -w RAW_ML_SYSTEM "$OUTPUT"
    3.71    fi
    3.72  else
    3.73 -  if [ "$BUILD_IMAGES" = false ]; then
    3.74 +  if [ -z "$OUTPUT" ]; then
    3.75      "$ISABELLE_PROCESS" \
    3.76        -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
    3.77        -q RAW_ML_SYSTEM
    3.78 @@ -99,7 +76,7 @@
    3.79      "$ISABELLE_PROCESS" \
    3.80        -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
    3.81        -e "ml_prompts \"ML> \" \"ML# \";" \
    3.82 -      -f -q -w RAW_ML_SYSTEM Pure
    3.83 +      -f -q -w RAW_ML_SYSTEM "$OUTPUT"
    3.84    fi
    3.85  fi
    3.86