src/Pure/PIDE/protocol.ML
changeset 69650 c95edf19133b
parent 68381 2fd3a6d6ba2e
child 69845 d28e8199dcb9