| changeset 49843 | afddf4e26fac |
| parent 49827 | 77582720af96 |
| child 50201 | c26369c9eda6 |
--- a/src/Pure/General/pretty.scala Fri Oct 12 22:53:20 2012 +0200 +++ b/src/Pure/General/pretty.scala Fri Oct 12 23:38:48 2012 +0200 @@ -60,7 +60,7 @@ val FBreak = XML.Text("\n") 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 + def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten /* formatted output */