src/Pure/General/scan.scala
author wenzelm
Mon Dec 01 15:21:49 2014 +0100 (2014-12-01)
changeset 59073 dcecfcc56dce
parent 58505 d1fe47fe5401
child 59319 677615cba30d
permissions -rw-r--r--
more merge operations;
wenzelm@31648
     1
/*  Title:      Pure/General/scan.scala
wenzelm@31648
     2
    Author:     Makarius
wenzelm@31648
     3
wenzelm@40523
     4
Efficient scanning of keywords and tokens.
wenzelm@31648
     5
*/
wenzelm@31648
     6
wenzelm@31648
     7
package isabelle
wenzelm@31648
     8
wenzelm@34187
     9
wenzelm@55980
    10
import scala.annotation.tailrec
wenzelm@46627
    11
import scala.collection.{IndexedSeq, TraversableOnce}
wenzelm@34187
    12
import scala.collection.immutable.PagedSeq
wenzelm@34187
    13
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
wenzelm@31648
    14
import scala.util.parsing.combinator.RegexParsers
wenzelm@31648
    15
wenzelm@56822
    16
import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream}
wenzelm@56822
    17
import java.net.URL
wenzelm@34187
    18
wenzelm@31648
    19
wenzelm@31648
    20
object Scan
wenzelm@31648
    21
{
wenzelm@55510
    22
  /** context of partial line-oriented scans **/
wenzelm@43411
    23
wenzelm@55510
    24
  abstract class Line_Context
wenzelm@55510
    25
  case object Finished extends Line_Context
wenzelm@55510
    26
  case class Quoted(quote: String) extends Line_Context
wenzelm@55510
    27
  case object Verbatim extends Line_Context
wenzelm@55510
    28
  case class Cartouche(depth: Int) extends Line_Context
wenzelm@55510
    29
  case class Comment(depth: Int) extends Line_Context
wenzelm@43411
    30
wenzelm@43411
    31
wenzelm@43411
    32
wenzelm@55492
    33
  /** parser combinators **/
wenzelm@31650
    34
wenzelm@55492
    35
  object Parsers extends Parsers
wenzelm@36011
    36
wenzelm@55492
    37
  trait Parsers extends RegexParsers
wenzelm@55492
    38
  {
wenzelm@31649
    39
    override val whiteSpace = "".r
wenzelm@31649
    40
wenzelm@34137
    41
wenzelm@43411
    42
    /* optional termination */
wenzelm@43411
    43
wenzelm@43411
    44
    def opt_term[T](p: => Parser[T]): Parser[Option[T]] =
wenzelm@43411
    45
      p ^^ (x => Some(x)) | """\z""".r ^^ (_ => None)
wenzelm@43411
    46
wenzelm@43411
    47
wenzelm@55497
    48
    /* repeated symbols */
wenzelm@34137
    49
wenzelm@55497
    50
    def repeated(pred: Symbol.Symbol => Boolean, min_count: Int, max_count: Int): Parser[String] =
wenzelm@34140
    51
      new Parser[String]
wenzelm@34135
    52
      {
wenzelm@34137
    53
        def apply(in: Input) =
wenzelm@34137
    54
        {
wenzelm@34137
    55
          val start = in.offset
wenzelm@34137
    56
          val end = in.source.length
wenzelm@34137
    57
          val matcher = new Symbol.Matcher(in.source)
wenzelm@34137
    58
wenzelm@34137
    59
          var i = start
wenzelm@34137
    60
          var count = 0
wenzelm@34137
    61
          var finished = false
wenzelm@55034
    62
          while (!finished && i < end && count < max_count) {
wenzelm@55034
    63
            val n = matcher(i, end)
wenzelm@55034
    64
            val sym = in.source.subSequence(i, i + n).toString
wenzelm@55034
    65
            if (pred(sym)) { i += n; count += 1 }
wenzelm@34137
    66
            else finished = true
wenzelm@34137
    67
          }
wenzelm@34140
    68
          if (count < min_count) Failure("bad input", in)
wenzelm@34140
    69
          else Success(in.source.subSequence(start, i).toString, in.drop(i - start))
wenzelm@34137
    70
        }
wenzelm@55497
    71
      }.named("repeated")
wenzelm@34137
    72
wenzelm@43696
    73
    def one(pred: Symbol.Symbol => Boolean): Parser[String] =
wenzelm@55497
    74
      repeated(pred, 1, 1)
wenzelm@43696
    75
wenzelm@43696
    76
    def many(pred: Symbol.Symbol => Boolean): Parser[String] =
wenzelm@55497
    77
      repeated(pred, 0, Integer.MAX_VALUE)
wenzelm@43696
    78
wenzelm@43696
    79
    def many1(pred: Symbol.Symbol => Boolean): Parser[String] =
wenzelm@55497
    80
      repeated(pred, 1, Integer.MAX_VALUE)
wenzelm@55497
    81
wenzelm@55497
    82
wenzelm@55497
    83
    /* character */
wenzelm@55497
    84
wenzelm@55497
    85
    def character(pred: Char => Boolean): Symbol.Symbol => Boolean =
wenzelm@55497
    86
      (s: Symbol. Symbol) => s.length == 1 && pred(s.charAt(0))
wenzelm@34140
    87
wenzelm@34140
    88
wenzelm@34143
    89
    /* quoted strings */
wenzelm@34140
    90
wenzelm@43696
    91
    private def quoted_body(quote: Symbol.Symbol): Parser[String] =
wenzelm@43411
    92
    {
wenzelm@43411
    93
      rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" |
wenzelm@43411
    94
        (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString)
wenzelm@43411
    95
    }
wenzelm@43411
    96
wenzelm@55494
    97
    def quoted(quote: Symbol.Symbol): Parser[String] =
wenzelm@34143
    98
    {
wenzelm@43411
    99
      quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z }
wenzelm@34143
   100
    }.named("quoted")
wenzelm@34140
   101
wenzelm@43696
   102
    def quoted_content(quote: Symbol.Symbol, source: String): String =
wenzelm@34140
   103
    {
wenzelm@34140
   104
      require(parseAll(quoted(quote), source).successful)
wenzelm@34189
   105
      val body = source.substring(1, source.length - 1)
wenzelm@34189
   106
      if (body.exists(_ == '\\')) {
wenzelm@34189
   107
        val content =
wenzelm@40523
   108
          rep(many1(sym => sym != quote && sym != "\\") |
wenzelm@34189
   109
              "\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString }))
wenzelm@34189
   110
        parseAll(content ^^ (_.mkString), body).get
wenzelm@34189
   111
      }
wenzelm@34189
   112
      else body
wenzelm@34140
   113
    }
wenzelm@34140
   114
wenzelm@55510
   115
    def quoted_line(quote: Symbol.Symbol, ctxt: Line_Context): Parser[(String, Line_Context)] =
wenzelm@43411
   116
    {
wenzelm@43411
   117
      ctxt match {
wenzelm@43411
   118
        case Finished =>
wenzelm@43411
   119
          quote ~ quoted_body(quote) ~ opt_term(quote) ^^
wenzelm@43411
   120
            { case x ~ y ~ Some(z) => (x + y + z, Finished)
wenzelm@43411
   121
              case x ~ y ~ None => (x + y, Quoted(quote)) }
wenzelm@43411
   122
        case Quoted(q) if q == quote =>
wenzelm@43411
   123
          quoted_body(quote) ~ opt_term(quote) ^^
wenzelm@43411
   124
            { case x ~ Some(y) => (x + y, Finished)
wenzelm@43411
   125
              case x ~ None => (x, ctxt) }
wenzelm@43411
   126
        case _ => failure("")
wenzelm@43411
   127
      }
wenzelm@55510
   128
    }.named("quoted_line")
wenzelm@43411
   129
wenzelm@48763
   130
    def recover_quoted(quote: Symbol.Symbol): Parser[String] =
wenzelm@48763
   131
      quote ~ quoted_body(quote) ^^ { case x ~ y => x + y }
wenzelm@48743
   132
wenzelm@34140
   133
wenzelm@34143
   134
    /* verbatim text */
wenzelm@34143
   135
wenzelm@43411
   136
    private def verbatim_body: Parser[String] =
wenzelm@43411
   137
      rep(many1(sym => sym != "*") | """\*(?!\})""".r) ^^ (_.mkString)
wenzelm@43411
   138
wenzelm@55494
   139
    def verbatim: Parser[String] =
wenzelm@34143
   140
    {
wenzelm@43411
   141
      "{*" ~ verbatim_body ~ "*}" ^^ { case x ~ y ~ z => x + y + z }
wenzelm@34143
   142
    }.named("verbatim")
wenzelm@34140
   143
wenzelm@34140
   144
    def verbatim_content(source: String): String =
wenzelm@34140
   145
    {
wenzelm@34140
   146
      require(parseAll(verbatim, source).successful)
wenzelm@34140
   147
      source.substring(2, source.length - 2)
wenzelm@34140
   148
    }
wenzelm@34140
   149
wenzelm@55510
   150
    def verbatim_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
wenzelm@43411
   151
    {
wenzelm@43411
   152
      ctxt match {
wenzelm@43411
   153
        case Finished =>
wenzelm@43411
   154
          "{*" ~ verbatim_body ~ opt_term("*}") ^^
wenzelm@43411
   155
            { case x ~ y ~ Some(z) => (x + y + z, Finished)
wenzelm@43411
   156
              case x ~ y ~ None => (x + y, Verbatim) }
wenzelm@43411
   157
        case Verbatim =>
wenzelm@43411
   158
          verbatim_body ~ opt_term("*}") ^^
wenzelm@43411
   159
            { case x ~ Some(y) => (x + y, Finished)
wenzelm@43411
   160
              case x ~ None => (x, Verbatim) }
wenzelm@43411
   161
        case _ => failure("")
wenzelm@43411
   162
      }
wenzelm@55510
   163
    }.named("verbatim_line")
wenzelm@43411
   164
wenzelm@48763
   165
    val recover_verbatim: Parser[String] =
wenzelm@48763
   166
      "{*" ~ verbatim_body ^^ { case x ~ y => x + y }
wenzelm@48743
   167
wenzelm@34140
   168
wenzelm@55033
   169
    /* nested text cartouches */
wenzelm@55033
   170
wenzelm@55033
   171
    private def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
wenzelm@55033
   172
    {
wenzelm@55033
   173
      require(depth >= 0)
wenzelm@55033
   174
wenzelm@55033
   175
      def apply(in: Input) =
wenzelm@55033
   176
      {
wenzelm@55033
   177
        val start = in.offset
wenzelm@55033
   178
        val end = in.source.length
wenzelm@55033
   179
        val matcher = new Symbol.Matcher(in.source)
wenzelm@55033
   180
wenzelm@55033
   181
        var i = start
wenzelm@55033
   182
        var d = depth
wenzelm@55033
   183
        var finished = false
wenzelm@55034
   184
        while (!finished && i < end) {
wenzelm@55034
   185
          val n = matcher(i, end)
wenzelm@55034
   186
          val sym = in.source.subSequence(i, i + n).toString
wenzelm@55034
   187
          if (Symbol.is_open(sym)) { i += n; d += 1 }
wenzelm@58505
   188
          else if (Symbol.is_close(sym) && d > 0) { i += n; d -= 1; if (d == 0) finished = true }
wenzelm@58505
   189
          else if (d > 0) i += n
wenzelm@55033
   190
          else finished = true
wenzelm@55033
   191
        }
wenzelm@55033
   192
        if (i == start) Failure("bad input", in)
wenzelm@55033
   193
        else Success((in.source.subSequence(start, i).toString, d), in.drop(i - start))
wenzelm@55033
   194
      }
wenzelm@55033
   195
    }.named("cartouche_depth")
wenzelm@55033
   196
wenzelm@55033
   197
    def cartouche: Parser[String] =
wenzelm@55033
   198
      cartouche_depth(0) ^? { case (x, d) if d == 0 => x }
wenzelm@55033
   199
wenzelm@55510
   200
    def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
wenzelm@55033
   201
    {
wenzelm@55033
   202
      val depth =
wenzelm@55033
   203
        ctxt match {
wenzelm@55033
   204
          case Finished => 0
wenzelm@55033
   205
          case Cartouche(d) => d
wenzelm@55033
   206
          case _ => -1
wenzelm@55033
   207
        }
wenzelm@55033
   208
      if (depth >= 0)
wenzelm@55033
   209
        cartouche_depth(depth) ^^
wenzelm@55033
   210
          { case (x, 0) => (x, Finished)
wenzelm@55033
   211
            case (x, d) => (x, Cartouche(d)) }
wenzelm@55033
   212
      else failure("")
wenzelm@55033
   213
    }
wenzelm@55033
   214
wenzelm@55033
   215
    val recover_cartouche: Parser[String] =
wenzelm@55033
   216
      cartouche_depth(0) ^^ (_._1)
wenzelm@55033
   217
wenzelm@55033
   218
    def cartouche_content(source: String): String =
wenzelm@55033
   219
    {
wenzelm@55033
   220
      def err(): Nothing = error("Malformed text cartouche: " + quote(source))
wenzelm@55033
   221
      val source1 =
wenzelm@55033
   222
        Library.try_unprefix(Symbol.open_decoded, source) orElse
wenzelm@55033
   223
          Library.try_unprefix(Symbol.open, source) getOrElse err()
wenzelm@55033
   224
      Library.try_unsuffix(Symbol.close_decoded, source1) orElse
wenzelm@55033
   225
        Library.try_unsuffix(Symbol.close, source1) getOrElse err()
wenzelm@55033
   226
    }
wenzelm@55033
   227
wenzelm@55033
   228
wenzelm@34143
   229
    /* nested comments */
wenzelm@34143
   230
wenzelm@43412
   231
    private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
wenzelm@34143
   232
    {
wenzelm@43412
   233
      require(depth >= 0)
wenzelm@43412
   234
wenzelm@34143
   235
      val comment_text =
wenzelm@42441
   236
        rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r)
wenzelm@34143
   237
wenzelm@34143
   238
      def apply(in: Input) =
wenzelm@34143
   239
      {
wenzelm@34143
   240
        var rest = in
wenzelm@42441
   241
        def try_parse[A](p: Parser[A]): Boolean =
wenzelm@34143
   242
        {
wenzelm@56663
   243
          parse(p ^^^ (()), rest) match {
wenzelm@34143
   244
            case Success(_, next) => { rest = next; true }
wenzelm@34143
   245
            case _ => false
wenzelm@34143
   246
          }
wenzelm@34143
   247
        }
wenzelm@43412
   248
        var d = depth
wenzelm@34143
   249
        var finished = false
wenzelm@34143
   250
        while (!finished) {
wenzelm@43412
   251
          if (try_parse("(*")) d += 1
wenzelm@58505
   252
          else if (d > 0 && try_parse("*)")) { d -= 1; if (d == 0) finished = true }
wenzelm@43412
   253
          else if (d == 0 || !try_parse(comment_text)) finished = true
wenzelm@34143
   254
        }
wenzelm@43412
   255
        if (in.offset < rest.offset)
wenzelm@43412
   256
          Success((in.source.subSequence(in.offset, rest.offset).toString, d), rest)
wenzelm@34143
   257
        else Failure("comment expected", in)
wenzelm@34143
   258
      }
wenzelm@43412
   259
    }.named("comment_depth")
wenzelm@43412
   260
wenzelm@43412
   261
    def comment: Parser[String] =
wenzelm@43412
   262
      comment_depth(0) ^? { case (x, d) if d == 0 => x }
wenzelm@43412
   263
wenzelm@55510
   264
    def comment_line(ctxt: Line_Context): Parser[(String, Line_Context)] =
wenzelm@43412
   265
    {
wenzelm@43412
   266
      val depth =
wenzelm@43412
   267
        ctxt match {
wenzelm@43412
   268
          case Finished => 0
wenzelm@43412
   269
          case Comment(d) => d
wenzelm@43412
   270
          case _ => -1
wenzelm@43412
   271
        }
wenzelm@43412
   272
      if (depth >= 0)
wenzelm@43412
   273
        comment_depth(depth) ^^
wenzelm@43412
   274
          { case (x, 0) => (x, Finished)
wenzelm@43412
   275
            case (x, d) => (x, Comment(d)) }
wenzelm@43412
   276
      else failure("")
wenzelm@43412
   277
    }
wenzelm@34143
   278
wenzelm@48763
   279
    val recover_comment: Parser[String] =
wenzelm@48763
   280
      comment_depth(0) ^^ (_._1)
wenzelm@34143
   281
wenzelm@55033
   282
    def comment_content(source: String): String =
wenzelm@55033
   283
    {
wenzelm@55033
   284
      require(parseAll(comment, source).successful)
wenzelm@55033
   285
      source.substring(2, source.length - 2)
wenzelm@55033
   286
    }
wenzelm@55033
   287
wenzelm@34143
   288
wenzelm@55492
   289
    /* keyword */
wenzelm@55492
   290
wenzelm@55497
   291
    def literal(lexicon: Lexicon): Parser[String] = new Parser[String]
wenzelm@55492
   292
    {
wenzelm@55492
   293
      def apply(in: Input) =
wenzelm@55492
   294
      {
wenzelm@55492
   295
        val result = lexicon.scan(in)
wenzelm@55492
   296
        if (result.isEmpty) Failure("keyword expected", in)
wenzelm@55492
   297
        else Success(result, in.drop(result.length))
wenzelm@55492
   298
      }
wenzelm@55492
   299
    }.named("keyword")
wenzelm@31649
   300
  }
