# HG changeset patch # User wenzelm # Date 1215526764 -7200 # Node ID c8178a6a6480602d91ba1e64daf88f4fa1c0761f # Parent ac1d6e87aa52b9fd53571b610cf90f8a53b02ce1 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; diff -r ac1d6e87aa52 -r c8178a6a6480 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 =