more Present operations on Scala side;
authorwenzelm
Fri Oct 09 16:09:16 2015 +0200 (2015-10-09)
changeset 61372cf40b6b1de54
parent 61371 17944b500166
child 61373 16ed9b97c72d
more Present operations on Scala side;
src/Pure/Thy/present.ML
src/Pure/Thy/present.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/present.ML	Fri Oct 09 16:07:14 2015 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Fri Oct 09 16:09:16 2015 +0200
     1.3 @@ -246,8 +246,8 @@
     1.4      val {theories, tex_index, html_index} = Synchronized.value browser_info;
     1.5      val thys = Symtab.dest theories;
     1.6  
     1.7 -    val chapter_prefix = Path.append info_path (Path.basic chapter);
     1.8 -    val session_prefix = Path.append chapter_prefix (Path.basic name);
     1.9 +    val session_prefix =
    1.10 +      Path.append (Path.append info_path (Path.basic chapter)) (Path.basic name);
    1.11  
    1.12      fun finish_html (a, {html_source, ...}: theory_info) =
    1.13        File.write (Path.append session_prefix (html_path a)) html_source;
    1.14 @@ -257,9 +257,7 @@
    1.15         (Isabelle_System.mkdirs session_prefix;
    1.16          File.write_buffer (Path.append session_prefix index_path)
    1.17            (index_buffer html_index |> Buffer.add HTML.end_document);
    1.18 -        Isabelle_System.copy_file graph_file (Path.append session_prefix session_graph_path);
    1.19          (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
    1.20 -        Isabelle_System.copy_file (Path.explode "~~/etc/isabelle.css") session_prefix;
    1.21          List.app finish_html thys;
    1.22          if verbose
    1.23          then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
     2.1 --- a/src/Pure/Thy/present.scala	Fri Oct 09 16:07:14 2015 +0200
     2.2 +++ b/src/Pure/Thy/present.scala	Fri Oct 09 16:09:16 2015 +0200
     2.3 @@ -7,6 +7,8 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import java.io.{File => JFile}
     2.8 +
     2.9  import scala.collection.immutable.SortedMap
    2.10  
    2.11  
    2.12 @@ -59,9 +61,9 @@
    2.13      File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
    2.14    }
    2.15  
    2.16 -  def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)])
    2.17 +  def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
    2.18    {
    2.19 -    val dir = info_path + Path.basic(chapter)
    2.20 +    val dir = browser_info + Path.basic(chapter)
    2.21      Isabelle_System.mkdirs(dir)
    2.22  
    2.23      val sessions0 =
    2.24 @@ -73,4 +75,36 @@
    2.25      write_sessions(dir, sessions)
    2.26      File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
    2.27    }
    2.28 +
    2.29 +  def make_global_index(browser_info: Path)
    2.30 +  {
    2.31 +    if (!(browser_info + Path.explode("index.html")).is_file) {
    2.32 +      Isabelle_System.mkdirs(browser_info)
    2.33 +      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
    2.34 +        browser_info + Path.explode("isabelle.gif"))
    2.35 +      File.write(browser_info + Path.explode("index.html"),
    2.36 +        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
    2.37 +        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
    2.38 +        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
    2.39 +    }
    2.40 +  }
    2.41 +
    2.42 +
    2.43 +  /* finish session */
    2.44 +
    2.45 +  def finish(
    2.46 +    progress: Progress,
    2.47 +    browser_info: Path,
    2.48 +    graph_file: JFile,
    2.49 +    info: Build.Session_Info,
    2.50 +    name: String)
    2.51 +  {
    2.52 +    val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
    2.53 +
    2.54 +    if (info.options.bool("browser_info")) {
    2.55 +      Isabelle_System.mkdirs(session_prefix)
    2.56 +      File.copy(graph_file, (session_prefix + Path.basic("session_graph.pdf")).file)
    2.57 +      File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix)
    2.58 +    }
    2.59 +  }
    2.60  }
     3.1 --- a/src/Pure/Tools/build.scala	Fri Oct 09 16:07:14 2015 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Fri Oct 09 16:09:16 2015 +0200
     3.3 @@ -628,6 +628,9 @@
     3.4      {
     3.5        val res = result.join
     3.6  
     3.7 +      if (res.rc == 0 && !is_pure(name))
     3.8 +        Present.finish(progress, browser_info, graph_file, info, name)
     3.9 +
    3.10        graph_file.delete
    3.11        args_file.delete
    3.12        timeout_request.foreach(_.cancel)
    3.13 @@ -958,16 +961,7 @@
    3.14        for ((chapter, entries) <- browser_chapters)
    3.15          Present.update_chapter_index(browser_info, chapter, entries)
    3.16  
    3.17 -      if (browser_chapters.nonEmpty && !(browser_info + Path.explode("index.html")).is_file)
    3.18 -      {
    3.19 -        Isabelle_System.mkdirs(browser_info)
    3.20 -        File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
    3.21 -          browser_info + Path.explode("isabelle.gif"))
    3.22 -        File.write(browser_info + Path.explode("index.html"),
    3.23 -          File.read(Path.explode("~~/lib/html/library_index_header.template")) +
    3.24 -          File.read(Path.explode("~~/lib/html/library_index_content.template")) +
    3.25 -          File.read(Path.explode("~~/lib/html/library_index_footer.template")))
    3.26 -      }
    3.27 +      if (browser_chapters.nonEmpty) Present.make_global_index(browser_info)
    3.28      }
    3.29  
    3.30