src/Pure/PIDE/command_span.ML
changeset 57915 448325de6e4f
parent 57905 c0c5652e796e
child 58923 cb9b69cca999