wenzelm@55492
   301
wenzelm@55492
   302
wenzelm@55492
   303
wenzelm@55492
   304
  /** Lexicon -- position tree **/
wenzelm@55492
   305
wenzelm@55492
   306
  object Lexicon
wenzelm@55492
   307
  {
wenzelm@55492
   308
    /* representation */
wenzelm@55492
   309
wenzelm@55492
   310
    private sealed case class Tree(val branches: Map[Char, (String, Tree)])
wenzelm@55492
   311
    private val empty_tree = Tree(Map())
wenzelm@55492
   312
wenzelm@55492
   313
    val empty: Lexicon = new Lexicon(empty_tree)
wenzelm@55492
   314
    def apply(elems: String*): Lexicon = empty ++ elems
wenzelm@55492
   315
  }
wenzelm@55492
   316
wenzelm@55492
   317
  final class Lexicon private(rep: Lexicon.Tree)
wenzelm@55492
   318
  {
wenzelm@55492
   319
    /* auxiliary operations */
wenzelm@55492
   320
wenzelm@59073
   321
    private def dest(tree: Lexicon.Tree, result: List[String]): List[String] =
wenzelm@55492
   322
      (result /: tree.branches.toList) ((res, entry) =>
wenzelm@55492
   323
        entry match { case (_, (s, tr)) =>
wenzelm@59073
   324
          if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) })
