src/Pure/PIDE/document.scala
changeset 52895 a806aa7a5370
parent 52889 ea3338812e67
child 52900 d29bf6db8a2d
equal deleted inserted replaced
52894:cebaf814ca6e 52895:a806aa7a5370