# HG changeset patch
# User wenzelm
# Date 1363110288 -3600
# Node ID f390b59b4b4a9769ef311d092e51038a0cb86000
# Parent  96361e8f0a54d0b6e7e35444b65251c0f4d579d7
tuned;

diff -r 96361e8f0a54 -r f390b59b4b4a 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;