finish browser_info: invoke isabelle browser -b to ensure that the jar really exists;
authorwenzelm
Fri, 05 Mar 2010 21:29:55 +0100
changeset 35588 f1429d5df3d2
parent 35587 f037aa6699c3
child 35591 ad7d2f9cc47d
finish browser_info: invoke isabelle browser -b to ensure that the jar really exists;
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Mar 05 21:26:21 2010 +0100
+++ b/src/Pure/Thy/present.ML	Fri Mar 05 21:29:55 2010 +0100
@@ -402,6 +402,7 @@
       if length path > 1 then update_index parent_html_prefix name else ();
       (case readme of NONE => () | SOME path => File.copy path html_prefix);
       write_graph sorted_graph (Path.append html_prefix graph_path);
+      File.isabelle_tool "browser" "-b";
       File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
       List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
         (HTML.applet_pages name (Url.File index_path, name));