author  wenzelm 
Thu, 16 Jun 2011 18:00:56 +0200  
changeset 43412  81517eed8a78 
parent 43411  0206466ee473 
child 43420  a26e514c92b2 
permissions  rwrr 
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 

36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

10 
import scala.collection.generic.Addable 
36679
ac021aed685e
use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;
wenzelm
parents:
36012
diff
changeset

11 
import scala.collection.IndexedSeq 
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

12 
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

13 
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader} 
31648  14 
import scala.util.parsing.combinator.RegexParsers 
15 

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 
import java.io.{File, InputStream, BufferedInputStream, FileInputStream} 
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset

17 

31648  18 

19 
object Scan 

20 
{ 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

21 
/** context of partial scans **/ 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

22 

0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

23 
sealed abstract class Context 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

24 
case object Finished extends Context 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

25 
case class Quoted(quote: String) extends Context 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

26 
case object Verbatim extends Context 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

27 
case class Comment(depth: Int) extends Context 
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 

0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

30 

31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

31 
/** Lexicon  position tree **/ 
31648  32 

31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

33 
object Lexicon 
31648  34 
{ 
42718  35 
protected case class Tree(val branches: Map[Char, (String, Tree)]) 
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

36 
private val empty_tree = Tree(Map()) 
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

37 

a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

38 
val empty: Lexicon = new Lexicon 
31762
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

39 
def apply(elems: String*): Lexicon = empty ++ elems 
31648  40 
} 
41 

36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

42 
class Lexicon extends Addable[String, Lexicon] with RegexParsers 
31648  43 
{ 
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

44 
/* representation */ 
31648  45 

31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

46 
import Lexicon.Tree 
31764  47 
protected val main_tree: Tree = Lexicon.empty_tree 
31648  48 

49 

31650  50 
/* auxiliary operations */ 
51 

52 
private def content(tree: Tree, result: List[String]): List[String] = 

53 
(result /: tree.branches.toList) ((res, entry) => 

54 
entry match { case (_, (s, tr)) => 

55 
if (s.isEmpty) content(tr, res) else content(tr, s :: res) }) 

56 

57 
private def lookup(str: CharSequence): Option[(Boolean, Tree)] = 

58 
{ 

59 
val len = str.length 

60 
def look(tree: Tree, tip: Boolean, i: Int): Option[(Boolean, Tree)] = 

61 
{ 

62 
if (i < len) { 

63 
tree.branches.get(str.charAt(i)) match { 

64 
case Some((s, tr)) => look(tr, !s.isEmpty, i + 1) 

65 
case None => None 

66 
} 

67 
} else Some(tip, tree) 

68 
} 

69 
look(main_tree, false, 0) 

70 
} 

71 

72 
def completions(str: CharSequence): List[String] = 

31764  73 
lookup(str) match { 
31650  74 
case Some((true, tree)) => content(tree, List(str.toString)) 
75 
case Some((false, tree)) => content(tree, Nil) 

76 
case None => Nil 

31764  77 
} 
31650  78 

79 

36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

80 
/* pseudo Set methods */ 
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

81 

36012  82 
def iterator: Iterator[String] = content(main_tree, Nil).sortWith(_ <= _).iterator 
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 
override def toString: String = iterator.mkString("Lexicon(", ", ", ")") 
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

85 

36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

86 
def empty: Lexicon = Lexicon.empty 
3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

87 
def isEmpty: Boolean = main_tree.branches.isEmpty 
31648  88 

31762
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

89 
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

90 
lookup(elem) match { 
31650  91 
case Some((tip, _)) => tip 
92 
case _ => false 

93 
} 

31648  94 

36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

95 

3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

96 
/* Addable methods */ 
3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

97 

3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

98 
def repr = this 
3ff725ac13a4
adapted to Scala 2.8.0 Beta1  with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset

99 

31762
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

100 
def + (elem: String): Lexicon = 
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

101 
if (contains(elem)) this 
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

102 
else { 
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

103 
val len = elem.length 
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

104 
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

105 
if (i < len) { 
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

106 
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

107 
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

108 
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

109 
case Some((s, tr)) => 
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

110 
Tree(tree.branches + 
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

111 
(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

112 
case None => 
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

113 
Tree(tree.branches + 
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

114 
(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

115 
} 
34135  116 
} 
117 
else tree 

31762
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

118 
val old = this 
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

119 
new Lexicon { override val main_tree = extend(old.main_tree, 0) } 
31648  120 
} 
31762
20745ab5b79a
more precise implementation of trait methods  oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset

121 

31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

122 

34301  123 

34137  124 
/** RegexParsers methods **/ 
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

125 

a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

126 
override val whiteSpace = "".r 
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

127 

34137  128 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

129 
/* optional termination */ 
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 
def opt_term[T](p: => Parser[T]): Parser[Option[T]] = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

132 
p ^^ (x => Some(x))  """\z""".r ^^ (_ => None) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

133 

0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

134 

34137  135 
/* keywords from lexicon */ 
136 

34140  137 
def keyword: Parser[String] = new Parser[String] 
34135  138 
{ 
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

139 
def apply(in: Input) = 
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

140 
{ 
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

141 
val source = in.source 
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

142 
val offset = in.offset 
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

143 
val len = source.length  offset 
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

144 

34140  145 
def scan(tree: Tree, result: String, i: Int): String = 
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

146 
{ 
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

147 
if (i < len) { 
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

148 
tree.branches.get(source.charAt(offset + i)) match { 
34140  149 
case Some((s, tr)) => scan(tr, if (s.isEmpty) result else s, i + 1) 
34135  150 
case None => result 
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

151 
} 
34135  152 
} 
153 
else result 

31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

154 
} 
34140  155 
val result = scan(main_tree, "", 0) 
156 
if (result.isEmpty) Failure("keyword expected", in) 

157 
else Success(result, in.drop(result.length)) 

31648  158 
} 
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

159 
}.named("keyword") 
31648  160 

34137  161 

34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34144
diff
changeset

162 
/* symbol range */ 
34137  163 

34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34144
diff
changeset

164 
def symbol_range(pred: String => Boolean, min_count: Int, max_count: Int): Parser[String] = 
34140  165 
new Parser[String] 
34135  166 
{ 
34137  167 
def apply(in: Input) = 
168 
{ 

169 
val start = in.offset 

170 
val end = in.source.length 

171 
val matcher = new Symbol.Matcher(in.source) 

172 

173 
var i = start 

174 
var count = 0 

175 
var finished = false 

176 
while (!finished) { 

177 
if (i < end && count < max_count) { 

178 
val n = matcher(i, end) 

179 
val sym = in.source.subSequence(i, i + n).toString 

180 
if (pred(sym)) { i += n; count += 1 } 

181 
else finished = true 

182 
} 

183 
else finished = true 

184 
} 

34140  185 
if (count < min_count) Failure("bad input", in) 
186 
else Success(in.source.subSequence(start, i).toString, in.drop(i  start)) 

34137  187 
} 
34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34144
diff
changeset

188 
}.named("symbol_range") 
34137  189 

34157
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34144
diff
changeset

190 
def one(pred: String => Boolean): Parser[String] = symbol_range(pred, 1, 1) 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34144
diff
changeset

191 
def many(pred: String => Boolean): Parser[String] = symbol_range(pred, 0, Integer.MAX_VALUE) 
0a0a19153626
explicit representation of Token_Kind  cannot really depend on runtime types due to erasure;
wenzelm
parents:
34144
diff
changeset

192 
def many1(pred: String => Boolean): Parser[String] = symbol_range(pred, 1, Integer.MAX_VALUE) 
34140  193 

194 

34143  195 
/* quoted strings */ 
34140  196 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

197 
private def quoted_body(quote: String): Parser[String] = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

198 
{ 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

199 
rep(many1(sym => sym != quote && sym != "\\")  "\\" + quote  "\\\\"  
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

200 
(("""\\\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

201 
} 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

202 

34143  203 
private def quoted(quote: String): Parser[String] = 
204 
{ 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

205 
quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z } 
34143  206 
}.named("quoted") 
34140  207 

208 
def quoted_content(quote: String, source: String): String = 

209 
{ 

210 
require(parseAll(quoted(quote), source).successful) 

34189  211 
val body = source.substring(1, source.length  1) 
212 
if (body.exists(_ == '\\')) { 

213 
val content = 

40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40290
diff
changeset

214 
rep(many1(sym => sym != quote && sym != "\\")  
34189  215 
"\\" ~> (quote  "\\"  """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString })) 
216 
parseAll(content ^^ (_.mkString), body).get 

217 
} 

218 
else body 

34140  219 
} 
220 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

221 
def quoted_context(quote: String, ctxt: Context): Parser[(String, Context)] = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

222 
{ 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

223 
ctxt match { 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

224 
case Finished => 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

225 
quote ~ quoted_body(quote) ~ opt_term(quote) ^^ 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

226 
{ case x ~ y ~ Some(z) => (x + y + z, Finished) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

227 
case x ~ y ~ None => (x + y, Quoted(quote)) } 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

228 
case Quoted(q) if q == quote => 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

229 
quoted_body(quote) ~ opt_term(quote) ^^ 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

230 
{ case x ~ Some(y) => (x + y, Finished) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

231 
case x ~ None => (x, ctxt) } 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

232 
case _ => failure("") 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

233 
} 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

234 
}.named("quoted_context") 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

235 

34140  236 

34143  237 
/* verbatim text */ 
238 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

239 
private def verbatim_body: Parser[String] = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

240 
rep(many1(sym => sym != "*")  """\*(?!\})""".r) ^^ (_.mkString) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

241 

34143  242 
private def verbatim: Parser[String] = 
243 
{ 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

244 
"{*" ~ verbatim_body ~ "*}" ^^ { case x ~ y ~ z => x + y + z } 
34143  245 
}.named("verbatim") 
34140  246 

247 
def verbatim_content(source: String): String = 

248 
{ 

249 
require(parseAll(verbatim, source).successful) 

250 
source.substring(2, source.length  2) 

251 
} 

252 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

253 
def verbatim_context(ctxt: Context): Parser[(String, Context)] = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

254 
{ 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

255 
ctxt match { 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

256 
case Finished => 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

257 
"{*" ~ verbatim_body ~ opt_term("*}") ^^ 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

258 
{ case x ~ y ~ Some(z) => (x + y + z, Finished) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

259 
case x ~ y ~ None => (x + y, Verbatim) } 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

260 
case Verbatim => 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

261 
verbatim_body ~ opt_term("*}") ^^ 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

262 
{ case x ~ Some(y) => (x + y, Finished) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

263 
case x ~ None => (x, Verbatim) } 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

264 
case _ => failure("") 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

265 
} 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

266 
}.named("verbatim_context") 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

267 

34140  268 

34143  269 
/* nested comments */ 
270 

43412  271 
private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)] 
34143  272 
{ 
43412  273 
require(depth >= 0) 
274 

34143  275 
val comment_text = 
42441
781c622af16a
more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents:
40523
diff
changeset

276 
rep1(many1(sym => sym != "*" && sym != "(")  """\*(?!\))\((?!\*)""".r) 
34143  277 

278 
def apply(in: Input) = 

279 
{ 

280 
var rest = in 

42441
781c622af16a
more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents:
40523
diff
changeset

281 
def try_parse[A](p: Parser[A]): Boolean = 
34143  282 
{ 
42441
781c622af16a
more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents:
40523
diff
changeset

283 
parse(p ^^^ (), rest) match { 
34143  284 
case Success(_, next) => { rest = next; true } 
285 
case _ => false 

286 
} 

287 
} 

43412  288 
var d = depth 
34143  289 
var finished = false 
290 
while (!finished) { 

43412  291 
if (try_parse("(*")) d += 1 
292 
else if (d > 0 && try_parse("*)")) d = 1 

293 
else if (d == 0  !try_parse(comment_text)) finished = true 

34143  294 
} 
43412  295 
if (in.offset < rest.offset) 
296 
Success((in.source.subSequence(in.offset, rest.offset).toString, d), rest) 

34143  297 
else Failure("comment expected", in) 
298 
} 

43412  299 
}.named("comment_depth") 
300 

301 
def comment: Parser[String] = 

302 
comment_depth(0) ^? { case (x, d) if d == 0 => x } 

303 

304 
def comment_context(ctxt: Context): Parser[(String, Context)] = 

305 
{ 

306 
val depth = 

307 
ctxt match { 

308 
case Finished => 0 

309 
case Comment(d) => d 

310 
case _ => 1 

311 
} 

312 
if (depth >= 0) 

313 
comment_depth(depth) ^^ 

314 
{ case (x, 0) => (x, Finished) 

315 
case (x, d) => (x, Comment(d)) } 

316 
else failure("") 

317 
} 

34143  318 

319 
def comment_content(source: String): String = 

320 
{ 

321 
require(parseAll(comment, source).successful) 

322 
source.substring(2, source.length  2) 

323 
} 

324 

325 

34140  326 
/* outer syntax tokens */ 
327 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

328 
private def delimited_token: Parser[Token] = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

329 
{ 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

330 
val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x)) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

331 
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

332 
val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x)) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

