src/Pure/Tools/build.scala

--- a/src/Pure/Tools/build.scala	Mon Mar 11 14:25:14 2013 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 12 16:47:24 2013 +0100
@@ -497,9 +497,10 @@
         {
           import XML.Encode._
               pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
-                pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
+                pair(string, pair(string, pair(string,
+                  list(pair(Options.encode, list(Path.encode)))))))))))(
               (command_timings, (do_output, (info.options, (verbose, (browser_info,
-                (parent, (name, info.theories))))))))
+                (parent, (info.chapter, (name, info.theories)))))))))
         }))
 
     private val env =
@@ -595,7 +596,6 @@
   private def log_gz(name: String): Path = log(name).ext("gz")
 
   private val SESSION_NAME = "\fSession.name = "
-  private val SESSION_PARENT_PATH = "\fSession.parent_path = "
 
 
   sealed case class Log_Info(
@@ -754,7 +754,7 @@
     }
 
     // scheduler loop
-    case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int)
+    case class Result(current: Boolean, heap: String, rc: Int)
 
     def sleep(): Unit = Thread.sleep(500)
 
@@ -775,7 +775,7 @@
             val res = job.join
             progress.echo(res.err)
 
-            val (parent_path, heap) =
+            val heap =
               if (res.rc == 0) {
                 (output_dir + log(name)).file.delete
 
@@ -784,13 +784,7 @@
                 File.write_gzip(output_dir + log_gz(name),
                   sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out)
 
-                val parent_path =
-                  if (job.info.options.bool("browser_info"))
-                    res.out_lines.find(_.startsWith(SESSION_PARENT_PATH))
-                      .map(_.substring(SESSION_PARENT_PATH.length))
-                  else None
-
-                (parent_path, heap)
+                heap
               }
               else {
                 (output_dir + Path.basic(name)).file.delete
@@ -805,10 +799,10 @@
                   progress.echo("\n" + cat_lines(tail))
                 }
 
-                (None, no_heap)
+                no_heap
               }
             loop(pending - name, running - name,
-              results + (name -> Result(false, parent_path, heap, res.rc)))
+              results + (name -> Result(false, heap, res.rc)))
             //}}}
           case None if (running.size < (max_jobs max 1)) =>
             //{{{ check/start next job
@@ -816,7 +810,7 @@
               case Some((name, info)) =>
                 val parent_result =
                   info.parent match {
-                    case None => Result(true, None, no_heap, 0)
+                    case None => Result(true, no_heap, 0)
                     case Some(parent) => results(parent)
                   }
                 val output = output_dir + Path.basic(name)
@@ -839,10 +833,10 @@
                 val all_current = current && parent_result.current
 
                 if (all_current)
-                  loop(pending - name, running, results + (name -> Result(true, None, heap, 0)))
+                  loop(pending - name, running, results + (name -> Result(true, heap, 0)))
                 else if (no_build) {
                   if (verbose) progress.echo("Skipping " + name + " ...")
-                  loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
+                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
                 }
                 else if (parent_result.rc == 0 && !progress.stopped) {
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
@@ -853,7 +847,7 @@
                 }
                 else {
                   progress.echo(name + " CANCELLED")
-                  loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
+                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
                 }
               case None => sleep(); loop(pending, running, results)
             }
@@ -874,11 +868,11 @@
       else loop(queue, Map.empty, Map.empty)
 
     val session_entries =
-      (for ((name, res) <- results.iterator if res.parent_path.isDefined)
-        yield (res.parent_path.get, name)).toList.groupBy(_._1).map(
-          { case (p, es) => (p, es.map(_._2).sorted) })
-    for ((p, names) <- session_entries)
-      Present.update_index(browser_info + Path.explode(p), names)
+      (for ((name, res) <- results.iterator)
+        yield (full_tree(name).chapter, name)).toList.groupBy(_._1).map(
+          { case (chapter, es) => (chapter, es.map(_._2).sorted) })
+    for ((chapter, names) <- session_entries)
+      Present.update_chapter_index(browser_info, chapter, names)
 
     val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
     if (rc != 0 && (verbose || !no_build)) {