HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
authorwenzelm
Mon, 16 Nov 2020 22:23:04 +0100
changeset 72861 830222403681
parent 72860 65554bac121b
child 72862 e788488b0607
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
src/Pure/PIDE/session.ML
src/Pure/Thy/html.ML
src/Pure/Thy/html.scala
src/Pure/Thy/present.ML
src/Pure/Thy/present.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
--- a/src/Pure/PIDE/session.ML	Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/PIDE/session.ML	Mon Nov 16 22:23:04 2020 +0100
@@ -9,7 +9,7 @@
   val get_name: unit -> string
   val welcome: unit -> string
   val get_keywords: unit -> Keyword.keywords
-  val init: bool -> Path.T -> string list -> string -> string * string -> bool -> unit
+  val init: string -> string * string -> unit
   val shutdown: unit -> unit
   val finish: unit -> unit
 end;
@@ -45,12 +45,11 @@
 
 (* init *)
 
-fun init info info_path documents parent (chapter, name) verbose =
+fun init parent (chapter, name) =
   (Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) =>
     if parent_name <> parent orelse not parent_finished then
       error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
-    else ({chapter = chapter, name = name}, false));
-    Present.init info info_path documents (chapter, name) verbose);
+    else ({chapter = chapter, name = name}, false)));
 
 
 (* finish *)
@@ -64,7 +63,6 @@
  (shutdown ();
   Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ());
   Thy_Info.finish ();
-  Present.finish ();
   shutdown ();
   update_keywords ();
   Synchronized.change session (apsnd (K true)));
--- a/src/Pure/Thy/html.ML	Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/html.ML	Mon Nov 16 22:23:04 2020 +0100
@@ -1,5 +1,5 @@
 (*  Title:      Pure/Thy/html.ML
-    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
+    Author:     Makarius
 
 HTML presentation elements.
 *)
@@ -11,11 +11,14 @@
   val no_symbols: symbols
   val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output
   type text = string
+  val name: symbols -> string -> text
+  val keyword: symbols -> string -> text
+  val command: symbols -> string -> text
+  val href_name: string -> string -> string
+  val href_path: Url.T -> string -> string
+  val href_opt_path: Url.T option -> string -> string
   val begin_document: symbols -> string -> text
   val end_document: text
-  val begin_session_index: symbols -> string -> Url.T -> (Url.T * string) list -> text
-  val theory_entry: symbols -> Url.T * string -> text
-  val theory: symbols -> string -> (Url.T option * string) list -> text -> text
 end;
 
 structure HTML: HTML =
@@ -120,8 +123,6 @@
 fun href_opt_path NONE txt = txt
   | href_opt_path (SOME p) txt = href_path p txt;
 
-fun para txt = "\n<p>" ^ txt ^ "</p>\n";
-
 
 (* document *)
 
@@ -142,27 +143,4 @@
 
 val end_document = "\n</div>\n</body>\n</html>\n";
 
-
-(* session index *)
-
-fun begin_session_index symbols session graph docs =
-  begin_document symbols ("Session " ^ output symbols session) ^
-  para ("View " ^ href_path graph "theory dependencies" ^
-    implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
-  "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
-
-fun theory_entry symbols (p, s) = "<li>" ^ href_path p (output symbols s) ^ "</li>\n";
-
-
-(* theory *)
-
-fun theory symbols A Bs txt =
-  begin_document symbols ("Theory " ^ A) ^ "\n" ^
-  command symbols "theory" ^ " " ^ name symbols A ^ "<br/>\n" ^
-  keyword symbols "imports" ^ " " ^
-    space_implode " " (map (uncurry href_opt_path o apsnd (name symbols)) Bs) ^
-  "<br/>\n" ^
-  enclose "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" "</pre>\n" txt ^
-  end_document;
-
 end;
--- a/src/Pure/Thy/html.scala	Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/html.scala	Mon Nov 16 22:23:04 2020 +0100
@@ -155,6 +155,7 @@
   def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
   val no_text: XML.Tree = XML.Text("")
   val break: XML.Body = List(XML.elem("br"))
+  val nl: XML.Body = List(XML.Text("\n"))
 
   class Operator(val name: String)
   {
@@ -197,9 +198,11 @@
   def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
     descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) }))
 
-  def link(href: String, body: XML.Body = Nil): XML.Elem =
+  def link(href: String, body: XML.Body): XML.Elem =
     XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
 
+  def link(path: Path, body: XML.Body): XML.Elem = link(path.implode, body)
+
   def image(src: String, alt: String = ""): XML.Elem =
     XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
 
