src/Pure/PIDE/xml.scala
changeset 65991 fa787e233214
parent 65990 868089ee9d60
child 66196 31c9b09cc1d4
equal deleted inserted replaced
65990:868089ee9d60 65991:fa787e233214
   114   def string_of_body(body: Body): String =
   114   def string_of_body(body: Body): String =
   115   {
   115   {
   116     val s = new StringBuilder
   116     val s = new StringBuilder
   117 
   117 
   118     def text(txt: String) { output_string(txt, s) }
   118     def text(txt: String) { output_string(txt, s) }
   119     def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
   119     def elem(markup: Markup)
   120     def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
   120     {
       
   121       s ++= markup.name
       
   122       for ((a, b) <- markup.properties) {
       
   123         s += ' '; s ++= a; s += '='; s += '"'; text(b); s += '"'
       
   124       }
       
   125     }
   121     def tree(t: Tree): Unit =
   126     def tree(t: Tree): Unit =
   122       t match {
   127       t match {
   123         case XML.Elem(markup, Nil) =>
   128         case XML.Elem(markup, Nil) =>
   124           s ++= "<"; elem(markup); s ++= "/>"
   129           s += '<'; elem(markup); s ++= "/>"
   125         case XML.Elem(markup, ts) =>
   130         case XML.Elem(markup, ts) =>
   126           s ++= "<"; elem(markup); s ++= ">"
   131           s += '<'; elem(markup); s += '>'
   127           ts.foreach(tree)
   132           ts.foreach(tree)
   128           s ++= "</"; s ++= markup.name; s ++= ">"
   133           s ++= "</"; s ++= markup.name; s += '>'
   129         case XML.Text(txt) => text(txt)
   134         case XML.Text(txt) => text(txt)
   130       }
   135       }
   131     body.foreach(tree)
   136     body.foreach(tree)
   132     s.toString
   137     s.toString
   133   }
   138   }