src/Pure/Tools/build.scala

       if (is_pure(name)) Options.encode(info.options)
       else
         {
           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 =
       Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
         (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->

   private val LOG = Path.explode("log")
   private def log(name: String): Path = LOG + Path.basic(name)
   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(
     name: String,
     stats: List[Properties.T],

         if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
       }
     }
 
     // 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)
 
     @tailrec def loop(
       pending: Queue,

             //{{{ finish job
 
             val res = job.join
             progress.echo(res.err)
 
-            val (parent_path, heap) =
+            val heap =
               if (res.rc == 0) {
                 (output_dir + log(name)).file.delete
 
                 val sources = make_stamp(name)
                 val heap = heap_stamp(job.output_path)
                 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
                 (output_dir + log_gz(name)).file.delete
 

                   val lines = res.out_lines.filterNot(_.startsWith("\f"))
                   val tail = lines.drop(lines.length - 20 max 0)
                   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
             pending.dequeue(running.isDefinedAt(_)) match {
               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)
                 val do_output = build_heap || queue.is_inner(name)
 

                   }
                 }
                 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 + " ...")
                   val job =
                     new Job(progress, name, info, output, do_output, verbose, browser_info,
                       queue.command_timings(name))
                   loop(pending, running + (name -> (parent_result.heap, job)), results)
                 }
                 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)
             }
             ///}}}
           case None => sleep(); loop(pending, running, results)

         Map.empty[String, Result]
       }
       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)) {
       val unfinished =
         (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList