# HG changeset patch
# User wenzelm
# Date 1007655406 -3600
# Node ID f879fcc9412d44d29e941e24b168bb4c6ba01928
# Parent  d0857ea70f23d269a3d866bf9f2c2541f9331d3a
tuned line breaks in HTML source;

diff -r d0857ea70f23 -r f879fcc9412d src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu Dec 06 17:16:30 2001 +0100
+++ b/src/Pure/Thy/html.ML	Thu Dec 06 17:16:46 2001 +0100
@@ -159,7 +159,7 @@
 fun href_opt_path None txt = txt
   | href_opt_path (Some p) txt = href_path p txt;
 
-fun para txt = "\n<p>\n" ^ txt ^ "\n</p>\n";
+fun para txt = "\n<p>" ^ txt ^ "</p>\n";
 fun preform txt = "<pre>" ^ txt ^ "</pre>";
 val verbatim = preform o output;
 
@@ -248,7 +248,7 @@
 in
 
 fun begin_theory up A Bs [] body = theory up A ^ parents Bs ^ ":\n" ^ body
-  | begin_theory up A Bs Ps body = theory up A ^ parents Bs ^ "<br>" ^ keyword "files" ^
+  | begin_theory up A Bs Ps body = theory up A ^ parents Bs ^ "<br>\n" ^ keyword "files" ^
       " " ^ files Ps ^ ":" ^ "\n" ^ body;
 end;