src/Pure/General/scan.scala
author wenzelm
Sat, 19 Dec 2009 11:48:11 +0100
changeset 34135 63dd95e3b393
parent 32450 375db037f4d2
child 34137 6cc9a0cbaf55
permissions -rw-r--r--
indicate final state of keywords; added symbol scanner;
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
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
     4
Efficient scanning of keywords.
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
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
     9
import scala.util.parsing.combinator.RegexParsers
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    10
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    11
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    12
object Scan
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    13
{
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    14
  /** Lexicon -- position tree **/
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    15
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    16
  object Lexicon
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    17
  {
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    18
    private case class Tree(val branches: Map[Char, (String, Tree)])
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    19
    private val empty_tree = Tree(Map())
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    20
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    21
    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
    22
    def apply(elems: String*): Lexicon = empty ++ elems
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    23
  }
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    24
31764
e767fee21b22 moved string utilities to completion.scala;
wenzelm
parents: 31762
diff changeset
    25
  class Lexicon extends scala.collection.Set[String] with RegexParsers
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    26
  {
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    27
    /* representation */
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    28
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    29
    import Lexicon.Tree
31764
e767fee21b22 moved string utilities to completion.scala;
wenzelm
parents: 31762
diff changeset
    30
    protected val main_tree: Tree = Lexicon.empty_tree
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    31
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    32
31650
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    33
    /* auxiliary operations */
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    34
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    35
    private def content(tree: Tree, result: List[String]): List[String] =
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    36
      (result /: tree.branches.toList) ((res, entry) =>
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    37
        entry match { case (_, (s, tr)) =>
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    38
          if (s.isEmpty) content(tr, res) else content(tr, s :: res) })
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    39
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    40
    private def lookup(str: CharSequence): Option[(Boolean, Tree)] =
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    41
    {
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    42
      val len = str.length
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    43
      def look(tree: Tree, tip: Boolean, i: Int): Option[(Boolean, Tree)] =
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    44
      {
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    45
        if (i < len) {
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    46
          tree.branches.get(str.charAt(i)) match {
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    47
            case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    48
            case None => None
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    49
          }
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    50
        } else Some(tip, tree)
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    51
      }
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    52
      look(main_tree, false, 0)
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    53
    }
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    54
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    55
    def completions(str: CharSequence): List[String] =
31764
e767fee21b22 moved string utilities to completion.scala;
wenzelm
parents: 31762
diff changeset
    56
      lookup(str) match {
31650
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    57
        case Some((true, tree)) => content(tree, List(str.toString))
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    58
        case Some((false, tree)) => content(tree, Nil)
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    59
        case None => Nil
31764
e767fee21b22 moved string utilities to completion.scala;
wenzelm
parents: 31762
diff changeset
    60
      }
31650
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    61
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    62
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    63
    /* Set methods */
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    64
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    65
    override def stringPrefix = "Lexicon"
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    66
31753
a61475260e47 Lexicon: removed unused max_entry;
wenzelm
parents: 31701
diff changeset
    67
    override def isEmpty: Boolean = { main_tree.branches.isEmpty }
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
    68
31650
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    69
    def size: Int = content(main_tree, Nil).length
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    70
    def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    71
31762
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    72
    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
    73
      lookup(elem) match {
31650
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    74
        case Some((tip, _)) => tip
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    75
        case _ => false
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
    76
      }
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    77
31762
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    78
    def + (elem: String): Lexicon =
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    79
      if (contains(elem)) this
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    80
      else {
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    81
        val len = elem.length
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    82
        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
    83
          if (i < len) {
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    84
            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
    85
            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
    86
            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
    87
              case Some((s, tr)) =>
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    88
                Tree(tree.branches +
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    89
                  (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
    90
              case None =>
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    91
                Tree(tree.branches +
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    92
                  (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
    93
            }
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
    94
          }
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
    95
          else tree
31762
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    96
        val old = this
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    97
        new Lexicon { override val main_tree = extend(old.main_tree, 0) }
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
    98
      }
31762
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
    99
31764
e767fee21b22 moved string utilities to completion.scala;
wenzelm
parents: 31762
diff changeset
   100
    def + (elem1: String, elem2: String, elems: String*): Lexicon =
31762
20745ab5b79a more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents: 31753
diff changeset
   101
      this + elem1 + elem2 ++ elems
31764
e767fee21b22 moved string utilities to completion.scala;
wenzelm
parents: 31762
diff changeset
   102
    def ++ (elems: Iterable[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
e767fee21b22 moved string utilities to completion.scala;
wenzelm
parents: 31762
diff changeset
   103
    def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   104
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   105
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   106
    /* RegexParsers methods */
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   107
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   108
    override val whiteSpace = "".r
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   109
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   110
    type Result = (String, Boolean)
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   111
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   112
    def keyword: Parser[Result] = new Parser[Result]
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   113
    {
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   114
      def apply(in: Input) =
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   115
      {
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   116
        val source = in.source
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   117
        val offset = in.offset
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   118
        val len = source.length - offset
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   119
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   120
        def scan(tree: Tree, result: Result, i: Int): Result =
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   121
        {
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   122
          if (i < len) {
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   123
            tree.branches.get(source.charAt(offset + i)) match {
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   124
              case Some((s, tr)) =>
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   125
                scan(tr, if (s.isEmpty) result else (s, tr.branches.isEmpty), i + 1)
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   126
              case None => result
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   127
            }
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   128
          }
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   129
          else result
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   130
        }
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   131
        val result @ (text, terminated) = scan(main_tree, ("", false), 0)
31650
cfaed41ee2c5 added completions;
wenzelm
parents: 31649
diff changeset
   132
        if (text.isEmpty) Failure("keyword expected", in)
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   133
        else Success(result, in.drop(text.length))
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
   134
      }
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   135
    }.named("keyword")
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
   136
34135
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   137
    def symbol: Parser[String] = new Parser[String]
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   138
    {
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   139
      private val symbol_regex = regex(Symbol.regex)
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   140
      def apply(in: Input) =
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   141
      {
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   142
        val source = in.source
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   143
        val offset = in.offset
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   144
        if (offset >= source.length) Failure("input expected", in)
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   145
        else if (Symbol.could_open(source.charAt(offset))) symbol_regex(in)
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   146
        else Success(source.subSequence(offset, offset + 1).toString, in.drop(1))
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   147
      }
63dd95e3b393 indicate final state of keywords;
wenzelm
parents: 32450
diff changeset
   148
    }.named("symbol")
31649
a11ea667d676 reorganized and abstracted version, via Set trait;
wenzelm
parents: 31648
diff changeset
   149
  }
31648
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
   150
}
31b1f296515b Efficient scanning of literals.
wenzelm
parents:
diff changeset
   151