equal
deleted
inserted
replaced
29 |
29 |
30 |
30 |
31 /* Symbol regexps */ |
31 /* Symbol regexps */ |
32 |
32 |
33 private val plain = new Regex("""(?xs) |
33 private val plain = new Regex("""(?xs) |
34 [^\r\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """) |
34 [^\r\\\ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """) |
35 |
35 |
36 private val newline = new Regex("""(?xs) \r\n | \r """) |
36 private val physical_newline = new Regex("""(?xs) \n | \r\n | \r """) |
37 |
37 |
38 private val symbol = new Regex("""(?xs) |
38 private val symbol = new Regex("""(?xs) |
39 \\ < (?: |
39 \\ < (?: |
40 \^? [A-Za-z][A-Za-z0-9_']* | |
40 \^? [A-Za-z][A-Za-z0-9_']* | |
41 \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""") |
41 \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""") |
44 // FIXME check wrt. Isabelle/ML version |
44 // FIXME check wrt. Isabelle/ML version |
45 private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" + |
45 private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" + |
46 """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""") |
46 """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""") |
47 |
47 |
48 // total pattern |
48 // total pattern |
49 val regex = new Regex(plain + "|" + newline + "|" + symbol + "|" + bad_symbol + "| .") |
49 val regex = new Regex(plain + "|" + physical_newline + "|" + symbol + "|" + bad_symbol + "| .") |
50 |
50 |
51 |
51 |
52 /* basic matching */ |
52 /* basic matching */ |
53 |
53 |
54 def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff') |
54 def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff') |
79 def iterator(text: CharSequence) = new Iterator[CharSequence] |
79 def iterator(text: CharSequence) = new Iterator[CharSequence] |
80 { |
80 { |
81 private val matcher = new Matcher(text) |
81 private val matcher = new Matcher(text) |
82 private var i = 0 |
82 private var i = 0 |
83 def hasNext = i < text.length |
83 def hasNext = i < text.length |
84 def next = { |
84 def next = |
|
85 { |
85 val n = matcher(i, text.length) |
86 val n = matcher(i, text.length) |
86 val s = text.subSequence(i, i + n) |
87 val s = text.subSequence(i, i + n) |
87 i += n |
88 i += n |
88 s |
89 s |
89 } |
90 } |