src/Pure/PIDE/command_span.ML
changeset 82809 b908d50f42d4
parent 82679 1dd29afaddda
child 82931 fa8067dc6787