further imitation of "usedir" shell script;
Pure/build observes build_images option, unlike traditional version;
tuned signature;

--- a/src/Pure/General/path.scala	Fri Jul 20 18:50:33 2012 +0200
+++ b/src/Pure/General/path.scala	Fri Jul 20 21:04:03 2012 +0200
@@ -8,6 +8,8 @@
 package isabelle
 
 
+import java.io.File
+
 import scala.util.matching.Regex
 
 
@@ -162,4 +164,9 @@
 
     new Path(Path.norm_elems(elems.map(eval).flatten))
   }
+
+
+  /* platform file */
+
+  def file: File = Isabelle_System.platform_file(this)
 }

--- a/src/Pure/System/build.scala	Fri Jul 20 18:50:33 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Jul 20 21:04:03 2012 +0200
@@ -198,7 +198,7 @@
 
   private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
   {
-    val root = Isabelle_System.platform_file(dir + ROOT)
+    val root = (dir + ROOT).file
     if (root.isFile) sessions_root(dir, root, queue)
     else if (strict) error("Bad session root file: " + quote(root.toString))
     else queue
@@ -212,7 +212,7 @@
     (queue /: dirs)((queue1, dir1) =>
       try {
         val dir2 = dir + Path.explode(dir1)
-        if (Isabelle_System.platform_file(dir2).isDirectory) sessions_dir(true, dir2, queue1)
+        if (dir2.file.isDirectory) sessions_dir(true, dir2, queue1)
         else error("Bad session directory: " + dir2.toString)
       }
       catch {
@@ -228,7 +228,7 @@
     for (dir <- Isabelle_System.components()) {
       queue = sessions_dir(false, dir, queue)
 
-      val catalog = Isabelle_System.platform_file(dir + SESSIONS)
+      val catalog = (dir + SESSIONS).file
       if (catalog.isFile)
         queue = sessions_catalog(dir, catalog, queue)
     }
@@ -242,12 +242,15 @@
 
   /** build **/
 
+  private def echo(msg: String) { java.lang.System.out.println(msg) }
+  private def echo_n(msg: String) { java.lang.System.out.print(msg) }
+
   private def build_job(build_images: Boolean,  // FIXME
     key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
   {
-    val cwd = Isabelle_System.platform_file(info.dir)
+    val cwd = info.dir.file
     val script =
-      if (is_pure(key.name)) "./build " + key.name
+      if (is_pure(key.name)) "./build " + (if (build_images) "-b " else "") + key.name
       else """echo "Bad session" >&2; exit 2"""
     new Isabelle_System.Bash_Job(cwd, null, script)
   }
@@ -256,7 +259,6 @@
     more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   {
     val full_queue = find_sessions(more_dirs)
-
     val build_options = (Options.init() /: options)(_.define_simple(_))
 
     sessions.filter(name => !full_queue.defined(name)) match {
@@ -268,15 +270,54 @@
       if (all_sessions) full_queue
       else full_queue.required(sessions)
 
-    for ((key, info) <- required_queue.topological_order) {
-      if (list_only) println(key.name + " in " + info.dir)
-      else {
-        val (out, err, rc) = build_job(build_images, key, info).join
-        java.lang.System.err.print(err)
-      }
+    // prepare browser info dir
+    if (build_options.bool("browser_info") &&
+      !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
+    {
+      Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
+      Standard_System.copy_file(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif").file,
+        Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif").file)
+      Standard_System.write_file(Path.explode("$ISABELLE_BROWSER_INFO/index.html").file,
+        Standard_System.read_file(
+          Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template").file) +
+        Standard_System.read_file(
+          Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template").file) +
+        Standard_System.read_file(
+          Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template").file))
     }
 
-    0
+    // prepare log dir
+    val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
+    log_dir.file.mkdirs()
+
+    // run jobs
+    val rcs =
+      for ((key, info) <- required_queue.topological_order) yield
+      {
+        if (list_only) { echo(key.name + " in " + info.dir); 0 }
+        else {
+          if (build_images) echo("Building " + key.name + "...")
+          else echo("Running " + key.name + "...")
+
+          val (out, err, rc) = build_job(build_images, key, info).join
+          echo_n(err)
+
+          val log = log_dir + Path.basic(key.name)
+          if (rc == 0) {
+            Standard_System.write_file(log.ext("gz").file, out, true)
+          }
+          else {
+            Standard_System.write_file(log.file, out)
+            echo(key.name + " FAILED")
+            echo("(see also " + log.file + ")")
+            val lines = split_lines(out)
+            val tail = lines.drop(lines.length - 20 max 0)
+            echo("\n" + cat_lines(tail))
+          }
+          rc
+        }
+      }
+    (0 /: rcs)(_ max _)
   }
 
 

--- a/src/Pure/System/isabelle_system.scala	Fri Jul 20 18:50:33 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri Jul 20 21:04:03 2012 +0200
@@ -146,10 +146,9 @@
     if (path.is_absolute || path.is_current)
       try_file(platform_file(path))
     else {
-      val pure_file = platform_file(Path.explode("~~/src/Pure") + path)
+      val pure_file = (Path.explode("~~/src/Pure") + path).file
       if (pure_file.isFile) Some(pure_file)
-      else if (getenv("ML_SOURCES") != "")
-        try_file(platform_file(Path.explode("$ML_SOURCES") + path))
+      else if (getenv("ML_SOURCES") != "") try_file((Path.explode("$ML_SOURCES") + path).file)
       else None
     }
   }
@@ -278,7 +277,7 @@
   def isabelle_tool(name: String, args: String*): (String, Int) =
   {
     Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
-      val file = platform_file(dir + Path.basic(name))
+      val file = (dir + Path.basic(name)).file
       try {
         file.isFile && file.canRead && file.canExecute &&
           !name.endsWith("~") && !name.endsWith(".orig")
@@ -309,7 +308,7 @@
     val ml_ident = getenv_strict("ML_IDENTIFIER")
     val logics = new mutable.ListBuffer[String]
     for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
-      val files = platform_file(dir + Path.explode(ml_ident)).listFiles()
+      val files = (dir + Path.explode(ml_ident)).file.listFiles()
       if (files != null) {
         for (file <- files if file.isFile) logics += file.getName
       }
@@ -327,6 +326,6 @@
   {
     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
     for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
-      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
+      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
   }
 }

--- a/src/Pure/System/options.scala	Fri Jul 20 18:50:33 2012 +0200
+++ b/src/Pure/System/options.scala	Fri Jul 20 21:04:03 2012 +0200
@@ -66,7 +66,7 @@
     var options = empty
     for {
       dir <- Isabelle_System.components()
-      file = Isabelle_System.platform_file(dir + OPTIONS)
+      file = (dir + OPTIONS).file
       if file.isFile
       entry <- Parser.parse_entries(file)
     } {

--- a/src/Pure/System/standard_system.scala	Fri Jul 20 18:50:33 2012 +0200
+++ b/src/Pure/System/standard_system.scala	Fri Jul 20 21:04:03 2012 +0200
@@ -15,6 +15,7 @@
   BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
   File, FileFilter, IOException}
 import java.nio.charset.Charset
+import java.util.zip.GZIPOutputStream
 
 import scala.io.Codec
 import scala.util.matching.Regex
@@ -115,10 +116,11 @@
 
   def read_file(file: File): String = slurp(new FileInputStream(file))
 
-  def write_file(file: File, text: CharSequence)
+  def write_file(file: File, text: CharSequence, zip: Boolean = false)
   {
-    val writer =
-      new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
+    val stream1 = new FileOutputStream(file)
+    val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
+    val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset))
     try { writer.append(text) }
     finally { writer.close }
   }

--- a/src/Pure/System/system_channel.scala	Fri Jul 20 18:50:33 2012 +0200
+++ b/src/Pure/System/system_channel.scala	Fri Jul 20 21:04:03 2012 +0200
@@ -47,8 +47,7 @@
   }
 
   private def rm_fifo(fifo: String): Boolean =
-    Isabelle_System.platform_file(
-      Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo)).delete
+    Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo).file.delete
 
   private def fifo_input_stream(fifo: String): InputStream =
   {

--- a/src/Pure/build	Fri Jul 20 18:50:33 2012 +0200
+++ b/src/Pure/build	Fri Jul 20 21:04:03 2012 +0200
@@ -12,7 +12,10 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG TARGET"
+  echo "Usage: $PRG [OPTIONS] TARGET"
+  echo
+  echo "  Options are:"
+  echo "    -b           build target images"
   echo
   echo "  Build Isabelle/ML TARGET: RAW or Pure"
   echo
@@ -30,6 +33,27 @@
 
 ## 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\""
@@ -54,29 +78,37 @@
 
 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
-echo "Building $TARGET ..." >&2
+if [ "$TARGET" = RAW ]; then
+  if [ "$BUILD_IMAGES" = false ]; then
+    "$ISABELLE_PROCESS" \
+      -e "use\"$COMPAT\" handle _ => exit 1;" \
+      -q RAW_ML_SYSTEM
+  else
+    "$ISABELLE_PROCESS" \
+      -e "use\"$COMPAT\" handle _ => exit 1;" \
+      -e "structure Isar = struct fun main () = () end;" \
+      -e "ml_prompts \"ML> \" \"ML# \";" \
+      -q -w RAW_ML_SYSTEM RAW
+  fi
+else
+  if [ "$BUILD_IMAGES" = false ]; then
+    "$ISABELLE_PROCESS" \
+      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
+      -q RAW_ML_SYSTEM
+  else
+    "$ISABELLE_PROCESS" \
+      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
+      -e "ml_prompts \"ML> \" \"ML# \";" \
+      -f -q -w RAW_ML_SYSTEM Pure
+  fi
+fi
 
-if [ "$TARGET" = RAW ]; then
-  "$ISABELLE_PROCESS" \
-    -e "use\"$COMPAT\" handle _ => exit 1;" \
-    -e "structure Isar = struct fun main () = () end;" \
-    -e "ml_prompts \"ML> \" \"ML# \";" \
-    -q -w RAW_ML_SYSTEM RAW
-  RC="$?"
-else
-  "$ISABELLE_PROCESS" \
-    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
-    -e "ml_prompts \"ML> \" \"ML# \";" \
-    -f -q -w RAW_ML_SYSTEM Pure
-  RC="$?"
-fi
+RC="$?"
 
 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
 
 if [ "$RC" -eq 0 ]; then
   echo "Finished $TARGET ($TIMES_REPORT)" >&2
-else
-  echo "$TARGET FAILED" >&2
 fi
 
 exit "$RC"