src/Pure/PIDE/xml.scala
changeset 74789 a5c23da73fca
parent 74785 4671d29feb00
child 75393 87ebf5a50283
equal deleted inserted replaced
74788:95e514137861 74789:a5c23da73fca
    43 
    43 
    44   val no_text: Text = Text("")
    44   val no_text: Text = Text("")
    45   val newline: Text = Text("\n")
    45   val newline: Text = Text("\n")
    46 
    46 
    47   def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s))
    47   def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s))
       
    48 
       
    49   def enclose(bg: String, en:String, body: Body): Body =
       
    50     string(bg) ::: body ::: string(en)
    48 
    51 
    49 
    52 
    50   /* name space */
    53   /* name space */
    51 
    54 
    52   object Namespace
    55   object Namespace