equal
deleted
inserted
replaced
515 (* read embedded source, e.g. for antiquotations *) |
515 (* read embedded source, e.g. for antiquotations *) |
516 |
516 |
517 fun tokenize keywords = Token.tokenize keywords {strict = true} #> filter Token.is_proper; |
517 fun tokenize keywords = Token.tokenize keywords {strict = true} #> filter Token.is_proper; |
518 |
518 |
519 fun read_antiq keywords scan (syms, pos) = |
519 fun read_antiq keywords scan (syms, pos) = |
520 (case Scan.read Token.stopper scan (tokenize (Keyword.no_command_keywords keywords) syms) of |
520 (case Scan.read Token.stopper scan (tokenize (Keyword.no_major_keywords keywords) syms) of |
521 SOME res => res |
521 SOME res => res |
522 | NONE => error ("Malformed antiquotation" ^ Position.here pos)); |
522 | NONE => error ("Malformed antiquotation" ^ Position.here pos)); |
523 |
523 |
524 fun read_embedded ctxt keywords parse input = |
524 fun read_embedded ctxt keywords parse input = |
525 let |
525 let |