--- a/src/Pure/Thy/present.ML	Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/present.ML	Mon Nov 16 22:23:04 2020 +0100
@@ -1,168 +1,75 @@
 (*  Title:      Pure/Thy/present.ML
-    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
+    Author:     Makarius
 
-Theory presentation: HTML and PDF-LaTeX documents.
+Theory presentation: HTML and LaTeX documents.
 *)
 
 signature PRESENT =
 sig
-  val init: bool -> Path.T -> string list -> string * string -> bool -> unit
-  val finish: unit -> unit
-  val begin_theory: int -> HTML.text -> theory -> theory
+  val document_html_name: theory -> Path.binding
+  val document_tex_name: theory -> Path.binding
+  val html_name: theory -> Path.T
+  val export_html: theory -> Command_Span.span list -> unit
 end;
 
 structure Present: PRESENT =
 struct
 
-
-(** paths **)
-
-val html_ext = Path.ext "html";
-val html_path = html_ext o Path.basic;
-val index_path = Path.basic "index.html";
-val readme_html_path = Path.basic "README.html";
-val session_graph_path = Path.basic "session_graph.pdf";
-val document_path = Path.ext "pdf" o Path.basic;
-
-fun show_path path = Path.implode (Path.expand (File.full_path Path.current path));
-
+(** artefact names **)
 
-
-(** global browser info state **)
-
-(* type browser_info *)
-
-type browser_info =
- {html_theories: string Symtab.table,
-  html_index: (int * string) list};
-
-fun make_browser_info (html_theories, html_index) : browser_info =
-  {html_theories = html_theories, html_index = html_index};
-
-val empty_browser_info = make_browser_info (Symtab.empty, []);
+fun document_name ext thy =
+  Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext);
 
-fun map_browser_info f {html_theories, html_index} =
-  make_browser_info (f (html_theories, html_index));
-
-
-(* state *)
-
-val browser_info = Synchronized.var "browser_info" empty_browser_info;
-fun change_browser_info f = Synchronized.change browser_info (map_browser_info f);
-
-fun update_html name html = change_browser_info (apfst (Symtab.update (name, html)));
-
-fun add_html_index txt = change_browser_info (apsnd (cons txt));
+val document_html_name = document_name "html";
+val document_tex_name = document_name "tex";
 
-
-
-(** global session state **)
-
-(* session_info *)
-
-type session_info =
-  {name: string, chapter: string, info_path: Path.T, info: bool,
-    verbose: bool, readme: Path.T option};
-
-fun make_session_info (name, chapter, info_path, info, verbose, readme) =
-  {name = name, chapter = chapter, info_path = info_path, info = info,
-    verbose = verbose, readme = readme}: session_info;
+fun html_name thy = Path.basic (Context.theory_name thy ^ ".html");
 
 
-(* state *)
-
-val session_info = Unsynchronized.ref (NONE: session_info option);
-
-fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
-
-val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name;
-
-fun is_session_theory thy =
-  (case ! session_info of
-    NONE => false
-  | SOME {name, ...} => name = theory_qualifier thy);
-
-
-(** document preparation **)
-
-(* init session *)
-
-fun init info info_path documents (chapter, name) verbose =
-  let
-    val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
-    val symbols = Resources.html_symbols ();
-    val docs =
-      (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
-        map (fn name => (Url.File (document_path name), name)) documents;
-  in
-    session_info := SOME (make_session_info (name, chapter, info_path, info, verbose, readme));
-    Synchronized.change browser_info (K empty_browser_info);
-    add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs)
-  end;
-
+(* theory as HTML *)
 
