no check for bibtex entries from other sessions;
authorwenzelm
Fri, 29 Dec 2017 21:17:43 +0100
changeset 67302 48ca44fdc038
parent 67301 e255c76db052
child 67303 a77c0dd8bb7c
no check for bibtex entries from other sessions;
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Dec 29 19:53:43 2017 +0100
+++ b/src/Pure/Thy/present.ML	Fri Dec 29 21:17:43 2017 +0100
@@ -312,13 +312,15 @@
       val html_source = HTML.theory symbols name parent_specs (mk_text ());
       val _ = init_theory_info name (make_theory_info ("", html_source));
 
-      val _ =
+      val bibtex_entries' =
         if is_session_theory thy then
           (add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
-           add_tex_index (update_time, Latex.theory_entry name))
-        else ();
+           add_tex_index (update_time, Latex.theory_entry name);
+           bibtex_entries)
+        else [];
     in
-      Browser_Info.put {chapter = chapter, name = session_name, bibtex_entries = bibtex_entries} thy
+      thy
+      |> Browser_Info.put {chapter = chapter, name = session_name, bibtex_entries = bibtex_entries'}
     end);
 
 end;