# HG changeset patch
# User wenzelm
# Date 1343054669 -7200
# Node ID 8eaaaf376dc9cfe0813bc38c566693c7ef88d224
# Parent  3c9890c19e901dfbbf418f463366066fc886f1b7# Parent  2d987dad7c3ec573806a4cea7394f1692d3b6aec
merged

diff -r 3c9890c19e90 -r 8eaaaf376dc9 Admin/init_components
--- a/Admin/init_components	Mon Jul 23 15:32:30 2012 +0200
+++ b/Admin/init_components	Mon Jul 23 16:44:29 2012 +0200
@@ -5,22 +5,11 @@
 # init_components - bash source script to initialize components
 # as specified in the Admin directory
 
-function init_component_liberal
-{
-  local LOCATION="$1"
-  if [[ -d "${LOCATION}" ]]
-  then
-    init_component "${LOCATION}"
-  else
-    echo "Warning: no component found in ${LOCATION}" >&2
-  fi
-}
-
-while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
+while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
 do
-  case "${REPLY}" in
+  case "$REPLY" in
     \#* | "") ;;
-    /*) init_component_liberal "${REPLY}" ;;
-    *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
+    /*) init_component "$REPLY" ;;
+    *) init_component "$COMPONENT/$REPLY" ;;
   esac
-done < "${ISABELLE_HOME}/Admin/components"
+done < "$ISABELLE_HOME/Admin/components"
diff -r 3c9890c19e90 -r 8eaaaf376dc9 Admin/isatest/annomaly
--- a/Admin/isatest/annomaly	Mon Jul 23 15:32:30 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-#!/bin/sh
-
-# Create AnnoMaLy documentation for Isabelle
-# See http://martin.von-gagern.net/projects/annomaly/
-#   2007  Martin von Gagern (martin@von-gagern.net)
-
-# Abort on any error
-set -e -o pipefail
-
-BUILD_DIR="$HOME/isabelle.annomaly"
-ISABELLE_HOME="$BUILD_DIR/Isabelle"
-ISABELLE_CVS="$HOME/isabelle.cvs"
-ADMIN_CVS="$ISABELLE_CVS/Admin"
-# ISABELLE_HOME="$ISABELLE_CVS/Distribution"
-ISABELLE_SRC="$ISABELLE_HOME/src"
-HTML_DIR="$HOME/html-data/isabelle-doc"
-export CVS_RSH=ssh
-export SMLNJ_HOME="$HOME/annomaly"
-export PATH="$SMLNJ_HOME/bin:$PATH"
-export SML_DOC_DIR="$HTML_DIR.tmp"
-# export SML_DOC_DEBUG="all"
-TARGET=HOL
-CVSUP=true
-
-# Parse command line
-for ARG in "$@"; do case "$ARG" in
-	-p) TARGET=Pure ;;
-	-n) CVSUP=false ;;
-	-l) export SML_LOG_DIR="$HOME/logs" ;;
-esac; done
-
-# Update CVS
-cd "$ADMIN_CVS"
-if $CVSUP; then
-  echo "Updating CVS"
-  cvs -q up -d
-fi
-
-# Find nightly isabelle tarball
-ISABELLE_TAR=""
-for i in /home/html/isatest/Isabelle_[0-9]*-20[0-9][0-9].tar.gz; do
-  if [[ -r "$i" ]]; then ISABELLE_TAR="$i"; fi
-done
-if [[ -z $ISABELLE_TAR ]]; then
-  echo "No isabelle tarball found!" >&2
-  exit 1
-fi
-
-# Create build environemnt
-mkdir -p "$BUILD_DIR"
-cd "$BUILD_DIR"
-if [[ -d Isabelle ]]; then
-  rm -rf *
-fi
-tar xzf "$ISABELLE_TAR"
-cd "$ISABELLE_HOME"
-cp "$ADMIN_CVS"/isatest/annomaly.ML src/Pure/ML-Systems/annomaly.ML
-ln -s run-smlnj lib/scripts/run-annomaly
-
-# Create clean output directory
-rm -rf "$SML_DOC_DIR"
-mkdir "$SML_DOC_DIR"
-cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
-cat > "$SML_DOC_DIR/.htaccess" <<EOF
-DirectoryIndex index.html source.html
-<IfModule mod_deflate>
-SetOutputFilter DEFLATE 
-</IfModule>
-AddType text/plain .dot
-EOF
-
-# Build isabelle
-ISABELLE_HOME="$(cd "$ISABELLE_HOME"; pwd -P)"
-cd "$ISABELLE_HOME"
-export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
-rm -rf heaps
-./build -b $TARGET
-cd "$BUILD_DIR"
-rm -rf *
-
-# Postprocess created files
-cd $SML_DOC_DIR
-dot -Tsvg depGraph.dot \
-  | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
-  > depGraph.svg
-dot -Tps2 depGraph.dot > depGraph.ps
-ps2pdf depGraph.ps depGraph.pdf
-grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
-
-# Install result by renaming, to be almost atomic
-rm -rf "$HTML_DIR.bac"
-if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
-mv "$SML_DOC_DIR" "$HTML_DIR"
-rm -rf "$HTML_DIR.bac"
-
-# Done
-echo "Completed successfully"
-exit 0
diff -r 3c9890c19e90 -r 8eaaaf376dc9 Admin/isatest/annomaly.ML
--- a/Admin/isatest/annomaly.ML	Mon Jul 23 15:32:30 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*  Title:      Admin/isatest/annomaly.ML
-    Author:     Martin von Gagern <martin@von-gagern.net>
-*)
-
-use "ML-Systems/smlnj.ML";
-
-local
-
-  val smlnj_use_text = use_text
-
-  val smlnj_use_file = use_file
-
-  val smlnj_forget_structure = forget_structure
-
-  fun mkAbsolute path =
-      OS.Path.mkAbsolute { path = path, relativeTo = OS.FileSys.getDir () }
-
-  fun toArcs path = #arcs (OS.Path.fromString path)
-
-  val isabelleHome =
-      case OS.Process.getEnv "ISABELLE_HOME"
-       of  NONE => OS.FileSys.getDir ()
-         | SOME home => mkAbsolute home
-
-  fun noparent [] = []
-    | noparent (n :: ns) =
-      if n = OS.Path.parentArc then noparent ns else n :: noparent ns
-
-  fun isabellePath [] = []
-    | isabellePath ("src" :: name) = "Isabelle" :: name
-    | isabellePath (name as (n :: ns)) =
-      if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name
-
-  fun rewrite defPrefix name =
-      let val abs = mkAbsolute name
-          val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
-          val exists = (OS.FileSys.access(abs, nil)
-                        handle OS.SysErr _ => false)
-      in  if exists andalso rel <> ""
-          then isabellePath (toArcs rel)
-          else defPrefix @ noparent (toArcs name)
-      end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
-
-in
-
-  fun use_text tune str_of_pos name_space (line, name) p v t =
-    let val name = case name of "" => "unnamed" | name => name
-        val arcs = rewrite ["use_text"] name
-        (* should we have different files for different line numbers? *
-        val arcs = if line <= 1 then arcs
-                   else arcs @ [ "l." ^ Int.toString line ]
-        *)
-        val arcs = if t = "structure Isabelle =\nstruct\nend;"
-                      andalso name = "ML"
-                   then ["empty_Isabelle", "empty" ] else arcs
-        val _    = AnnoMaLy.nameNextStream arcs
-    in  smlnj_use_text tune str_of_pos name_space (line, name) p v t  end;
-
-  fun use_file tune str_of_pos name_space output verbose name =
-      let val arcs = rewrite ["use_file"] name
-          val _    = AnnoMaLy.nameNextStream arcs
-      in  smlnj_use_file tune str_of_pos name_space output verbose name  end;
-
-  fun forget_structure name =
-      let val arcs = [ "forget_structure", name ]
-          val _    = AnnoMaLy.nameNextStream arcs
-      in  smlnj_forget_structure name  end;
-
-end;
diff -r 3c9890c19e90 -r 8eaaaf376dc9 Admin/isatest/isatest-annomaly
--- a/Admin/isatest/isatest-annomaly	Mon Jul 23 15:32:30 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-#!/usr/bin/env bash
-#
-# Create AnnoMaLy documentation for Isabelle
-#
-# Based on http://martin.von-gagern.net/projects/annomaly/
-#   2007  Martin von Gagern (martin@von-gagern.net)
-
-## global settings
-. ~/admin/isatest/isatest-settings
-
-PRG="$(basename "$0")"
-
-export SMLNJ_HOME="/home/gagern/annomaly"
-export SML_DOC_DIR="$HOME/anno-html"
-
-ADMIN="$HOME/admin/isatest"
-LOGICS="HOL"
-
-# Abort on any error
-set -e -o pipefail
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG"
-  echo
-  echo "  Generate html documentation from .ML files"
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  log "FAILED, $1"
-  exit 2
-}
-
-
-## main
-
-ISABELLE_HOME="$DISTPREFIX/Isabelle"
-ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
-
-[ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
-
-
-# Create clean output directory
-rm -rf "$SML_DOC_DIR"
-mkdir "$SML_DOC_DIR"
-cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
-cat > "$SML_DOC_DIR/.htaccess" <<EOF
-DirectoryIndex index.html source.html
-<IfModule mod_deflate>
-SetOutputFilter DEFLATE 
-</IfModule>
-AddType text/plain .dot
-EOF
-
-# Prepare build environemnt
-cd "$ISABELLE_HOME"
-cp "$ADMIN/annomaly.ML" src/Pure/ML-Systems/annomaly.ML
-ln -fs run-smlnj lib/scripts/run-annomaly
-
-cd "$ISABELLE_HOME"
-export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
-
-
-# Process image(s)
-for L in $LOGICS
-do
-  ( cd "$ISABELLE_HOME/src/$L"; \
-    cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
-    "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
-done
-
-
-# Postprocess created files
-cd "$SML_DOC_DIR"
-dot -Tsvg depGraph.dot \
-  | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
-  > depGraph.svg
-dot -Tps2 depGraph.dot > depGraph.ps
-ps2pdf depGraph.ps depGraph.pdf
-
-# $ISABELLE_HOME does not seem to occur anywhere ??
-# grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
-
-
-log "annomaly docs generated successfully."
diff -r 3c9890c19e90 -r 8eaaaf376dc9 Admin/isatest/settings/annomaly
--- a/Admin/isatest/settings/annomaly	Mon Jul 23 15:32:30 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-ML_SYSTEM=annomaly
-ML_HOME="$SMLNJ_HOME/bin"
-ML_OPTIONS="-m $SMLNJ_HOME/annomaly/annomaly.cm @SMLdebug=/dev/null"
-ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-
-
-ISABELLE_HOME_USER="$HOME/isabelle-annomaly"
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-
diff -r 3c9890c19e90 -r 8eaaaf376dc9 Admin/mira.py
--- a/Admin/mira.py	Mon Jul 23 15:32:30 2012 +0200
+++ b/Admin/mira.py	Mon Jul 23 16:44:29 2012 +0200
@@ -492,8 +492,8 @@
 
 smlnj_settings = '''
 ML_SYSTEM=smlnj
-ML_HOME="/home/smlnj/110.72/bin"
-ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
+ML_HOME="/home/smlnj/110.74/bin"
+ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
 '''
 
diff -r 3c9890c19e90 -r 8eaaaf376dc9 etc/settings
--- a/etc/settings	Mon Jul 23 15:32:30 2012 +0200
+++ b/etc/settings	Mon Jul 23 16:44:29 2012 +0200
@@ -45,7 +45,7 @@
 # Standard ML of New Jersey (slow!)
 #ML_SYSTEM=smlnj-110
 #ML_HOME="/usr/local/smlnj/bin"
-#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
+#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
 #SMLNJ_CYGWIN_RUNTIME=1
 
@@ -93,7 +93,11 @@
 ###
 
 # The place for user configuration, heap files, etc.
-ISABELLE_HOME_USER="$USER_HOME/.isabelle/${ISABELLE_IDENTIFIER:-.}"
+if [ -z "ISABELLE_IDENTIFIER" ]; then
+  ISABELLE_HOME_USER="$USER_HOME/.isabelle"
+else
+  ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
+fi
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
diff -r 3c9890c19e90 -r 8eaaaf376dc9 lib/Tools/build
--- a/lib/Tools/build	Mon Jul 23 15:32:30 2012 +0200
+++ b/lib/Tools/build	Mon Jul 23 16:44:29 2012 +0200
@@ -21,6 +21,7 @@
   echo "    -j INT       maximum number of jobs (default 1)"
   echo "    -l           list sessions only"
   echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
+  echo "    -s           system build mode: produce output in ISABELLE_HOME"
   echo "    -v           verbose"
   echo
   echo "  Build and manage Isabelle sessions, depending on implicit"
@@ -52,12 +53,13 @@
 BUILD_IMAGES=false
 MAX_JOBS=1
 LIST_ONLY=false
+SYSTEM_MODE=false
 VERBOSE=false
 
 declare -a MORE_DIRS=()
 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
 
-while getopts "abd:j:lo:v" OPT
+while getopts "abd:j:lo:sv" OPT
 do
   case "$OPT" in
     a)
@@ -79,6 +81,9 @@
     o)
       BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
       ;;
+    s)
+      SYSTEM_MODE="true"
+      ;;
     v)
       VERBOSE="true"
       ;;
@@ -96,5 +101,5 @@
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
 exec "$ISABELLE_TOOL" java isabelle.Build \
-  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$VERBOSE" \
+  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$VERBOSE" \
   "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
diff -r 3c9890c19e90 -r 8eaaaf376dc9 lib/Tools/usedir
--- a/lib/Tools/usedir	Mon Jul 23 15:32:30 2012 +0200
+++ b/lib/Tools/usedir	Mon Jul 23 16:44:29 2012 +0200
@@ -241,7 +241,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
+    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
     -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
@@ -250,7 +250,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
+    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
     -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
diff -r 3c9890c19e90 -r 8eaaaf376dc9 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Mon Jul 23 15:32:30 2012 +0200
+++ b/lib/scripts/getsettings	Mon Jul 23 16:44:29 2012 +0200
@@ -163,8 +163,7 @@
   esac
 
   if [ ! -d "$COMPONENT" ]; then
-    echo >&2 "Missing Isabelle component directory: \"$COMPONENT\""
-    exit 2
+    echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   elif [ -z "$ISABELLE_COMPONENTS" ]; then
     ISABELLE_COMPONENTS="$COMPONENT"
   else
diff -r 3c9890c19e90 -r 8eaaaf376dc9 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/Pure/General/file.ML	Mon Jul 23 16:44:29 2012 +0200
@@ -45,11 +45,7 @@
 
 val platform_path = Path.implode o Path.expand;
 
-fun shell_quote s =
-  if exists_string (fn c => c = "'") s then
-    error ("Illegal single quote in path specification: " ^ quote s)
-  else enclose "'" "'" s;
-
+val shell_quote = enclose "'" "'";
 val shell_path = shell_quote o platform_path;
 
 
diff -r 3c9890c19e90 -r 8eaaaf376dc9 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/Pure/System/build.scala	Mon Jul 23 16:44:29 2012 +0200
@@ -340,20 +340,20 @@
     def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
   }
 
-  private def start_job(save: Boolean, name: String, info: Session.Info): Job =
+  private def start_job(name: String, info: Session.Info, output: Option[String]): Job =
   {
     val parent = info.parent.getOrElse("")
 
     val cwd = info.dir.file
-    val env = Map("INPUT" -> parent, "TARGET" -> name)
+    val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse(""))
     val script =
-      if (is_pure(name)) "./build " + (if (save) "-b " else "") + name
+      if (is_pure(name)) "./build " + name + " \"$OUTPUT\""
       else {
         """
         . "$ISABELLE_HOME/lib/scripts/timestart.bash"
         """ +
-          (if (save)
-            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
+          (if (output.isDefined)
+            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """
           else
             """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
         """
@@ -372,7 +372,7 @@
     {
       import XML.Encode._
       pair(bool, pair(string, pair(string, list(string))))(
-        save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
+        output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
     }
     new Job(cwd, env, script, YXML.string_of_body(args_xml))
   }
@@ -384,29 +384,31 @@
   private def sleep(): Unit = Thread.sleep(500)
 
   def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
-    list_only: Boolean, verbose: Boolean,
+    list_only: Boolean, system_mode: Boolean, verbose: Boolean,
     more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
   {
     val options = (Options.init() /: more_options)(_.define_simple(_))
     val queue = find_sessions(options, all_sessions, sessions, more_dirs)
     val deps = dependencies(queue)
 
+    val (output_dir, browser_info) =
+      if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info"))
+      else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO"))
 
     // prepare browser info dir
-    if (options.bool("browser_info") &&
-      !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
+    if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
     {
-      Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
-      File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
-        Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
-      File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
-        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
-        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
-        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
+      browser_info.file.mkdirs()
+      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
+        browser_info + Path.explode("isabelle.gif"))
+      File.write(browser_info + Path.explode("index.html"),
+        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
+        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
     }
 
     // prepare log dir
-    val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
+    val log_dir = output_dir + Path.explode("log")
     log_dir.file.mkdirs()
 
     // scheduler loop
@@ -447,9 +449,12 @@
               loop(pending - name, running, results + (name -> 0))
             }
             else if (info.parent.map(results(_)).forall(_ == 0)) {
-              val save = build_images || queue.is_inner(name)
-              echo((if (save) "Building " else "Running ") + name + " ...")
-              val job = start_job(save, name, info)
+              val output =
+                if (build_images || queue.is_inner(name))
+                  Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
+                else None
+              echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
+              val job = start_job(name, info, output)
               loop(pending, running + (name -> job), results)
             }
             else {
@@ -477,10 +482,11 @@
           Properties.Value.Boolean(build_images) ::
           Properties.Value.Int(max_jobs) ::
           Properties.Value.Boolean(list_only) ::
+          Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(verbose) ::
           Command_Line.Chunks(more_dirs, options, sessions) =>
-            build(all_sessions, build_images, max_jobs, list_only, verbose,
-              more_dirs.map(Path.explode), options, sessions)
+            build(all_sessions, build_images, max_jobs, list_only, system_mode,
+              verbose, more_dirs.map(Path.explode), options, sessions)
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }
diff -r 3c9890c19e90 -r 8eaaaf376dc9 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/Pure/System/session.ML	Mon Jul 23 16:44:29 2012 +0200
@@ -10,7 +10,7 @@
   val name: unit -> string
   val welcome: unit -> string
   val init: bool -> string -> string -> unit
-  val use_dir: string -> string -> bool -> string list -> bool -> bool ->
+  val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     string -> bool -> string list -> string -> string -> bool * string ->
     string -> int -> bool -> bool -> int -> int -> int -> int -> unit
   val finish: unit -> unit
@@ -94,12 +94,12 @@
 fun dumping (_, "") = NONE
   | dumping (cp, path) = SOME (cp, Path.explode path);
 
-fun use_dir item root build modes reset info doc doc_graph doc_variants parent
+fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
      (init reset parent name;
-      Present.init build info doc doc_graph doc_variants (path ()) name
+      Present.init build info info_path doc doc_graph doc_variants (path ()) name
         (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
       if timing then
         let
diff -r 3c9890c19e90 -r 8eaaaf376dc9 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/Pure/Thy/present.ML	Mon Jul 23 16:44:29 2012 +0200
@@ -17,7 +17,7 @@
    path: string, parents: string list} list -> Path.T -> unit
   val display_graph: {name: string, ID: string, dir: string, unfold: bool,
    path: string, parents: string list} list -> unit
-  val init: bool -> bool -> string -> bool -> string list -> string list ->
+  val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
     string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
     theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
@@ -34,8 +34,6 @@
 
 (** paths **)
 
-val output_path = Path.variable "ISABELLE_BROWSER_INFO";
-
 val tex_ext = Path.ext "tex";
 val tex_path = tex_ext o Path.basic;
 val html_ext = Path.ext "html";
@@ -275,7 +273,7 @@
 
 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
 
-fun init build info doc doc_graph doc_variants path name dump_prefix
+fun init build info info_path doc doc_graph doc_variants path name dump_prefix
     (remote_path, first_time) verbose thys =
   if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
     (browser_info := empty_browser_info; session_info := NONE)
@@ -284,7 +282,7 @@
       val parent_name = name_of_session (take (length path - 1) path);
       val session_name = name_of_session path;
       val sess_prefix = Path.make path;
-      val html_prefix = Path.append (Path.expand output_path) sess_prefix;
+      val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
 
       val documents =
         if doc = "" then []
diff -r 3c9890c19e90 -r 8eaaaf376dc9 src/Pure/build
--- a/src/Pure/build	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/Pure/build	Mon Jul 23 16:44:29 2012 +0200
@@ -12,12 +12,7 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG [OPTIONS] TARGET"
-  echo
-  echo "  Options are:"
-  echo "    -b           build target images"
-  echo
-  echo "  Build Isabelle/ML TARGET: RAW or Pure"
+  echo "Usage: $PRG TARGET OUTPUT"
   echo
   exit 1
 }
@@ -33,32 +28,14 @@
 
 ## process command line
 
-# options
-
-BUILD_IMAGES=false
-
-while getopts "b" OPT
-do
-  case "$OPT" in
-    b)
-      BUILD_IMAGES="true"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
 # args
 
-TARGET="Pure"
-[ "$#" -ge 1 ] && { TARGET="$1"; shift; }
-[ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\""
-
-[ "$#" -eq 0 ] || usage
+if [ "$#" -eq 2 ]; then
+  TARGET="$1"; shift
+  OUTPUT="$1"; shift
+else
+  usage
+fi
 
 
 ## main
@@ -79,7 +56,7 @@
 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
 if [ "$TARGET" = RAW ]; then
-  if [ "$BUILD_IMAGES" = false ]; then
+  if [ -z "$OUTPUT" ]; then
     "$ISABELLE_PROCESS" \
       -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
       -q RAW_ML_SYSTEM
@@ -88,10 +65,10 @@
       -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
       -e "structure Isar = struct fun main () = () end;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
-      -q -w RAW_ML_SYSTEM RAW
+      -q -w RAW_ML_SYSTEM "$OUTPUT"
   fi
 else
-  if [ "$BUILD_IMAGES" = false ]; then
+  if [ -z "$OUTPUT" ]; then
     "$ISABELLE_PROCESS" \
       -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
       -q RAW_ML_SYSTEM
@@ -99,7 +76,7 @@
     "$ISABELLE_PROCESS" \
       -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
-      -f -q -w RAW_ML_SYSTEM Pure
+      -f -q -w RAW_ML_SYSTEM "$OUTPUT"
   fi
 fi