src/Pure/PIDE/text.scala
changeset 45470 81b85d4ed269
parent 45455 4f974c0c5c2f
child 45631 6bdf8b926f50
     1.1 --- a/src/Pure/PIDE/text.scala	Sat Nov 12 17:01:58 2011 +0100
     1.2 +++ b/src/Pure/PIDE/text.scala	Sat Nov 12 17:52:28 2011 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4        catch { case ERROR(_) => None }
     1.5    }
     1.6  
     1.7 -  type Markup = Info[XML.Tree]
     1.8 +  type Markup = Info[XML.Elem]
     1.9  
    1.10  
    1.11    /* editing */