# HG changeset patch
# User wenzelm
# Date 1279831835 -7200
# Node ID 1d812ff95a14b2905a8678cfe46bb29f794ece13
# Parent  4857eab312982de5904646ae99bf806ccfd776cb
refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;

diff -r 4857eab31298 -r 1d812ff95a14 lib/html/isabelle.css
--- a/lib/html/isabelle.css	Thu Jul 22 22:39:31 2010 +0200
+++ b/lib/html/isabelle.css	Thu Jul 22 22:50:35 2010 +0200
@@ -14,9 +14,6 @@
 .name     { font-style: italic; }
 .filename { font-family: fixed; }
 
-/* hide hr for this style */
-hr { height: 0px; border: 0px; }
-
 
 /* basic syntax markup */
 
diff -r 4857eab31298 -r 1d812ff95a14 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu Jul 22 22:39:31 2010 +0200
+++ b/src/Pure/Thy/html.ML	Thu Jul 22 22:50:35 2010 +0200
@@ -309,7 +309,7 @@
   begin_document ("Index of " ^ session) ^ up_link up ^
   para ("View " ^ href_path graph "theory dependencies" ^
     implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
-  "\n</div>\n<hr/>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
+  "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
 
 fun choice chs s = space_implode " " (map (fn (s', lnk) =>
   enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
@@ -329,12 +329,12 @@
         (name, begin_document ("Theory dependencies of " ^ session) ^
           back_link back ^
           para browser_size ^
-          "\n</div>\n<hr/>\n<div class=\"graphbrowser\">\n\
+          "\n</div>\n<div class=\"graphbrowser\">\n\
           \<applet code=\"GraphBrowser/GraphBrowser.class\" \
           \archive=\"GraphBrowser.jar\" \
           \width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\
           \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\
-          \</applet>\n<hr/>" ^ end_document)
+          \</applet>" ^ end_document)
       end;
   in map applet_page sizes end;
 
@@ -345,15 +345,15 @@
 
 fun session_entries [] = "</ul>"
   | session_entries es =
-      "</ul>\n</div>\n<hr/>\n<div class=\"sessions\">\n\
+      "</ul>\n</div>\n<div class=\"sessions\">\n\
       \<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
 
 
 (* theory *)
 
 val theory_source = enclose
-  "\n</div>\n<hr/>\n<div class=\"source\">\n<pre>"
-  "</pre>\n<hr/>\n";
+  "\n</div>\n<div class=\"source\">\n<pre>"
+  "</pre>\n";
 
 
 local
@@ -383,9 +383,9 @@
 
 fun external_file path str =
   begin_document ("File " ^ Url.implode path) ^
-  "\n</div>\n<hr/><div class=\"external_source\">\n" ^
+  "\n</div><div class=\"external_source\">\n" ^
   verbatim str ^
-  "\n</div>\n<hr/>\n<div class=\"external_footer\">" ^
+  "\n</div>\n<div class=\"external_footer\">" ^
   end_document;
 
 end;