333 
val cmt = comment ^^ (x => Token(Token.Kind.COMMENT, x)) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

334 

0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

335 
string  (alt_string  (verb  cmt)) 
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 

0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

338 
private def other_token(symbols: Symbol.Interpretation, is_command: String => Boolean) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

339 
: Parser[Token] = 
34140  340 
{ 
341 
val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y } 

342 
val nat = many1(symbols.is_digit) 

40290
47f572aff50a
support for floatingpoint tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38367
diff
changeset

343 
val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z } 
34140  344 
val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x } 
345 

346 
val ident = id ~ rep("." ~> id) ^^ 

36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset

347 
{ 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

348 
case x ~ ys => Token(Token.Kind.LONG_IDENT, (x :: ys).mkString(".")) } 
34140  349 

36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset

350 
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

351 
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

352 
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

353 
val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x)) 
40290
47f572aff50a
support for floatingpoint tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38367
diff
changeset

354 
val float = 
47f572aff50a
support for floatingpoint tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents:
38367
diff
changeset

355 
("" ~ natdot ^^ { case x ~ y => x + y }  natdot) ^^ (x => Token(Token.Kind.FLOAT, x)) 
34140  356 

357 
val sym_ident = 

40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40290
diff
changeset

358 
(many1(symbols.is_symbolic_char)  one(sym => symbols.is_symbolic(sym))) ^^ 
36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset

