src/Pure/PIDE/command_span.ML
changeset 58646 cd63a4b12a33
parent 57905 c0c5652e796e
child 58923 cb9b69cca999