317 local |
317 local |
318 |
318 |
319 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2; |
319 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2; |
320 |
320 |
321 fun token k ss = |
321 fun token k ss = |
322 Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot); |
322 Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); |
323 |
323 |
324 fun token_range k (pos1, (ss, pos2)) = |
324 fun token_range k (pos1, (ss, pos2)) = |
325 Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot); |
325 Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot); |
326 |
326 |
327 fun scan (lex1, lex2) = !!! "bad input" |
327 fun scan (lex1, lex2) = !!! "bad input" |
328 (Symbol_Pos.scan_string_qq >> token_range String || |
328 (Symbol_Pos.scan_string_qq >> token_range String || |
329 Symbol_Pos.scan_string_bq >> token_range AltString || |
329 Symbol_Pos.scan_string_bq >> token_range AltString || |
330 scan_verbatim >> token_range Verbatim || |
330 scan_verbatim >> token_range Verbatim || |