src/Pure/PIDE/protocol_command.ML
changeset 78733 70e1c0167ae2
parent 78725 3c02ad5a1586
child 78757 a094bf81a496
equal deleted inserted replaced
78732:fc179b4423b4 78733:70e1c0167ae2