src/Pure/General/yxml.scala
changeset 38230 ed147003de4b
parent 36685 2b3076cfd6dd
child 38231 968844caaff9
equal deleted inserted replaced
38229:61d0fe8b96ac 38230:ed147003de4b
    62   def parse_body(source: CharSequence): List[XML.Tree] =
    62   def parse_body(source: CharSequence): List[XML.Tree] =
    63   {
    63   {
    64     /* stack operations */
    64     /* stack operations */
    65 
    65 
    66     def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
    66     def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
    67     var stack: List[((String, XML.Attributes), ListBuffer[XML.Tree])] = List((("", Nil), buffer()))
    67     var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup("", Nil), buffer()))
    68 
    68 
    69     def add(x: XML.Tree)
    69     def add(x: XML.Tree)
    70     {
    70     {
    71       (stack: @unchecked) match { case ((_, body) :: _) => body += x }
    71       (stack: @unchecked) match { case ((_, body) :: _) => body += x }
    72     }
    72     }
    73 
    73 
    74     def push(name: String, atts: XML.Attributes)
    74     def push(name: String, atts: XML.Attributes)
    75     {
    75     {
    76       if (name == "") err_element()
    76       if (name == "") err_element()
    77       else stack = ((name, atts), buffer()) :: stack
    77       else stack = (Markup(name, atts), buffer()) :: stack
    78     }
    78     }
    79 
    79 
    80     def pop()
    80     def pop()
    81     {
    81     {
    82       (stack: @unchecked) match {
    82       (stack: @unchecked) match {
    83         case ((("", _), _) :: _) => err_unbalanced("")
    83         case ((Markup("", _), _) :: _) => err_unbalanced("")
    84         case (((name, atts), body) :: pending) =>
    84         case ((markup, body) :: pending) =>
    85           stack = pending; add(XML.Elem(name, atts, body.toList))
    85           stack = pending
       
    86           add(XML.Elem(markup, body.toList))
    86       }
    87       }
    87     }
    88     }
    88 
    89 
    89 
    90 
    90     /* parse chunks */
    91     /* parse chunks */
    98           case txts => for (txt <- txts) add(XML.Text(txt.toString))
    99           case txts => for (txt <- txts) add(XML.Text(txt.toString))
    99         }
   100         }
   100       }
   101       }
   101     }
   102     }
   102     stack match {
   103     stack match {
   103       case List((("", _), body)) => body.toList
   104       case List((Markup("", _), body)) => body.toList
   104       case ((name, _), _) :: _ => err_unbalanced(name)
   105       case (Markup(name, _), _) :: _ => err_unbalanced(name)
   105     }
   106     }
   106   }
   107   }
   107 
   108 
   108   def parse(source: CharSequence): XML.Tree =
   109   def parse(source: CharSequence): XML.Tree =
   109     parse_body(source) match {
   110     parse_body(source) match {
   114 
   115 
   115 
   116 
   116   /* failsafe parsing */
   117   /* failsafe parsing */
   117 
   118 
   118   private def markup_failsafe(source: CharSequence) =
   119   private def markup_failsafe(source: CharSequence) =
   119     XML.Elem (Markup.MALFORMED, Nil,
   120     XML.Elem (Markup(Markup.MALFORMED, Nil),
   120       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
   121       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
   121 
   122 
   122   def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
   123   def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
   123   {
   124   {
   124     try { parse_body(source) }
   125     try { parse_body(source) }