src/Pure/PIDE/document_info.scala
changeset 76371 1ac2416e8432
parent 75972 d574b55c4e83
child 76656 a8f452f7c503
equal deleted inserted replaced
76370:9bd948666e8a 76371:1ac2416e8432