src/Pure/Isar/isar_output.ML
changeset 9828 1d8bc4f1833e
parent 9750 270cd9831e7b
child 9863 67cdb658e422
equal deleted inserted replaced
9827:ce6e22ff89c3 9828:1d8bc4f1833e
   269   if ! quotes then Pretty.quote prt else prt;
   269   if ! quotes then Pretty.quote prt else prt;
   270 
   270 
   271 fun cond_display prt =
   271 fun cond_display prt =
   272   if ! display then
   272   if ! display then
   273     Pretty.string_of (Pretty.indent (! indent) prt)
   273     Pretty.string_of (Pretty.indent (! indent) prt)
   274     |> enclose "\n\\begin{isabelle}%\n" "\n\\end{isabelle}%\n"
   274     |> enclose "%\n\\begin{isabelle}%\n" "%\n\\end{isabelle}%\n"
   275   else
   275   else
   276     Pretty.str_of prt
   276     Pretty.str_of prt
   277     |> enclose "\\isa{" "}";
   277     |> enclose "\\isa{" "}";
   278 
   278 
   279 
   279