-(* finish session -- output all generated text *)
-
-fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index));
-fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
-
-fun finish () = with_session_info () (fn {name, chapter, info, info_path, verbose, readme, ...} =>
-  let
-    val {html_theories, html_index} = Synchronized.value browser_info;
-
-    val session_prefix = info_path + Path.basic chapter + Path.basic name;
-
-    fun finish_html (a, html) = File.write (session_prefix + html_path a) html;
+local
 
-    val _ =
-      if info then
-       (Isabelle_System.make_directory session_prefix;
-        File.write_buffer (session_prefix + index_path)
-          (index_buffer html_index |> Buffer.add HTML.end_document);
-        (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
-        Symtab.fold (K o finish_html) html_theories ();
-        if verbose
-        then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
-        else ())
-      else ();
-  in
-    Synchronized.change browser_info (K empty_browser_info);
-    session_info := NONE
-  end);
-
-
-(* theory elements *)
-
-fun theory_link (curr_chapter, curr_session) thy =
+fun get_session_chapter thy =
   let
     val session = Resources.theory_qualifier (Context.theory_long_name thy);
     val chapter = Resources.session_chapter session;
-    val link = html_path (Context.theory_name thy);
+  in (session, chapter) end;
+
+fun theory_link thy thy' =
+  let
+    val ((session, chapter), (session', chapter')) = apply2 get_session_chapter (thy, thy');
+    val link = html_name thy';
   in
-    if curr_session = session then SOME link
-    else if curr_chapter = chapter then
-      SOME (Path.parent + Path.basic session + link)
+    if session = session' then SOME link
+    else if chapter = chapter' then SOME (Path.parent + Path.basic session + link)
     else if chapter = Context.PureN then NONE
     else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link)
   end;
 
-fun begin_theory update_time html thy =
-  with_session_info thy (fn {name = session_name, chapter, ...} =>
-    let
-      val name = Context.theory_name thy;
+fun theory_document symbols A Bs body =
+  HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^
+  HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "<br/>\n" ^
+  HTML.keyword symbols "imports" ^ " " ^
+    space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^
+  "<br/>\n\n</div>\n<div class=\"source\">\n<pre class=\"source\">" ::
+  body @ ["</pre>\n", HTML.end_document];
+
+in
 
-      val parent_specs =
-        Theory.parents_of thy |> map (fn parent =>
-          (Option.map Url.File (theory_link (chapter, session_name) parent),
-            (Context.theory_name parent)));
+fun export_html thy spans =
+  let
+    val name = Context.theory_name thy;
+    val parents =
+      Theory.parents_of thy |> map (fn thy' =>
+        (Option.map Url.File (theory_link thy thy'), Context.theory_name thy'));
 
-      val symbols = Resources.html_symbols ();
-      val _ = update_html name (HTML.theory symbols name parent_specs html);
-
-      val _ =
-        if is_session_theory thy then
-          add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name))
-        else ();
-    in thy end);
+    val symbols = Resources.html_symbols ();
+    val keywords = Thy_Header.get_keywords thy;
+    val body = map (HTML.present_span symbols keywords) spans;
+    val html = XML.blob (theory_document symbols name parents body);
+  in Export.export thy (document_html_name thy) html end
 
 end;
+
+end;
--- a/src/Pure/Thy/present.scala	Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/present.scala	Mon Nov 16 22:23:04 2020 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Thy/present.scala
     Author:     Makarius
 
-Theory presentation: HTML.
+Theory presentation: HTML and LaTeX documents.
 */
 
 package isabelle
@@ -74,27 +74,72 @@
   }
 
 
-  /* finish session */
+  /* present session */
+
+  val session_graph_path = Path.explode("session_graph.pdf")
+  val readme_path = Path.basic("README.html")
+
+  def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html"
+  def document_html_name(name: Document.Node.Name): String = "document/" + html_name(name)
+
+  def theory_link(name: Document.Node.Name): XML.Tree =
+    HTML.link(html_name(name), HTML.text(name.theory_base_name))
 
-  def finish(
-    browser_info: Path,
-    graph_pdf: Bytes,
-    info: Sessions.Info,
-    name: String)
+  def session_html(session: String, deps: Sessions.Deps, store: Sessions.Store): Path =
   {
-    val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
-    val session_fonts = session_prefix + Path.explode("fonts")
+    val info = deps.sessions_structure(session)
+    val options = info.options
+    val base = deps(session)
+
+    val session_dir = store.browser_info + info.chapter_session
+    val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts"))
+    for (entry <- Isabelle_Fonts.fonts(hidden = true))
+      File.copy(entry.path, session_fonts)
+
+    Bytes.write(session_dir + session_graph_path,
+      graphview.Graph_File.make_pdf(options, base.session_graph_display))
+
+    val links =
+    {
+      val deps_link =
+        HTML.link(session_graph_path, HTML.text("theory dependencies"))
 
-    if (info.options.bool("browser_info")) {
-      Isabelle_System.make_directory(session_fonts)
+      val readme_links =
+        if ((info.dir + readme_path).is_file) {
+          File.copy(info.dir + readme_path, session_dir + readme_path)
+          List(HTML.link(readme_path, HTML.text("README")))
+        }
+        else Nil
 
-      Bytes.write(session_prefix + session_graph_path, graph_pdf)
+      val document_links =
+        for ((name, _) <- info.documents)
+          yield HTML.link(Path.basic(name).pdf, HTML.text(name))
+
+      Library.separate(HTML.break ::: HTML.nl,
+        (deps_link :: readme_links ::: document_links).
+          map(link => HTML.text("View ") ::: List(link))).flatten
+    }
 
-      HTML.write_isabelle_css(session_prefix)
+    val theories =
+      using(store.open_database(session))(db =>
+        for {
+          name <- base.session_theories
+          entry <- Export.read_entry(db, session, name.theory, document_html_name(name))
+        } yield name -> entry.uncompressed(cache = store.xz_cache))
+
+    val theories_body =
+      HTML.itemize(for ((name, _) <- theories) yield List(theory_link(name)))
 
-      for (entry <- Isabelle_Fonts.fonts(hidden = true))
-        File.copy(entry.path, session_fonts)
-    }
+    val title = "Session " + session
+    HTML.write_document(session_dir, "index.html",
+      List(HTML.title(title + " (" + Distribution.version + ")")),
+      HTML.div("head", List(HTML.chapter(title), HTML.par(links))) ::
+       (if (theories.isEmpty) Nil
+        else List(HTML.div("theories", List(HTML.section("Theories"), theories_body)))))
+
+    for ((name, html) <- theories) Bytes.write(session_dir + Path.basic(html_name(name)), html)
+
+    session_dir
   }
 
 
