equal
deleted
inserted
replaced
540 |
540 |
541 fun token k ss = |
541 fun token k ss = |
542 Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); |
542 Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); |
543 |
543 |
544 fun token_range k (pos1, (ss, pos2)) = |
544 fun token_range k (pos1, (ss, pos2)) = |
545 Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot); |
545 Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot); |
546 |
546 |
547 fun scan_token keywords = !!! "bad input" |
547 fun scan_token keywords = !!! "bad input" |
548 (Symbol_Pos.scan_string_qq err_prefix >> token_range String || |
548 (Symbol_Pos.scan_string_qq err_prefix >> token_range String || |
549 Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String || |
549 Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String || |
550 scan_verbatim >> token_range Verbatim || |
550 scan_verbatim >> token_range Verbatim || |