| changeset 49827 | 77582720af96 |
| parent 49657 | 40e4feac2921 |
| child 49843 | afddf4e26fac |
--- a/src/Pure/General/pretty.scala Thu Oct 11 21:02:19 2012 +0200 +++ b/src/Pure/General/pretty.scala Thu Oct 11 23:10:49 2012 +0200 @@ -59,7 +59,8 @@ val FBreak = XML.Text("\n") - val Separator = XML.elem(Isabelle_Markup.SEPARATOR, List(FBreak)) + val Separator = List(XML.elem(Isabelle_Markup.SEPARATOR, List(XML.Text(space))), FBreak) + def separate(ts: List[XML.Tree]): XML.Body = ts.map(t => t :: Separator).flatten /* formatted output */