src/Pure/PIDE/protocol.ML
changeset 52516 b5b3c888df9f
parent 52111 1fd184eaa310
child 52527 dbac84eab3bc