1.1 --- a/src/Pure/Thy/present.ML	Tue Mar 18 22:19:18 2008 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Tue Mar 18 23:25:06 2008 +0100
     1.3 @@ -462,15 +462,12 @@
     1.4          else Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
     1.5    in (link, name) end;
     1.6  
     1.7 -fun begin_theory update_time dir orig_files thy =
     1.8 +fun begin_theory update_time dir files thy =
     1.9      with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
    1.10    let
    1.11      val name = Context.theory_name thy;
    1.12      val parents = Theory.parents_of thy;
    1.13      val parent_specs = map (parent_link remote_path path) parents;
    1.14 -    val ml_path = ThyLoad.ml_path name;
    1.15 -    val files = map (apsnd SOME) orig_files @
    1.16 -      (if is_some (ThyLoad.check_file dir ml_path) then [(ml_path, NONE)] else []);
    1.17  
    1.18      fun prep_file (raw_path, loadit) =
    1.19        (case ThyLoad.check_ml dir raw_path of
    1.20 @@ -478,21 +475,17 @@
    1.21            let
    1.22              val base = Path.base path;
    1.23              val base_html = html_ext base;
    1.24 -          in
    1.25 -            add_file (Path.append html_prefix base_html,
    1.26 +            val _ = add_file (Path.append html_prefix base_html,
    1.27                HTML.ml_file (Url.File base) (File.read path));
    1.28 -            (SOME (Url.File base_html), Url.File raw_path, loadit)
    1.29 -          end
    1.30 +          in (SOME (Url.File base_html), Url.File raw_path, loadit) end
    1.31        | NONE =>
    1.32            (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
    1.33              (NONE, Url.File raw_path, loadit)));
    1.34  
    1.35 -    val files_html = map prep_file files;
    1.36 -
    1.37      fun prep_html_source (tex_source, html_source, html) =
    1.38        let
    1.39          val txt = HTML.begin_theory (Url.File index_path, session)
    1.40 -          name parent_specs files_html (Buffer.content html_source)
    1.41 +          name parent_specs (map prep_file files) (Buffer.content html_source)
    1.42        in (tex_source, Buffer.empty, Buffer.add txt html) end;
    1.43  
    1.44      val entry =