added line break for 'uses';
authorwenzelm
Wed, 31 Aug 2005 15:46:48 +0200
changeset 17209 2ae243868a62
parent 17208 49bc1bdc7b6e
child 17210 e80fd664a119
added line break for 'uses';
src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Wed Aug 31 15:46:47 2005 +0200
+++ b/src/Pure/Thy/html.ML	Wed Aug 31 15:46:48 2005 +0200
@@ -380,7 +380,7 @@
   fun imports Bs =
     keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs);
 
-  fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps);
+  fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br>\n";
 in
 
 fun begin_theory up A Bs Ps body =