wenzelm@55492
   325
wenzelm@55492
   326
    private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
wenzelm@55492
   327
    {
wenzelm@55492
   328
      val len = str.length
wenzelm@55980
   329
      @tailrec def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
wenzelm@55492
   330
      {
wenzelm@55492
   331
        if (i < len) {
wenzelm@55492
   332
          tree.branches.get(str.charAt(i)) match {
wenzelm@55492
   333
            case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
wenzelm@55492
   334
            case None => None
wenzelm@55492
   335
          }
wenzelm@55980
   336
        }
wenzelm@55980
   337
        else Some(tip, tree)
wenzelm@55492
   338
      }
wenzelm@55492
   339
      look(rep, false, 0)
wenzelm@55492
   340
    }
wenzelm@55492
   341
wenzelm@55492
   342
    def completions(str: CharSequence): List[String] =
wenzelm@55492
   343
      lookup(str) match {
wenzelm@59073
   344
        case Some((true, tree)) => dest(tree, List(str.toString))
wenzelm@59073
   345
        case Some((false, tree)) => dest(tree, Nil)
wenzelm@55492
   346
        case None => Nil
wenzelm@55492
   347
      }
wenzelm@55492
   348
wenzelm@55492
   349
wenzelm@55492
   350
    /* pseudo Set methods */
