changeset 74789 | a5c23da73fca |
parent 74785 | 4671d29feb00 |
child 75393 | 87ebf5a50283 |
--- a/src/Pure/PIDE/xml.scala Sun Nov 14 21:52:13 2021 +0100 +++ b/src/Pure/PIDE/xml.scala Mon Nov 15 11:38:14 2021 +0100 @@ -46,6 +46,9 @@ def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s)) + def enclose(bg: String, en:String, body: Body): Body = + string(bg) ::: body ::: string(en) + /* name space */