src/Pure/General/scan.scala
changeset 46627 fbe2cb05bdb3
parent 45900 793bf5fa5fbf
child 46712 8650d9a95736
equal deleted inserted replaced
46626:a02115865bcc 46627:fbe2cb05bdb3
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 
    10 import scala.collection.generic.Addable
    10 import scala.collection.{IndexedSeq, TraversableOnce}
    11 import scala.collection.IndexedSeq
       
    12 import scala.collection.immutable.PagedSeq
    11 import scala.collection.immutable.PagedSeq
    13 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
    12 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
    14 import scala.util.parsing.combinator.RegexParsers
    13 import scala.util.parsing.combinator.RegexParsers
    15 
    14 
    16 import java.io.{File, InputStream, BufferedInputStream, FileInputStream}
    15 import java.io.{File, InputStream, BufferedInputStream, FileInputStream}
    39 
    38 
    40     val empty: Lexicon = new Lexicon(empty_tree)
    39     val empty: Lexicon = new Lexicon(empty_tree)
    41     def apply(elems: String*): Lexicon = empty ++ elems
    40     def apply(elems: String*): Lexicon = empty ++ elems
    42   }
    41   }
    43 
    42 
    44   class Lexicon private(private val main_tree: Lexicon.Tree)
    43   class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
    45     extends Addable[String, Lexicon] with RegexParsers
       
    46   {
    44   {
    47     import Lexicon.Tree
    45     import Lexicon.Tree
    48 
    46 
    49 
    47 
    50     /* auxiliary operations */
    48     /* auxiliary operations */
    91         case Some((tip, _)) => tip
    89         case Some((tip, _)) => tip
    92         case _ => false
    90         case _ => false
    93       }
    91       }
    94 
    92 
    95 
    93 
    96     /* Addable methods */
    94     /* add elements */
    97 
       
    98     def repr = this
       
    99 
    95 
   100     def + (elem: String): Lexicon =
    96     def + (elem: String): Lexicon =
   101       if (contains(elem)) this
    97       if (contains(elem)) this
   102       else {
    98       else {
   103         val len = elem.length
    99         val len = elem.length
   113                 Tree(tree.branches +
   109                 Tree(tree.branches +
   114                   (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
   110                   (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
   115             }
   111             }
   116           }
   112           }
   117           else tree
   113           else tree
   118         val old = this
   114         new Lexicon(extend(main_tree, 0))
   119         new Lexicon(extend(old.main_tree, 0))
   115       }
   120       }
   116 
       
   117     def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
   121 
   118 
   122 
   119 
   123 
   120 
   124     /** RegexParsers methods **/
   121     /** RegexParsers methods **/
   125 
   122