wenzelm@55492
   351
wenzelm@59073
   352
    def raw_iterator: Iterator[String] = dest(rep, Nil).iterator
wenzelm@59073
   353
    def iterator: Iterator[String] = dest(rep, Nil).sorted.iterator
wenzelm@55492
   354
wenzelm@55492
   355
    override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
wenzelm@55492
   356
wenzelm@59073
   357
    def is_empty: Boolean = rep.branches.isEmpty
wenzelm@55492
   358
wenzelm@55492
   359
    def contains(elem: String): Boolean =
wenzelm@55492
   360
      lookup(elem) match {
wenzelm@55492
   361
        case Some((tip, _)) => tip
wenzelm@55492
   362
        case _ => false
wenzelm@55492
   363
      }
wenzelm@55492
   364
wenzelm@55492
   365
wenzelm@59073
   366
    /* build lexicon */
wenzelm@55492
   367
wenzelm@55492
   368
    def + (elem: String): Lexicon =
wenzelm@55492
   369
      if (contains(elem)) this
wenzelm@55492
   370
      else {
wenzelm@55492
   371
        val len = elem.length
wenzelm@55492
   372
        def extend(tree: Lexicon.Tree, i: Int): Lexicon.Tree =
wenzelm@55492
   373
          if (i < len) {
wenzelm@55492
   374
            val c = elem.charAt(i)
wenzelm@55492
   375
            val end = (i + 1 == len)
wenzelm@55492
   376
            tree.branches.get(c) match {
wenzelm@55492
   377
              case Some((s, tr)) =>
wenzelm@55492
   378
                Lexicon.Tree(tree.branches +
wenzelm@55492
   379
                  (c -> (if (end) elem else s, extend(tr, i + 1))))
wenzelm@55492
   380
              case None =>
wenzelm@55492
   381
                Lexicon.Tree(tree.branches +
wenzelm@55492
   382
                  (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
wenzelm@55492
   383
            }
wenzelm@55492
   384
          }
wenzelm@55492
   385
          else tree
wenzelm@55492
   386
        new Lexicon(extend(rep, 0))
wenzelm@55492
   387
      }
wenzelm@55492
   388
wenzelm@55492
   389
    def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
wenzelm@55492
   390
wenzelm@59073
   391
    def ++ (other: Lexicon): Lexicon =
wenzelm@59073
   392
      if (this eq other) this
wenzelm@59073
   393
      else if (is_empty) other
wenzelm@59073
   394
      else this ++ other.raw_iterator
wenzelm@59073
   395
wenzelm@55492
   396
wenzelm@55492
   397
    /* scan */
wenzelm@55492
   398
wenzelm@55492
   399
    def scan(in: Reader[Char]): String =
wenzelm@55492
   400
    {
wenzelm@55492
   401
      val source = in.source
wenzelm@55492
   402
      val offset = in.offset
wenzelm@55492
   403
      val len = source.length - offset
wenzelm@55492
   404
wenzelm@55492
   405
      def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String =
wenzelm@55492
   406
      {
wenzelm@55492
   407
        if (i < len) {
wenzelm@55492
   408
          tree.branches.get(source.charAt(offset + i)) match {
wenzelm@55492
   409
            case Some((s, tr)) => scan_tree(tr, if (s.isEmpty) result else s, i + 1)
wenzelm@55492
   410
            case None => result
wenzelm@55492
   411
          }
wenzelm@55492
   412
        }
wenzelm@55492
   413
        else result
wenzelm@55492
   414
      }
wenzelm@55492
   415
      scan_tree(rep, "", 0)
wenzelm@55492
   416
    }
wenzelm@55492
   417
  }
wenzelm@56821
   418
wenzelm@56821
   419
wenzelm@56821
   420
wenzelm@56822
   421
  /** read stream without decoding: efficient length operation **/
wenzelm@56821
   422
wenzelm@56821
   423
  private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int)