@@ -193,7 +238,6 @@
   /** build documents **/
 
   val session_tex_path = Path.explode("session.tex")
-  val session_graph_path = Path.explode("session_graph.pdf")
 
   def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
   def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
@@ -331,7 +375,7 @@
     }
 
     if (info.options.bool("browser_info") || doc_output.isEmpty) {
-      output(store.browser_info + Path.basic(info.chapter) + Path.basic(session))
+      output(store.browser_info + info.chapter_session)
     }
 
     doc_output.foreach(output)
--- a/src/Pure/Thy/sessions.scala	Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Nov 16 22:23:04 2020 +0100
@@ -459,6 +459,8 @@
     export_files: List[(Path, Int, List[String])],
     meta_digest: SHA1.Digest)
   {
+    def chapter_session: Path = Path.basic(chapter) + Path.basic(name)
+
     def deps: List[String] = parent.toList ::: imports
 
     def deps_base(session_bases: String => Base): Base =
--- a/src/Pure/Thy/thy_info.ML	Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Nov 16 22:23:04 2020 +0100
@@ -53,6 +53,7 @@
 
 val _ =
   Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
+   (Present.export_html thy (map #span segments);
     if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
@@ -62,12 +63,12 @@
         else
           let
             val thy_name = Context.theory_name thy;
-            val document_tex_name = Path.explode_binding0 ("document/" ^ thy_name ^ ".tex");
+            val document_tex_name = Present.document_tex_name thy;
 
             val latex = Latex.isabelle_body thy_name body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
           in Export.export thy document_tex_name (XML.blob output) end
-      end));
+      end)));
 
 
 
@@ -302,13 +303,7 @@
     val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
     val elements = Thy_Element.parse_elements keywords spans;
 
-    val symbols = Resources.html_symbols ();
-    val html = implode (map (HTML.present_span symbols keywords) spans);
-
-    fun init () =
-      Resources.begin_theory master_dir header parents
-      |> Present.begin_theory update_time html;
-
+    fun init () = Resources.begin_theory master_dir header parents;
     val (results, thy) =
       cond_timeit true ("theory " ^ quote name)
         (fn () => excursion keywords master_dir last_timing init elements);
