changeset 47121 | fb5764df8a9c |
parent 46997 | 395b7277ed76 |
child 47993 | 135fd6f2dadd |
47120:500a5d97511a | 47121:fb5764df8a9c |
---|---|
345 "\\<Psi>", "\\<Omega>", |
345 "\\<Psi>", "\\<Omega>", |
346 |
346 |
347 "\\<^isub>", "\\<^isup>") |
347 "\\<^isub>", "\\<^isup>") |
348 |
348 |
349 val blanks = |
349 val blanks = |
350 recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>") |
350 recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>") |
351 |
351 |
352 val sym_chars = |
352 val sym_chars = |
353 Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~") |
353 Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~") |
354 |
354 |
355 val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*) |
355 val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*) |