# HG changeset patch
# User berghofe
# Date 1051516692 -7200
# Node ID 21615e44ba886cfb1ecca7f9a2c92b45f75346b9
# Parent  d572aeea3ff3ea9ea4621e73f1267c598a1adc66
Added "break" flag to allow line breaks within \isa{...}

diff -r d572aeea3ff3 -r 21615e44ba88 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Sun Apr 27 22:53:11 2003 +0200
+++ b/src/Pure/Isar/isar_output.ML	Mon Apr 28 09:58:12 2003 +0200
@@ -257,6 +257,7 @@
 val quotes = ref false;
 val indent = ref 0;
 val source = ref false;
+val break = ref false;
 
 val _ = add_options
  [("show_types", Library.setmp Syntax.show_types o boolean),
@@ -264,6 +265,7 @@
   ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
   ("long_names", Library.setmp NameSpace.long_names o boolean),
   ("display", Library.setmp display o boolean),
+  ("break", Library.setmp break o boolean),
   ("quotes", Library.setmp quotes o boolean),
   ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
   ("margin", Pretty.setmp_margin o integer),
@@ -282,7 +284,7 @@
     Pretty.string_of (Pretty.indent (! indent) prt)
     |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   else
-    Pretty.str_of prt
+    (if ! break then Pretty.string_of else Pretty.str_of) prt
     |> enclose "\\isa{" "}";
 
 fun tweak_line s =