support for pretty blocks that are "open" and thus have no impact on formatting, only on markup;
effectively revert 2cb4a2970941 and unify pretty-printing in Scala and ML, following Scala before that change;
build error messages are properly formatted again (amending 320bcbf34849): "no_report" markup does not affect its enclosed line break anymore;
theory MicroJava
imports
"J/JTypeSafe"
"J/Example"
"J/JListExample"
"JVM/JVMListExample"
"JVM/JVMDefensive"
"BV/LBVJVM"
"BV/BVNoTypeError"
"BV/BVExample"
"Comp/CorrComp"
"Comp/CorrCompTp"
begin
end