author | wenzelm |
Sat, 21 Jul 2012 22:13:50 +0200 | |
changeset 48421 | c4d337782de4 |
parent 48409 | 0d2114eb412a |
child 48743 | a72f8ffecf31 |
permissions | -rw-r--r-- |
31648 | 1 |
/* Title: Pure/General/scan.scala |
2 |
Author: Makarius |
|
3 |
||
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40290
diff
changeset
|
4 |
Efficient scanning of keywords and tokens. |
31648 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
34187
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
9 |
|
46627
fbe2cb05bdb3
avoid trait Addable, which is deprecated in scala-2.9.x;
wenzelm
parents:
45900
diff
changeset
|
10 |
import scala.collection.{IndexedSeq, TraversableOnce} |
34187
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
11 |
import scala.collection.immutable.PagedSeq |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
12 |
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader} |
31648 | 13 |
import scala.util.parsing.combinator.RegexParsers |
14 |
||
48409 | 15 |
import java.io.{File => JFile, BufferedInputStream, FileInputStream} |
34187
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
16 |
|
31648 | 17 |
|
18 |
object Scan |
|
19 |
{ |
|
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
20 |
/** context of partial scans **/ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
21 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
22 |
sealed abstract class Context |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
23 |
case object Finished extends Context |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
24 |
case class Quoted(quote: String) extends Context |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
25 |
case object Verbatim extends Context |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
26 |
case class Comment(depth: Int) extends Context |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
27 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
28 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
29 |
|
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
30 |
/** Lexicon -- position tree **/ |
31648 | 31 |
|
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
32 |
object Lexicon |
31648 | 33 |
{ |
45252 | 34 |
/* representation */ |
35 |
||
36 |
sealed case class Tree(val branches: Map[Char, (String, Tree)]) |
|
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
37 |
private val empty_tree = Tree(Map()) |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
38 |
|
45252 | 39 |
val empty: Lexicon = new Lexicon(empty_tree) |
31762
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
40 |
def apply(elems: String*): Lexicon = empty ++ elems |
31648 | 41 |
} |
42 |
||
46712 | 43 |
final class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers |
31648 | 44 |
{ |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
45 |
import Lexicon.Tree |
31648 | 46 |
|
47 |
||
31650 | 48 |
/* auxiliary operations */ |
49 |
||
50 |
private def content(tree: Tree, result: List[String]): List[String] = |
|
51 |
(result /: tree.branches.toList) ((res, entry) => |
|
52 |
entry match { case (_, (s, tr)) => |
|
53 |
if (s.isEmpty) content(tr, res) else content(tr, s :: res) }) |
|
54 |
||
55 |
private def lookup(str: CharSequence): Option[(Boolean, Tree)] = |
|
56 |
{ |
|
57 |
val len = str.length |
|
58 |
def look(tree: Tree, tip: Boolean, i: Int): Option[(Boolean, Tree)] = |
|
59 |
{ |
|
60 |
if (i < len) { |
|
61 |
tree.branches.get(str.charAt(i)) match { |
|
62 |
case Some((s, tr)) => look(tr, !s.isEmpty, i + 1) |
|
63 |
case None => None |
|
64 |
} |
|
65 |
} else Some(tip, tree) |
|
66 |
} |
|
67 |
look(main_tree, false, 0) |
|
68 |
} |
|
69 |
||
70 |
def completions(str: CharSequence): List[String] = |
|
31764 | 71 |
lookup(str) match { |
31650 | 72 |
case Some((true, tree)) => content(tree, List(str.toString)) |
73 |
case Some((false, tree)) => content(tree, Nil) |
|
74 |
case None => Nil |
|
31764 | 75 |
} |
31650 | 76 |
|
77 |
||
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset
|
78 |
/* pseudo Set methods */ |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
79 |
|
45900 | 80 |
def iterator: Iterator[String] = content(main_tree, Nil).sorted.iterator |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
81 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset
|
82 |
override def toString: String = iterator.mkString("Lexicon(", ", ", ")") |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
83 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset
|
84 |
def empty: Lexicon = Lexicon.empty |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset
|
85 |
def isEmpty: Boolean = main_tree.branches.isEmpty |
31648 | 86 |
|
31762
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
87 |
def contains(elem: String): Boolean = |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
88 |
lookup(elem) match { |
31650 | 89 |
case Some((tip, _)) => tip |
90 |
case _ => false |
|
91 |
} |
|
31648 | 92 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset
|
93 |
|
46627
fbe2cb05bdb3
avoid trait Addable, which is deprecated in scala-2.9.x;
wenzelm
parents:
45900
diff
changeset
|
94 |
/* add elements */ |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset
|
95 |
|
31762
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
96 |
def + (elem: String): Lexicon = |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
97 |
if (contains(elem)) this |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
98 |
else { |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
99 |
val len = elem.length |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
100 |
def extend(tree: Tree, i: Int): Tree = |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
101 |
if (i < len) { |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
102 |
val c = elem.charAt(i) |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
103 |
val end = (i + 1 == len) |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
104 |
tree.branches.get(c) match { |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
105 |
case Some((s, tr)) => |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
106 |
Tree(tree.branches + |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
107 |
(c -> (if (end) elem else s, extend(tr, i + 1)))) |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
108 |
case None => |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
109 |
Tree(tree.branches + |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
110 |
(c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1)))) |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
111 |
} |
34135 | 112 |
} |
113 |
else tree |
|
46627
fbe2cb05bdb3
avoid trait Addable, which is deprecated in scala-2.9.x;
wenzelm
parents:
45900
diff
changeset
|
114 |
new Lexicon(extend(main_tree, 0)) |
31648 | 115 |
} |
31762
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
116 |
|
46627
fbe2cb05bdb3
avoid trait Addable, which is deprecated in scala-2.9.x;
wenzelm
parents:
45900
diff
changeset
|
117 |
def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _) |
fbe2cb05bdb3
avoid trait Addable, which is deprecated in scala-2.9.x;
wenzelm
parents:
45900
diff
changeset
|
118 |
|
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
119 |
|
34301 | 120 |
|
34137 | 121 |
/** RegexParsers methods **/ |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
122 |
|
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
123 |
override val whiteSpace = "".r |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
124 |
|
34137 | 125 |
|
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
126 |
/* optional termination */ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
127 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
128 |
def opt_term[T](p: => Parser[T]): Parser[Option[T]] = |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
129 |
p ^^ (x => Some(x)) | """\z""".r ^^ (_ => None) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
130 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
131 |
|
34137 | 132 |
/* keywords from lexicon */ |
133 |
||
34140 | 134 |
def keyword: Parser[String] = new Parser[String] |
34135 | 135 |
{ |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
136 |
def apply(in: Input) = |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
137 |
{ |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
138 |
val source = in.source |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
139 |
val offset = in.offset |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
140 |
val len = source.length - offset |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
141 |
|
34140 | 142 |
def scan(tree: Tree, result: String, i: Int): String = |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
143 |
{ |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
144 |
if (i < len) { |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
145 |
tree.branches.get(source.charAt(offset + i)) match { |
34140 | 146 |
case Some((s, tr)) => scan(tr, if (s.isEmpty) result else s, i + 1) |
34135 | 147 |
case None => result |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
148 |
} |
34135 | 149 |
} |
150 |
else result |
|
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
151 |
} |
34140 | 152 |
val result = scan(main_tree, "", 0) |
153 |
if (result.isEmpty) Failure("keyword expected", in) |
|
154 |
else Success(result, in.drop(result.length)) |
|
31648 | 155 |
} |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
156 |
}.named("keyword") |
31648 | 157 |
|
34137 | 158 |
|
34157
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34144
diff
changeset
|
159 |
/* symbol range */ |
34137 | 160 |
|
43696 | 161 |
def symbol_range(pred: Symbol.Symbol => Boolean, min_count: Int, max_count: Int): Parser[String] = |
34140 | 162 |
new Parser[String] |
34135 | 163 |
{ |
34137 | 164 |
def apply(in: Input) = |
165 |
{ |
|
166 |
val start = in.offset |
|
167 |
val end = in.source.length |
|
168 |
val matcher = new Symbol.Matcher(in.source) |
|
169 |
||
170 |
var i = start |
|
171 |
var count = 0 |
|
172 |
var finished = false |
|
173 |
while (!finished) { |
|
174 |
if (i < end && count < max_count) { |
|
175 |
val n = matcher(i, end) |
|
176 |
val sym = in.source.subSequence(i, i + n).toString |
|
177 |
if (pred(sym)) { i += n; count += 1 } |
|
178 |
else finished = true |
|
179 |
} |
|
180 |
else finished = true |
|
181 |
} |
|
34140 | 182 |
if (count < min_count) Failure("bad input", in) |
183 |
else Success(in.source.subSequence(start, i).toString, in.drop(i - start)) |
|
34137 | 184 |
} |
34157
0a0a19153626
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
wenzelm
parents:
34144
diff
changeset
|
185 |
}.named("symbol_range") |
34137 | 186 |
|
43696 | 187 |
def one(pred: Symbol.Symbol => Boolean): Parser[String] = |
188 |
symbol_range(pred, 1, 1) |
|
189 |
||
190 |
def many(pred: Symbol.Symbol => Boolean): Parser[String] = |
|
191 |
symbol_range(pred, 0, Integer.MAX_VALUE) |
|
192 |
||
193 |
def many1(pred: Symbol.Symbol => Boolean): Parser[String] = |
|
194 |
symbol_range(pred, 1, Integer.MAX_VALUE) |
|
34140 | 195 |
|
196 |
||
34143 | 197 |
/* quoted strings */ |
34140 | 198 |
|
43696 | 199 |
private def quoted_body(quote: Symbol.Symbol): Parser[String] = |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
200 |
{ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
201 |
rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" | |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
202 |
(("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
203 |
} |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
204 |
|
43696 | 205 |
private def quoted(quote: Symbol.Symbol): Parser[String] = |
34143 | 206 |
{ |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
207 |
quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z } |
34143 | 208 |
}.named("quoted") |
34140 | 209 |
|
43696 | 210 |
def quoted_content(quote: Symbol.Symbol, source: String): String = |
34140 | 211 |
{ |
212 |
require(parseAll(quoted(quote), source).successful) |
|
34189 | 213 |
val body = source.substring(1, source.length - 1) |
214 |
if (body.exists(_ == '\\')) { |
|
215 |
val content = |
|
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40290
diff
changeset
|
216 |
rep(many1(sym => sym != quote && sym != "\\") | |
34189 | 217 |
"\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString })) |
218 |
parseAll(content ^^ (_.mkString), body).get |
|
219 |
} |
|
220 |
else body |
|
34140 | 221 |
} |
222 |
||
43696 | 223 |
def quoted_context(quote: Symbol.Symbol, ctxt: Context): Parser[(String, Context)] = |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
224 |
{ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
225 |
ctxt match { |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
226 |
case Finished => |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
227 |
quote ~ quoted_body(quote) ~ opt_term(quote) ^^ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
228 |
{ case x ~ y ~ Some(z) => (x + y + z, Finished) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
229 |
case x ~ y ~ None => (x + y, Quoted(quote)) } |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
230 |
case Quoted(q) if q == quote => |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
231 |
quoted_body(quote) ~ opt_term(quote) ^^ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
232 |
{ case x ~ Some(y) => (x + y, Finished) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
233 |
case x ~ None => (x, ctxt) } |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
234 |
case _ => failure("") |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
235 |
} |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
236 |
}.named("quoted_context") |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
237 |
|
34140 | 238 |
|
34143 | 239 |
/* verbatim text */ |
240 |
||
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
241 |
private def verbatim_body: Parser[String] = |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
242 |
rep(many1(sym => sym != "*") | """\*(?!\})""".r) ^^ (_.mkString) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
243 |
|
34143 | 244 |
private def verbatim: Parser[String] = |
245 |
{ |
|
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
246 |
"{*" ~ verbatim_body ~ "*}" ^^ { case x ~ y ~ z => x + y + z } |
34143 | 247 |
}.named("verbatim") |
34140 | 248 |
|
249 |
def verbatim_content(source: String): String = |
|
250 |
{ |
|
251 |
require(parseAll(verbatim, source).successful) |
|
252 |
source.substring(2, source.length - 2) |
|
253 |
} |
|
254 |
||
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
255 |
def verbatim_context(ctxt: Context): Parser[(String, Context)] = |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
256 |
{ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
257 |
ctxt match { |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
258 |
case Finished => |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
259 |
"{*" ~ verbatim_body ~ opt_term("*}") ^^ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
260 |
{ case x ~ y ~ Some(z) => (x + y + z, Finished) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
261 |
case x ~ y ~ None => (x + y, Verbatim) } |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
262 |
case Verbatim => |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
263 |
verbatim_body ~ opt_term("*}") ^^ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
264 |
{ case x ~ Some(y) => (x + y, Finished) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
265 |
case x ~ None => (x, Verbatim) } |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
266 |
case _ => failure("") |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
267 |
} |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
268 |
}.named("verbatim_context") |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
269 |
|
34140 | 270 |
|
34143 | 271 |
/* nested comments */ |
272 |
||
43412 | 273 |
private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)] |
34143 | 274 |
{ |
43412 | 275 |
require(depth >= 0) |
276 |
||
34143 | 277 |
val comment_text = |
42441
781c622af16a
more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents:
40523
diff
changeset
|
278 |
rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r) |
34143 | 279 |
|
280 |
def apply(in: Input) = |
|
281 |
{ |
|
282 |
var rest = in |
|
42441
781c622af16a
more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents:
40523
diff
changeset
|
283 |
def try_parse[A](p: Parser[A]): Boolean = |
34143 | 284 |
{ |
42441
781c622af16a
more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents:
40523
diff
changeset
|
285 |
parse(p ^^^ (), rest) match { |
34143 | 286 |
case Success(_, next) => { rest = next; true } |
287 |
case _ => false |
|
288 |
} |
|
289 |
} |
|
43412 | 290 |
var d = depth |
34143 | 291 |
var finished = false |
292 |
while (!finished) { |
|
43412 | 293 |
if (try_parse("(*")) d += 1 |
294 |
else if (d > 0 && try_parse("*)")) d -= 1 |
|
295 |
else if (d == 0 || !try_parse(comment_text)) finished = true |
|
34143 | 296 |
} |
43412 | 297 |
if (in.offset < rest.offset) |
298 |
Success((in.source.subSequence(in.offset, rest.offset).toString, d), rest) |
|
34143 | 299 |
else Failure("comment expected", in) |
300 |
} |
|
43412 | 301 |
}.named("comment_depth") |
302 |
||
303 |
def comment: Parser[String] = |
|
304 |
comment_depth(0) ^? { case (x, d) if d == 0 => x } |
|
305 |
||
306 |
def comment_context(ctxt: Context): Parser[(String, Context)] = |
|
307 |
{ |
|
308 |
val depth = |
|
309 |
ctxt match { |
|
310 |
case Finished => 0 |
|
311 |
case Comment(d) => d |
|
312 |
case _ => -1 |
|
313 |
} |
|
314 |
if (depth >= 0) |
|
315 |
comment_depth(depth) ^^ |
|
316 |
{ case (x, 0) => (x, Finished) |
|
317 |
case (x, d) => (x, Comment(d)) } |
|
318 |
else failure("") |
|
319 |
} |
|
34143 | 320 |
|
321 |
def comment_content(source: String): String = |
|
322 |
{ |
|
323 |
require(parseAll(comment, source).successful) |
|
324 |
source.substring(2, source.length - 2) |
|
325 |
} |
|
326 |
||
327 |
||
34140 | 328 |
/* outer syntax tokens */ |
329 |
||
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
330 |
private def delimited_token: Parser[Token] = |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
331 |
{ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
332 |
val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x)) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
333 |
val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x)) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
334 |
val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x)) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
335 |
val cmt = comment ^^ (x => Token(Token.Kind.COMMENT, x)) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
336 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
337 |
string | (alt_string | (verb | cmt)) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
338 |
} |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
339 |
|
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
340 |
private def other_token(is_command: String => Boolean) |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
341 |
: Parser[Token] = |
34140 | 342 |
{ |
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
343 |
val id = one(Symbol.is_letter) ~ many(Symbol.is_letdig) ^^ { case x ~ y => x + y } |
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
344 |
val nat = many1(Symbol.is_digit) |
40290
47f572aff50a
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38367
diff
changeset
|
345 |
val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z } |
34140 | 346 |
val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x } |
347 |
||
348 |
val ident = id ~ rep("." ~> id) ^^ |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset
|
349 |
{ case x ~ Nil => Token(Token.Kind.IDENT, x) |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset
|
350 |
case x ~ ys => Token(Token.Kind.LONG_IDENT, (x :: ys).mkString(".")) } |
34140 | 351 |
|
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset
|
352 |
val var_ = "?" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.VAR, x + y) } |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset
|
353 |
val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token.Kind.TYPE_IDENT, x + y) } |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset
|
354 |
val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.TYPE_VAR, x + y) } |
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset
|
355 |
val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x)) |
40290
47f572aff50a
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38367
diff
changeset
|
356 |
val float = |
47f572aff50a
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38367
diff
changeset
|
357 |
("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x)) |
34140 | 358 |
|
359 |
val sym_ident = |
|
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
360 |
(many1(Symbol.is_symbolic_char) | one(sym => Symbol.is_symbolic(sym))) ^^ |
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset
|
361 |
(x => Token(Token.Kind.SYM_IDENT, x)) |
34140 | 362 |
|
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
363 |
val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x)) |
34140 | 364 |
|
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
365 |
// FIXME check |
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
366 |
val junk = many(sym => !(Symbol.is_blank(sym))) |
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
367 |
val junk1 = many1(sym => !(Symbol.is_blank(sym))) |
34140 | 368 |
|
34267 | 369 |
val bad_delimiter = |
38367 | 370 |
("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.UNPARSED, x + y) } |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
371 |
val bad = junk1 ^^ (x => Token(Token.Kind.UNPARSED, x)) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
372 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
373 |
val command_keyword = |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
374 |
keyword ^^ (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x)) |
34140 | 375 |
|
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
376 |
space | (bad_delimiter | |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
377 |
(((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) ||| |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
378 |
command_keyword) | bad)) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
379 |
} |
34140 | 380 |
|
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
381 |
def token(is_command: String => Boolean): Parser[Token] = |
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
382 |
delimited_token | other_token(is_command) |
34140 | 383 |
|
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
384 |
def token_context(is_command: String => Boolean, ctxt: Context): Parser[(Token, Context)] = |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
385 |
{ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
386 |
val string = |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
387 |
quoted_context("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) } |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
388 |
val alt_string = |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
389 |
quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) } |
43412 | 390 |
val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) } |
391 |
val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) } |
|
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43420
diff
changeset
|
392 |
val other = other_token(is_command) ^^ { case x => (x, Finished) } |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
393 |
|
43412 | 394 |
string | (alt_string | (verb | (cmt | other))) |
34140 | 395 |
} |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
396 |
} |
34187
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
397 |
|
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
398 |
|
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
399 |
|
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
400 |
/** read file without decoding -- enables efficient length operation **/ |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
401 |
|
36679
ac021aed685e
use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;
wenzelm
parents:
36012
diff
changeset
|
402 |
private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int) |
34187
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
403 |
extends CharSequence |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
404 |
{ |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
405 |
def charAt(i: Int): Char = |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
406 |
if (0 <= i && i < length) seq(start + i) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
407 |
else throw new IndexOutOfBoundsException |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
408 |
|
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
409 |
def length: Int = end - start // avoid potentially expensive seq.length |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
410 |
|
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
411 |
def subSequence(i: Int, j: Int): CharSequence = |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
412 |
if (0 <= i && i <= j && j <= length) new Restricted_Seq(seq, start + i, start + j) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
413 |
else throw new IndexOutOfBoundsException |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
414 |
|
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
415 |
override def toString: String = |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
416 |
{ |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
417 |
val buf = new StringBuilder(length) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
418 |
for (offset <- start until end) buf.append(seq(offset)) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
419 |
buf.toString |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
420 |
} |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
421 |
} |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
422 |
|
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
423 |
abstract class Byte_Reader extends Reader[Char] { def close: Unit } |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
424 |
|
48409 | 425 |
def byte_reader(file: JFile): Byte_Reader = |
34187
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
426 |
{ |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
427 |
val stream = new BufferedInputStream(new FileInputStream(file)) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
428 |
val seq = new PagedSeq( |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
429 |
(buf: Array[Char], offset: Int, length: Int) => |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
430 |
{ |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
431 |
var i = 0 |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
432 |
var c = 0 |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
433 |
var eof = false |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
434 |
while (!eof && i < length) { |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
435 |
c = stream.read |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
436 |
if (c == -1) eof = true |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
437 |
else { buf(offset + i) = c.toChar; i += 1 } |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
438 |
} |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
439 |
if (i > 0) i else -1 |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
440 |
}) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
441 |
val restricted_seq = new Restricted_Seq(seq, 0, file.length.toInt) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
442 |
|
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
443 |
class Paged_Reader(override val offset: Int) extends Byte_Reader |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
444 |
{ |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
445 |
override lazy val source: CharSequence = restricted_seq |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
446 |
def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\032' |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
447 |
def rest: Paged_Reader = if (seq.isDefinedAt(offset)) new Paged_Reader(offset + 1) else this |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
448 |
def pos: InputPosition = new OffsetPosition(source, offset) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
449 |
def atEnd: Boolean = !seq.isDefinedAt(offset) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
450 |
override def drop(n: Int): Paged_Reader = new Paged_Reader(offset + n) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
451 |
def close { stream.close } |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
452 |
} |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
453 |
new Paged_Reader(0) |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
454 |
} |
31648 | 455 |
} |