display: avoid empty lines;
authorwenzelm
Mon, 04 Sep 2000 18:38:53 +0200
changeset 9828 1d8bc4f1833e
parent 9827 ce6e22ff89c3
child 9829 bf49c3796599
display: avoid empty lines;
src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Mon Sep 04 11:21:24 2000 +0200
+++ b/src/Pure/Isar/isar_output.ML	Mon Sep 04 18:38:53 2000 +0200
@@ -271,7 +271,7 @@
 fun cond_display prt =
   if ! display then
     Pretty.string_of (Pretty.indent (! indent) prt)
-    |> enclose "\n\\begin{isabelle}%\n" "\n\\end{isabelle}%\n"
+    |> enclose "%\n\\begin{isabelle}%\n" "%\n\\end{isabelle}%\n"
   else
     Pretty.str_of prt
     |> enclose "\\isa{" "}";