src/Pure/General/scan.scala
author wenzelm
Thu, 16 Jun 2011 18:00:56 +0200
changeset 43412 81517eed8a78
parent 43411 0206466ee473
child 43420 a26e514c92b2
permissions -rw-r--r--
partial scans of nested comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/scan.scala
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
     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
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
     5
*/
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
     6
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
     7
package isabelle
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
     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
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    14
import scala.util.parsing.combinator.RegexParsers
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    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
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    18
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    19
object Scan
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    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
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    32
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    33
  object Lexicon
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    34
  {
42718
d7b2625c1193 minor adaption for scala-2.9.0.final;
wenzelm
parents: 42441
diff changeset
    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
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    40
  }
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    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
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    43
  {
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    44
    /* representation */
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    45
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    46
    import Lexicon.Tree
31764
e767fee21b22 moved string utilities to completion.scala;
wenzelm
parents: 31762
diff changeset
    47
    protected val main_tree: Tree = Lexicon.empty_tree
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    48
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    49
31650
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    50
    /* auxiliary operations */
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    51
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    52
    private def content(tree: Tree, result: List[String]): List[String] =
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    53
      (result /: tree.branches.toList) ((res, entry) =>
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    54
        entry match { case (_, (s, tr)) =>
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    55
          if (s.isEmpty) content(tr, res) else content(tr, s :: res) })
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    56
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    57
    private def lookup(str: CharSequence): Option[(Boolean, Tree)] =
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    58
    {
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    59
      val len = str.length
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    60
      def look(tree: Tree, tip: Boolean, i: Int): Option[(Boolean, Tree)] =
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    61
      {
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    62
        if (i < len) {
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    63
          tree.branches.get(str.charAt(i)) match {
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    64
            case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    65
            case None => None
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    66
          }
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    67
        } else Some(tip, tree)
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    68
      }
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    69
      look(main_tree, false, 0)
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    70
    }
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    71
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    72
    def completions(str: CharSequence): List[String] =
31764
e767fee21b22 moved string utilities to completion.scala;
wenzelm
parents: 31762
diff changeset
    73
      lookup(str) match {
31650
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    74
        case Some((true, tree)) => content(tree, List(str.toString))
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    75
        case Some((false, tree)) => content(tree, Nil)
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    76
        case None => Nil
31764
e767fee21b22 moved string utilities to completion.scala;
wenzelm
parents: 31762
diff changeset
    77
      }
31650
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    78
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    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
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 36011
diff changeset
    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
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    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
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    91
        case Some((tip, _)) => tip
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    92
        case _ => false
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    93
      }
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    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
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   116
          }
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   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
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
   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
wenzelm
parents: 34267
diff changeset
   123
34137
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   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
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   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
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   135
    /* keywords from lexicon */
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   136
34140
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   137
    def keyword: Parser[String] = new Parser[String]
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   149
              case Some((s, tr)) => scan(tr, if (s.isEmpty) result else s, i + 1)
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   150
              case None => result
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   151
            }
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   152
          }
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   153
          else result
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   154
        }
34140
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   155
        val result = scan(main_tree, "", 0)
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   156
        if (result.isEmpty) Failure("keyword expected", in)
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   157
        else Success(result, in.drop(result.length))
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
   158
      }
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   159
    }.named("keyword")
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
   160
