src/Pure/PIDE/execution.ML
changeset 60610 f52b4b0c10c4
parent 59467 58c4f3e1870f
child 61077 06cca32aa519
equal deleted inserted replaced
60609:15620ae824c0 60610:f52b4b0c10c4