begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear!
authorwenzelm
Tue, 08 Jul 2008 16:19:24 +0200
changeset 27491 c8178a6a6480
parent 27490 ac1d6e87aa52
child 27492 77ec4ad35ca2
begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear! replaced warning by error for non-existant theory/ML info;
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Jul 08 16:19:23 2008 +0200
+++ b/src/Pure/Thy/present.ML	Tue Jul 08 16:19:24 2008 +0200
@@ -183,7 +183,7 @@
 fun change_theory_info name f =
   change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
     (case Symtab.lookup theories name of
-      NONE => (warning ("Browser info: cannot access theory document " ^ quote name); info)
+      NONE => error ("Browser info: cannot access theory document " ^ quote name)
     | SOME info => (Symtab.update (name, map_theory_info f info) theories, files,
         tex_index, html_index, graph)));
 
@@ -474,15 +474,15 @@
             val base_html = html_ext base;
             val _ = add_file (Path.append html_prefix base_html,
               HTML.ml_file (Url.File base) (File.read path));
-          in (SOME (Url.File base_html), Url.File raw_path, loadit) end
-      | NONE =>
-          (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
-            (NONE, Url.File raw_path, loadit)));
+            in (Url.File base_html, Url.File raw_path, loadit) end
+      | NONE => error ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path)));
+
+    val files_html = map prep_file files;
 
     fun prep_html_source (tex_source, html_source, html) =
       let
         val txt = HTML.begin_theory (Url.File index_path, session)
-          name parent_specs (map prep_file files) (Buffer.content html_source)
+          name parent_specs files_html (Buffer.content html_source)
       in (tex_source, Buffer.empty, Buffer.add txt html) end;
 
     val entry =