src/Pure/PIDE/command_span.ML
changeset 74422 5294a44efc49
parent 72754 1456c5747416
child 82679 1dd29afaddda
equal deleted inserted replaced
74420:b618749bb8f4 74422:5294a44efc49