--- 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;