src/Pure/Thy/present.ML
changeset 7769 700439dc581e
parent 7763 fdf7c941a22b
child 7789 57d20133224e
equal deleted inserted replaced
7768:b106e4af1301 7769:700439dc581e
   327     (fn {name, html_prefix, doc_prefix, graph_path, all_graph_path, path, ...} =>
   327     (fn {name, html_prefix, doc_prefix, graph_path, all_graph_path, path, ...} =>
   328   let
   328   let
   329     val {theories, tex_index, html_index, graph, all_graph} = ! browser_info;
   329     val {theories, tex_index, html_index, graph, all_graph} = ! browser_info;
   330 
   330 
   331     fun finish_node (a, {tex_source, html_source = _, html}) =
   331     fun finish_node (a, {tex_source, html_source = _, html}) =
   332      (apsome (fn p => Buffer.write_nonempty (Path.append p (tex_path a)) tex_source) doc_prefix;
   332      (apsome (fn p => Buffer.write (Path.append p (tex_path a)) tex_source) doc_prefix;
   333       Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html));
   333       Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html));
   334   in
   334   in
   335     seq finish_node (Symtab.dest theories);
   335     seq finish_node (Symtab.dest theories);
   336     Buffer.write (Path.append html_prefix pre_index_path) html_index;
   336     Buffer.write (Path.append html_prefix pre_index_path) html_index;
   337     apsome (fn p => Buffer.write (Path.append p doc_index_path) tex_index) doc_prefix;
   337     apsome (fn p => Buffer.write (Path.append p doc_index_path) tex_index) doc_prefix;