34137
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   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
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   165
      new Parser[String]
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   166
      {
34137
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   167
        def apply(in: Input) =
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   168
        {
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   169
          val start = in.offset
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   170
          val end = in.source.length
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   171
          val matcher = new Symbol.Matcher(in.source)
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   172
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   173
          var i = start
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   174
          var count = 0
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   175
          var finished = false
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   176
          while (!finished) {
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   177
            if (i < end && count < max_count) {
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   178
              val n = matcher(i, end)
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   179
              val sym = in.source.subSequence(i, i + n).toString
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   180
              if (pred(sym)) { i += n; count += 1 }
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   181
              else finished = true
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   182
            }
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   183
            else finished = true
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   184
          }
34140
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   185
          if (count < min_count) Failure("bad input", in)
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   186
          else Success(in.source.subSequence(start, i).toString, in.drop(i - start))
34137
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   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
6cc9a0cbaf55 refined some Symbol operations/signatures;
wenzelm
parents: 34135
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   193
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   194
34143
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   195
    /* quoted strings */
34140
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   203
    private def quoted(quote: String): Parser[String] =
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   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
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   206
    }.named("quoted")
34140
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   207
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   208
    def quoted_content(quote: String, source: String): String =
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   209
    {
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   210
      require(parseAll(quoted(quote), source).successful)
34189
10c5871ec684 quoted_content: handle escapes;
wenzelm
parents: 34187
diff changeset
   211
      val body = source.substring(1, source.length - 1)
10c5871ec684 quoted_content: handle escapes;
wenzelm
parents: 34187
diff changeset
   212
      if (body.exists(_ == '\\')) {
10c5871ec684 quoted_content: handle escapes;
wenzelm
parents: 34187
diff changeset
   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
10c5871ec684 quoted_content: handle escapes;
wenzelm
parents: 34187
diff changeset
   215
              "\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString }))
10c5871ec684 quoted_content: handle escapes;
wenzelm
parents: 34187
diff changeset
   216
        parseAll(content ^^ (_.mkString), body).get
10c5871ec684 quoted_content: handle escapes;
wenzelm
parents: 34187
diff changeset
   217
      }
10c5871ec684 quoted_content: handle escapes;
wenzelm
parents: 34187
diff changeset
   218
      else body
34140
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   219
    }
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   236
34143
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   237
    /* verbatim text */
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   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
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   242
    private def verbatim: Parser[String] =
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   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
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   245
    }.named("verbatim")
34140
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   246
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   247
    def verbatim_content(source: String): String =
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   248
    {
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   249
      require(parseAll(verbatim, source).successful)
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   250
      source.substring(2, source.length - 2)
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   251
    }
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   268
34143
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   269
    /* nested comments */
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   270
43412
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   271
    private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)]
34143
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   272
    {
43412
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   273
      require(depth >= 0)
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   274
34143
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   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
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   277
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   278
      def apply(in: Input) =
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   279
      {
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   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
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   282
        {
42441
781c622af16a more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents: 40523
diff changeset
   283
          parse(p ^^^ (), rest) match {
34143
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   284
            case Success(_, next) => { rest = next; true }
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   285
            case _ => false
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   286
          }
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   287
        }
43412
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   288
        var d = depth
34143
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   289
        var finished = false
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   290
        while (!finished) {
43412
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   291
          if (try_parse("(*")) d += 1
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   292
          else if (d > 0 && try_parse("*)")) d -= 1
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   293
          else if (d == 0 || !try_parse(comment_text)) finished = true
34143
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   294
        }
43412
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   295
        if (in.offset < rest.offset)
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   296
          Success((in.source.subSequence(in.offset, rest.offset).toString, d), rest)
34143
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   297
        else Failure("comment expected", in)
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   298
      }
43412
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   299
    }.named("comment_depth")
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   300
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   301
    def comment: Parser[String] =
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   302
      comment_depth(0) ^? { case (x, d) if d == 0 => x }
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   303
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   304
    def comment_context(ctxt: Context): Parser[(String, Context)] =
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   305
    {
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   306
      val depth =
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   307
        ctxt match {
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   308
          case Finished => 0
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   309
          case Comment(d) => d
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   310
          case _ => -1
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   311
        }
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   312
      if (depth >= 0)
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   313
        comment_depth(depth) ^^
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   314
          { case (x, 0) => (x, Finished)
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   315
            case (x, d) => (x, Comment(d)) }
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   316
      else failure("")
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   317
    }
34143
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   318
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   319
    def comment_content(source: String): String =
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   320
    {
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   321
      require(parseAll(comment, source).successful)
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   322
      source.substring(2, source.length - 2)
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   323
    }
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   324
ded454429df3 added nested comments;
wenzelm
parents: 34140
diff changeset
   325
34140
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   326
    /* outer syntax tokens */
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   340
    {
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   341
      val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y }
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   342
      val nat = many1(symbols.is_digit)
40290
47f572aff50a support for floating-point 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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   344
      val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   345
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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 floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 38367
diff changeset
   354
      val float =
47f572aff50a support for floating-point 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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   356
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   366
34267
92810c85262e more accurate scanning of bad input;
wenzelm
parents: 34263
diff changeset
   367
      val bad_delimiter =
38367
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 36956
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   389
      val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   390
      val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   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
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   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
81517eed8a78 partial scans of nested comments;
wenzelm
parents: 43411
diff changeset
   398
      string | (alt_string | (verb | (cmt | other)))
34140
31be1235d0fb simplified result of keyword and symbols parser;
wenzelm
parents: 34137
diff changeset
   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
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
   459
}