use css
authorkleing
Mon, 12 Apr 2004 23:52:15 +0200
changeset 14540 0417e7ed93fd
parent 14539 90c625edaee1
child 14541 0a7743e2f8dd
use css use Graphbrowser.jar instead of .class files
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Apr 12 23:51:00 2004 +0200
+++ b/src/Pure/Thy/present.ML	Mon Apr 12 23:52:15 2004 +0200
@@ -375,12 +375,10 @@
       if length path > 1 then update_index parent_html_prefix name else ();
       (case readme of None => () | Some path => File.copy path (Path.append html_prefix path));
       write_graph graph (Path.append html_prefix graph_path);
-      copy_files (Path.unpack "~~/lib/browser/awtUtilities/*.class")
-        (Path.append html_prefix (Path.basic "awtUtilities"));
-      copy_files (Path.unpack "~~/lib/browser/GraphBrowser/*.class")
-        (Path.append html_prefix (Path.basic "GraphBrowser"));
+      copy_files (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix;
       seq (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
         (HTML.applet_pages name (Url.file index_path, name));
+      copy_files (Path.unpack "~~/lib/html/isabelle.css") html_prefix;
       seq finish_html thys;
       seq (uncurry File.write) files;
       conditional verbose (fn () =>