author  wenzelm 
Thu, 16 Jun 2011 17:25:16 +0200  
changeset 43411  0206466ee473 
parent 42718  d7b2625c1193 
child 43412  81517eed8a78 
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 

271 
def comment: Parser[String] = new Parser[String] 

272 
{ 

273 
val comment_text = 

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

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

276 
def apply(in: Input) = 

277 
{ 

278 
var rest = in 

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

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

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

284 
} 

285 
} 

286 
var depth = 0 

287 
var finished = false 

288 
while (!finished) { 

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

289 
if (try_parse("(*")) depth += 1 
781c622af16a
more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents:
40523
diff
changeset

290 
else if (depth > 0 && try_parse("*)")) depth = 1 
781c622af16a
more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents:
40523
diff
changeset

291 
else if (depth == 0  !try_parse(comment_text)) finished = true 
34143  292 
} 
293 
if (in.offset < rest.offset && depth == 0) 

294 
Success(in.source.subSequence(in.offset, rest.offset).toString, rest) 

295 
else Failure("comment expected", in) 

296 
} 

297 
}.named("comment") 

298 

299 
def comment_content(source: String): String = 

300 
{ 

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

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

303 
} 

304 

305 

34140  306 
/* outer syntax tokens */ 
307 

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

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

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

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

311 
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

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

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

314 

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

315 
string  (alt_string  (verb  cmt)) 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

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

317 

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

318 
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

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

322 
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

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

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

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

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

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

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

330 
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

331 
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

332 
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

333 
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

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

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

337 
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

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

339 
(x => Token(Token.Kind.SYM_IDENT, x)) 
34140  340 

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

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

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

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

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

345 
val junk1 = many1(sym => !(symbols.is_blank(sym))) 
34140  346 

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

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

350 

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

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

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

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

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

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

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

357 
} 
34140  358 

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

359 
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

360 
delimited_token  other_token(symbols, is_command) 
34140  361 

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

362 
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

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

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

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

366 
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

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

368 
quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) } 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

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

370 
verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) } 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

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

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

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

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

375 
case Finished => (cmt  other_token(symbols, is_command)) ^^ { case x => (x, Finished) } 
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset

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

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

378 

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

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

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

382 

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

383 

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

384 

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

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

386 

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

387 
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

388 
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

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

390 
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

391 
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

392 
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

393 

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

394 
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

395 

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

396 
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

397 
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

398 
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

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

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

403 
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

404 
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

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

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

409 

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

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

413 
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

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

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

417 
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

418 
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

419 
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

420 
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

421 
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

422 
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

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

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

427 

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

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

431 
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

432 
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

433 
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

434 
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

435 
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

436 
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

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

439 
} 
31648  440 
} 