--- a/src/Pure/Tools/build.ML	Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Tools/build.ML	Mon Nov 16 22:23:04 2020 +0100
@@ -86,25 +86,23 @@
   Isabelle_Process.protocol_command "build_session"
     (fn [args_yxml] =>
         let
-          val (html_symbols, (command_timings, (verbose, (browser_info,
-            (documents, (parent_name, (chapter, (session_name, (master_dir,
-            (theories, (session_positions, (session_directories, (session_chapters,
-            (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) =
+          val (html_symbols, (command_timings, (parent_name, (chapter,
+            (session_name, (master_dir, (theories, (session_positions, (session_directories,
+            (session_chapters, (doc_names,
+            (global_theories, (loaded_theories, bibtex_entries))))))))))))) =
             YXML.parse_body args_yxml |>
               let
                 open XML.Decode;
                 val position = Position.of_properties o properties;
                 val path = Path.explode o string;
               in
-                pair (list (pair string int)) (pair (list properties) (pair bool (pair path
-                  (pair (list string) (pair string (pair string (pair string
-                    (pair path
-                      (pair (((list (pair Options.decode (list (pair string position))))))
-                        (pair (list (pair string properties))
-                          (pair (list (pair string string))
-                            (pair (list (pair string string)) (pair (list string)
-                              (pair (list (pair string string)) (pair (list string)
-                                (list (pair string (list string))))))))))))))))))
+                pair (list (pair string int)) (pair (list properties) (pair string (pair string
+                  (pair string (pair path
+                    (pair (((list (pair Options.decode (list (pair string position))))))
+                      (pair (list (pair string properties)) (pair (list (pair string string))
+                        (pair (list (pair string string)) (pair (list string)
+                          (pair (list (pair string string)) (pair (list string)
+                            (list (pair string (list string)))))))))))))))
               end;
 
           fun build () =
@@ -120,14 +118,7 @@
                    global_theories = global_theories,
                    loaded_theories = loaded_theories};
 
-              val _ =
-                Session.init
-                  (Options.default_bool "browser_info")
-                  browser_info
-                  documents
-                  parent_name
-                  (chapter, session_name)
-                  verbose;
+              val _ = Session.init parent_name (chapter, session_name);
 
               val last_timing = get_timings (fold update_timings command_timings empty_timings);
 
--- a/src/Pure/Tools/build.scala	Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Tools/build.scala	Mon Nov 16 22:23:04 2020 +0100
@@ -165,7 +165,6 @@
     val options: Options = NUMA.policy_options(info.options, numa_node)
 
     private val sessions_structure = deps.sessions_structure
-    private val documents = info.documents.map(_._1)
 
     private val future_result: Future[Process_Result] =
       Future.thread("build", uninterruptible = true) {
@@ -175,23 +174,22 @@
           YXML.string_of_body(
             {
               import XML.Encode._
-              pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode,
-                pair(list(string), pair(string, pair(string, pair(string, pair(Path.encode,
+              pair(list(pair(string, int)), pair(list(properties), pair(string, pair(string,
+                pair(string, pair(Path.encode,
                 pair(list(pair(Options.encode, list(pair(string, properties)))),
                 pair(list(pair(string, properties)),
                 pair(list(pair(string, string)),
                 pair(list(pair(string, string)),
                 pair(list(string),
                 pair(list(pair(string, string)),
-                pair(list(string), list(pair(string, list(string)))))))))))))))))))(
-              (Symbol.codes, (command_timings0, (verbose, (store.browser_info,
-                (documents, (parent, (info.chapter, (session_name, (Path.current,
-                (info.theories,
+                pair(list(string), list(pair(string, list(string))))))))))))))))(
+              (Symbol.codes, (command_timings0, (parent, (info.chapter,
+                (session_name, (Path.current, (info.theories,
                 (sessions_structure.session_positions,
                 (sessions_structure.dest_session_directories,
                 (sessions_structure.session_chapters,
                 (base.doc_names, (base.global_theories.toList,
-                (base.loaded_theories.keys, sessions_structure.bibtex_entries)))))))))))))))))
+                (base.loaded_theories.keys, sessions_structure.bibtex_entries))))))))))))))
             })
 
         val env =
@@ -373,20 +371,23 @@
 
         val document_errors =
           try {
-            if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && documents.nonEmpty) {
-              val document_progress =
-                new Progress {
-                  override def echo(msg: String): Unit =
-                    document_output.synchronized { document_output += msg }
-                  override def echo_document(path: Path): Unit =
-                    progress.echo_document(path)
-                }
-              Present.build_documents(session_name, deps, store, verbose = verbose,
-                verbose_latex = true, progress = document_progress)
+            if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok) {
+              if (info.documents.nonEmpty) {
+                val document_progress =
+                  new Progress {
+                    override def echo(msg: String): Unit =
+                      document_output.synchronized { document_output += msg }
+                    override def echo_document(path: Path): Unit =
+                      progress.echo_document(path)
+                  }
+                Present.build_documents(session_name, deps, store, verbose = verbose,
+                  verbose_latex = true, progress = document_progress)
+              }
+              if (info.options.bool("browser_info")) {
+                val dir = Present.session_html(session_name, deps, store)
+                if (verbose) progress.echo("Browser info at " + dir.absolute)
+              }
             }
-            val graph_pdf =
-              graphview.Graph_File.make_pdf(options, deps(session_name).session_graph_display)
-            Present.finish(store.browser_info, graph_pdf, info, session_name)
             Nil
           }
           catch { case Exn.Interrupt.ERROR(msg) => List(msg) }