359 
(x => Token(Token.Kind.SYM_IDENT, x)) 
34140  360 

36956
21be4832c362
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents:
36679
diff
changeset

361 
val space = many1(symbols.is_blank) ^^ (x => Token(Token.Kind.SPACE, x)) 
34140  362 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

363 
// FIXME check 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

364 
val junk = many(sym => !(symbols.is_blank(sym))) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

365 
val junk1 = many1(sym => !(symbols.is_blank(sym))) 
34140  366 

34267  367 
val bad_delimiter = 
38367  368 
("\""  "`"  "{*"  "(*") ~ 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

369 
val bad = junk1 ^^ (x => Token(Token.Kind.UNPARSED, x)) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

370 

0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

371 
val command_keyword = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

372 
keyword ^^ (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x)) 
34140  373 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

374 
space  (bad_delimiter  
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

375 
(((ident  (var_  (type_ident  (type_var  (float  (nat_  sym_ident))))))  
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

376 
command_keyword)  bad)) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

377 
} 
34140  378 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

379 
def token(symbols: Symbol.Interpretation, is_command: String => Boolean): Parser[Token] = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

380 
delimited_token  other_token(symbols, is_command) 
34140  381 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

382 
def token_context(symbols: Symbol.Interpretation, is_command: String => Boolean, ctxt: Context) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