wenzelm@56821
   424
    extends CharSequence
wenzelm@56821
   425
  {
wenzelm@56821
   426
    def charAt(i: Int): Char =
wenzelm@56821
   427
      if (0 <= i && i < length) seq(start + i)
wenzelm@56821
   428
      else throw new IndexOutOfBoundsException
wenzelm@56821
   429
wenzelm@56822
   430
    def length: Int = end - start  // avoid expensive seq.length
wenzelm@56821
   431
wenzelm@56821
   432
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@56821
   433
      if (0 <= i && i <= j && j <= length) new Restricted_Seq(seq, start + i, start + j)
wenzelm@56821
   434
      else throw new IndexOutOfBoundsException
wenzelm@56821
   435
wenzelm@56821
   436
    override def toString: String =
wenzelm@56821
   437
    {
wenzelm@56821
   438
      val buf = new StringBuilder(length)
wenzelm@56821
   439
      for (offset <- start until end) buf.append(seq(offset))
wenzelm@56821
   440
      buf.toString
wenzelm@56821
   441
    }
wenzelm@56821
   442
  }
wenzelm@56821
   443
wenzelm@56821
   444
  abstract class Byte_Reader extends Reader[Char] { def close: Unit }
wenzelm@56821
   445
wenzelm@56822
   446
  private def make_byte_reader(stream: InputStream, stream_length: Int): Byte_Reader =
