equal
deleted
inserted
replaced
58 } |
58 } |
59 |
59 |
60 val FBreak = XML.Text("\n") |
60 val FBreak = XML.Text("\n") |
61 |
61 |
62 val Separator = List(XML.elem(Isabelle_Markup.SEPARATOR, List(XML.Text(space))), FBreak) |
62 val Separator = List(XML.elem(Isabelle_Markup.SEPARATOR, List(XML.Text(space))), FBreak) |
63 def separate(ts: List[XML.Tree]): XML.Body = ts.map(t => t :: Separator).flatten |
63 def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten |
64 |
64 |
65 |
65 |
66 /* formatted output */ |
66 /* formatted output */ |
67 |
67 |
68 def standard_format(body: XML.Body): XML.Body = |
68 def standard_format(body: XML.Body): XML.Body = |