diff -r c073006e0137 -r 68de2a2780b3 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML Mon Aug 11 18:37:51 2008 +0200
+++ b/src/Pure/Thy/html.ML Mon Aug 11 20:56:32 2008 +0200
@@ -269,7 +269,7 @@
| href_opt_path (SOME p) txt = href_path p txt;
fun para txt = "\n
" ^ txt ^ "
\n";
-fun preform txt = "" ^ txt ^ "
";
+fun preform txt = "" ^ txt ^ "
";
val verbatim = preform o output;
@@ -353,7 +353,7 @@
(* theory *)
fun verbatim_source ss =
- "\n\n
\n\n
\n\n
" ^
implode (output_symbols ss) ^
"
\n
\n
\n\n";
@@ -402,14 +402,14 @@
Output.output o Pretty.setmp_margin 80 Pretty.string_of o
setmp show_question_marks false (ProofContext.pretty_thm ctxt);
-fun thm ctxt th = preform (prefix_lines " " (html_mode (string_of_thm ctxt) th));
+fun thm ctxt th = prefix_lines " " (html_mode (string_of_thm ctxt) th);
fun thm_name "" = ""
| thm_name a = " " ^ name (a ^ ":");
in
-fun result ctxt k (a, ths) = para (cat_lines ((command k ^ thm_name a) :: map (thm ctxt) ths));
+fun result ctxt k (a, ths) = preform (cat_lines ((command k ^ thm_name a) :: map (thm ctxt) ths));
fun results _ _ [] = ""
| results ctxt k (res :: ress) = cat_lines (result ctxt k res :: map (result ctxt "and") ress);