tuned;
authorwenzelm
Tue, 12 Mar 2013 18:44:48 +0100
changeset 51401 f390b59b4b4a
parent 51400 96361e8f0a54
child 51402 b05cd411d3d3
tuned;
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Mar 12 18:30:28 2013 +0100
+++ b/src/Pure/Thy/present.ML	Tue Mar 12 18:44:48 2013 +0100
@@ -249,14 +249,12 @@
       val docs =
         (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
           map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
-      val index_text =  (* FIXME move to finish!? *)
-        HTML.begin_session_index name docs (Url.explode "medium.html");
     in
       session_info :=
         SOME (make_session_info (name, chapter, info_path, info, doc,
           doc_graph, doc_output, documents, doc_dump, verbose, readme));
       browser_info := init_browser_info (chapter, name) thys;
-      add_html_index (0, index_text)
+      add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
     end;