383 
: Parser[(Token, Context)] = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

384 
{ 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

385 
val string = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

386 
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

387 
val alt_string = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

388 
quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) } 
43412  389 
val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) } 
390 
val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) } 

391 

43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

392 
val other: Parser[(Token, Context)] = 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

393 
ctxt match { 
43412  394 
case Finished => other_token(symbols, is_command) ^^ { case x => (x, Finished) } 
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

395 
case _ => failure("") 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

396 
} 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

397 

43412  398 
string  (alt_string  (verb  (cmt  other))) 
34140  399 
} 
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset

400 
} 
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

401 

7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset

402 

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 

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 
/** 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

405 

36679
ac021aed685e
use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;
wenzelm
parents:
36012
diff
changeset

406 
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

407 
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

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 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

410 
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

411 
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

412 

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 
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

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 
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

416 
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

417 
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

418 

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 
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

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 
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

422 
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

423 
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

424 
} 
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset

425 
} 
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 
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

428 

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 
def byte_reader(file: File): 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

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 
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

432 
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

433 
(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

434 
{ 
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 
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

436 
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

437 
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

438 
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

439 
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

440 
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

441 
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

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 
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

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 
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

446 

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 
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

448 
{ 
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 
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

450 
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

451 
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

452 
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

453 
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

454 
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

455 
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

456 
} 
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset

457 
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

458 
} 
31648  459 
} 