wenzelm@56821
   447
  {
wenzelm@56822
   448
    val buffered_stream = new BufferedInputStream(stream)
wenzelm@56821
   449
    val seq = new PagedSeq(
wenzelm@56821
   450
      (buf: Array[Char], offset: Int, length: Int) =>
wenzelm@56821
   451
        {
wenzelm@56821
   452
          var i = 0
wenzelm@56821
   453
          var c = 0
wenzelm@56821
   454
          var eof = false
wenzelm@56821
   455
          while (!eof && i < length) {
wenzelm@56822
   456
            c = buffered_stream.read
wenzelm@56821
   457
            if (c == -1) eof = true
wenzelm@56821
   458
            else { buf(offset + i) = c.toChar; i += 1 }
wenzelm@56821
   459
          }
wenzelm@56821
   460
          if (i > 0) i else -1
wenzelm@56821
   461
        })
wenzelm@56822
   462
    val restricted_seq = new Restricted_Seq(seq, 0, stream_length)
wenzelm@56821
   463
wenzelm@56821
   464
    class Paged_Reader(override val offset: Int) extends Byte_Reader
wenzelm@56821
   465
    {
wenzelm@56821
   466
      override lazy val source: CharSequence = restricted_seq
wenzelm@56827
   467
      def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\u001a'
wenzelm@56821
   468
      def rest: Paged_Reader = if (seq.isDefinedAt(offset)) new Paged_Reader(offset + 1) else this
wenzelm@56821
   469
      def pos: InputPosition = new OffsetPosition(source, offset)
wenzelm@56821
   470
      def atEnd: Boolean = !seq.isDefinedAt(offset)
wenzelm@56821
   471
      override def drop(n: Int): Paged_Reader = new Paged_Reader(offset + n)
wenzelm@56822
   472
      def close { buffered_stream.close }
wenzelm@56821
   473
    }
wenzelm@56821
   474
    new Paged_Reader(0)
wenzelm@56821
   475
  }
wenzelm@56822
   476
wenzelm@56822
   477
  def byte_reader(file: JFile): Byte_Reader =
wenzelm@56822
   478
    make_byte_reader(new FileInputStream(file), file.length.toInt)
wenzelm@56822
   479
wenzelm@56822
   480
  def byte_reader(url: URL): Byte_Reader =
wenzelm@56822
   481
  {
wenzelm@56822
   482
    val connection = url.openConnection
wenzelm@56822
   483
    val stream = connection.getInputStream
wenzelm@56822
   484
    val stream_length = connection.getContentLength
wenzelm@56822
   485
    make_byte_reader(stream, stream_length)
wenzelm@56822
   486
  }
wenzelm@31648
   487
}