src/Pure/PIDE/command_span.ML
changeset 58605 9d5013661ac6
parent 57905 c0c5652e796e
child 58923 cb9b69cca999