# HG changeset patch
# User wenzelm
# Date 1444399756 -7200
# Node ID cf40b6b1de5493b23d236dbf2d26d3eceb7358bc
# Parent  17944b500166669a950f75c70caee4c138d5cfcb
more Present operations on Scala side;

diff -r 17944b500166 -r cf40b6b1de54 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Oct 09 16:07:14 2015 +0200
+++ b/src/Pure/Thy/present.ML	Fri Oct 09 16:09:16 2015 +0200
@@ -246,8 +246,8 @@
     val {theories, tex_index, html_index} = Synchronized.value browser_info;
     val thys = Symtab.dest theories;
 
-    val chapter_prefix = Path.append info_path (Path.basic chapter);
-    val session_prefix = Path.append chapter_prefix (Path.basic name);
+    val session_prefix =
+      Path.append (Path.append info_path (Path.basic chapter)) (Path.basic name);
 
     fun finish_html (a, {html_source, ...}: theory_info) =
       File.write (Path.append session_prefix (html_path a)) html_source;
@@ -257,9 +257,7 @@
        (Isabelle_System.mkdirs session_prefix;
         File.write_buffer (Path.append session_prefix index_path)
           (index_buffer html_index |> Buffer.add HTML.end_document);
-        Isabelle_System.copy_file graph_file (Path.append session_prefix session_graph_path);
         (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
-        Isabelle_System.copy_file (Path.explode "~~/etc/isabelle.css") session_prefix;
         List.app finish_html thys;
         if verbose
         then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
diff -r 17944b500166 -r cf40b6b1de54 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Fri Oct 09 16:07:14 2015 +0200
+++ b/src/Pure/Thy/present.scala	Fri Oct 09 16:09:16 2015 +0200
@@ -7,6 +7,8 @@
 package isabelle
 
 
+import java.io.{File => JFile}
+
 import scala.collection.immutable.SortedMap
 
 
@@ -59,9 +61,9 @@
     File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
   }
 
-  def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)])
+  def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
   {
-    val dir = info_path + Path.basic(chapter)
+    val dir = browser_info + Path.basic(chapter)
     Isabelle_System.mkdirs(dir)
 
     val sessions0 =
@@ -73,4 +75,36 @@
     write_sessions(dir, sessions)
     File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
   }
+
+  def make_global_index(browser_info: Path)
+  {
+    if (!(browser_info + Path.explode("index.html")).is_file) {
+      Isabelle_System.mkdirs(browser_info)
+      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")))
+    }
+  }
+
+
+  /* finish session */
+
+  def finish(
+    progress: Progress,
+    browser_info: Path,
+    graph_file: JFile,
+    info: Build.Session_Info,
+    name: String)
+  {
+    val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
+
+    if (info.options.bool("browser_info")) {
+      Isabelle_System.mkdirs(session_prefix)
+      File.copy(graph_file, (session_prefix + Path.basic("session_graph.pdf")).file)
+      File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix)
+    }
+  }
 }
diff -r 17944b500166 -r cf40b6b1de54 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Oct 09 16:07:14 2015 +0200
+++ b/src/Pure/Tools/build.scala	Fri Oct 09 16:09:16 2015 +0200
@@ -628,6 +628,9 @@
     {
       val res = result.join
 
+      if (res.rc == 0 && !is_pure(name))
+        Present.finish(progress, browser_info, graph_file, info, name)
+
       graph_file.delete
       args_file.delete
       timeout_request.foreach(_.cancel)
@@ -958,16 +961,7 @@
       for ((chapter, entries) <- browser_chapters)
         Present.update_chapter_index(browser_info, chapter, entries)
 
-      if (browser_chapters.nonEmpty && !(browser_info + Path.explode("index.html")).is_file)
-      {
-        Isabelle_System.mkdirs(browser_info)
-        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")))
-      }
+      if (browser_chapters.nonEmpty) Present.make_global_index(browser_info)
     }