tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
authorwenzelm
Fri Feb 14 15:42:27 2014 +0100 (2014-02-14)
changeset 5549228d4db6c6e79
parent 55491 74db756853d4
child 55493 47cac23e3d22
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
src/Pure/General/scan.scala
src/Pure/Isar/completion.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/token.scala
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/General/scan.scala	Fri Feb 14 14:52:50 2014 +0100
     1.2 +++ b/src/Pure/General/scan.scala	Fri Feb 14 15:42:27 2014 +0100
     1.3 @@ -28,99 +28,12 @@
     1.4  
     1.5  
     1.6  
     1.7 -  /** Lexicon -- position tree **/
     1.8 -
     1.9 -  object Lexicon
    1.10 -  {
    1.11 -    /* representation */
    1.12 -
    1.13 -    sealed case class Tree(val branches: Map[Char, (String, Tree)])
    1.14 -    private val empty_tree = Tree(Map())
    1.15 -
    1.16 -    val empty: Lexicon = new Lexicon(empty_tree)
    1.17 -    def apply(elems: String*): Lexicon = empty ++ elems
    1.18 -  }
    1.19 -
    1.20 -  final class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
    1.21 -  {
    1.22 -    import Lexicon.Tree
    1.23 -
    1.24 -
    1.25 -    /* auxiliary operations */
    1.26 -
    1.27 -    private def content(tree: Tree, result: List[String]): List[String] =
    1.28 -      (result /: tree.branches.toList) ((res, entry) =>
    1.29 -        entry match { case (_, (s, tr)) =>
    1.30 -          if (s.isEmpty) content(tr, res) else content(tr, s :: res) })
    1.31 -
    1.32 -    private def lookup(str: CharSequence): Option[(Boolean, Tree)] =
    1.33 -    {
    1.34 -      val len = str.length
    1.35 -      def look(tree: Tree, tip: Boolean, i: Int): Option[(Boolean, Tree)] =
    1.36 -      {
    1.37 -        if (i < len) {
    1.38 -          tree.branches.get(str.charAt(i)) match {
    1.39 -            case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
    1.40 -            case None => None
    1.41 -          }
    1.42 -        } else Some(tip, tree)
    1.43 -      }
    1.44 -      look(main_tree, false, 0)
    1.45 -    }
    1.46 -
    1.47 -    def completions(str: CharSequence): List[String] =
    1.48 -      lookup(str) match {
    1.49 -        case Some((true, tree)) => content(tree, List(str.toString))
    1.50 -        case Some((false, tree)) => content(tree, Nil)
    1.51 -        case None => Nil
    1.52 -      }
    1.53 +  /** parser combinators **/
    1.54  
    1.55 -
    1.56 -    /* pseudo Set methods */
    1.57 -
    1.58 -    def iterator: Iterator[String] = content(main_tree, Nil).sorted.iterator
    1.59 -
    1.60 -    override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
    1.61 -
    1.62 -    def empty: Lexicon = Lexicon.empty
    1.63 -    def isEmpty: Boolean = main_tree.branches.isEmpty
    1.64 -
    1.65 -    def contains(elem: String): Boolean =
    1.66 -      lookup(elem) match {
    1.67 -        case Some((tip, _)) => tip
    1.68 -        case _ => false
    1.69 -      }
    1.70 -
    1.71 -
    1.72 -    /* add elements */
    1.73 +  object Parsers extends Parsers
    1.74  
    1.75 -    def + (elem: String): Lexicon =
    1.76 -      if (contains(elem)) this
    1.77 -      else {
    1.78 -        val len = elem.length
    1.79 -        def extend(tree: Tree, i: Int): Tree =
    1.80 -          if (i < len) {
    1.81 -            val c = elem.charAt(i)
    1.82 -            val end = (i + 1 == len)
    1.83 -            tree.branches.get(c) match {
    1.84 -              case Some((s, tr)) =>
    1.85 -                Tree(tree.branches +
    1.86 -                  (c -> (if (end) elem else s, extend(tr, i + 1))))
    1.87 -              case None =>
    1.88 -                Tree(tree.branches +
    1.89 -                  (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
    1.90 -            }
    1.91 -          }
    1.92 -          else tree
    1.93 -        new Lexicon(extend(main_tree, 0))
    1.94 -      }
    1.95 -
    1.96 -    def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
    1.97 -
    1.98 -
    1.99 -
   1.100 -    /** RegexParsers methods **/
   1.101 -
   1.102 +  trait Parsers extends RegexParsers
   1.103 +  {
   1.104      override val whiteSpace = "".r
   1.105  
   1.106  
   1.107 @@ -130,33 +43,6 @@
   1.108        p ^^ (x => Some(x)) | """\z""".r ^^ (_ => None)
   1.109  
   1.110  
   1.111 -    /* keywords from lexicon */
   1.112 -
   1.113 -    def keyword: Parser[String] = new Parser[String]
   1.114 -    {
   1.115 -      def apply(in: Input) =
   1.116 -      {
   1.117 -        val source = in.source
   1.118 -        val offset = in.offset
   1.119 -        val len = source.length - offset
   1.120 -
   1.121 -        def scan(tree: Tree, result: String, i: Int): String =
   1.122 -        {
   1.123 -          if (i < len) {
   1.124 -            tree.branches.get(source.charAt(offset + i)) match {
   1.125 -              case Some((s, tr)) => scan(tr, if (s.isEmpty) result else s, i + 1)
   1.126 -              case None => result
   1.127 -            }
   1.128 -          }
   1.129 -          else result
   1.130 -        }
   1.131 -        val result = scan(main_tree, "", 0)
   1.132 -        if (result.isEmpty) Failure("keyword expected", in)
   1.133 -        else Success(result, in.drop(result.length))
   1.134 -      }
   1.135 -    }.named("keyword")
   1.136 -
   1.137 -
   1.138      /* symbol range */
   1.139  
   1.140      def symbol_range(pred: Symbol.Symbol => Boolean, min_count: Int, max_count: Int): Parser[String] =
   1.141 @@ -391,6 +277,19 @@
   1.142      }
   1.143  
   1.144  
   1.145 +    /* keyword */
   1.146 +
   1.147 +    def keyword(lexicon: Lexicon): Parser[String] = new Parser[String]
   1.148 +    {
   1.149 +      def apply(in: Input) =
   1.150 +      {
   1.151 +        val result = lexicon.scan(in)
   1.152 +        if (result.isEmpty) Failure("keyword expected", in)
   1.153 +        else Success(result, in.drop(result.length))
   1.154 +      }
   1.155 +    }.named("keyword")
   1.156 +
   1.157 +
   1.158      /* outer syntax tokens */
   1.159  
   1.160      private def delimited_token: Parser[Token] =
   1.161 @@ -404,7 +303,7 @@
   1.162        string | (alt_string | (verb | (cart | cmt)))
   1.163      }
   1.164  
   1.165 -    private def other_token(is_command: String => Boolean)
   1.166 +    private def other_token(lexicon: Lexicon, is_command: String => Boolean)
   1.167        : Parser[Token] =
   1.168      {
   1.169        val letdigs1 = many1(Symbol.is_letdig)
   1.170 @@ -434,7 +333,8 @@
   1.171          (x => Token(Token.Kind.SYM_IDENT, x))
   1.172  
   1.173        val command_keyword =
   1.174 -        keyword ^^ (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x))
   1.175 +        keyword(lexicon) ^^
   1.176 +          (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x))
   1.177  
   1.178        val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
   1.179  
   1.180 @@ -451,10 +351,11 @@
   1.181            command_keyword) | bad))
   1.182      }
   1.183  
   1.184 -    def token(is_command: String => Boolean): Parser[Token] =
   1.185 -      delimited_token | other_token(is_command)
   1.186 +    def token(lexicon: Lexicon, is_command: String => Boolean): Parser[Token] =
   1.187 +      delimited_token | other_token(lexicon, is_command)
   1.188  
   1.189 -    def token_context(is_command: String => Boolean, ctxt: Context): Parser[(Token, Context)] =
   1.190 +    def token_context(lexicon: Lexicon, is_command: String => Boolean, ctxt: Context)
   1.191 +      : Parser[(Token, Context)] =
   1.192      {
   1.193        val string =
   1.194          quoted_context("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) }
   1.195 @@ -463,9 +364,120 @@
   1.196        val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
   1.197        val cart = cartouche_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) }
   1.198        val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
   1.199 -      val other = other_token(is_command) ^^ { case x => (x, Finished) }
   1.200 +      val other = other_token(lexicon, is_command) ^^ { case x => (x, Finished) }
   1.201  
   1.202        string | (alt_string | (verb | (cart | (cmt | other))))
   1.203      }
   1.204    }
   1.205 +
   1.206 +
   1.207 +
   1.208 +  /** Lexicon -- position tree **/
   1.209 +
   1.210 +  object Lexicon
   1.211 +  {
   1.212 +    /* representation */
   1.213 +
   1.214 +    private sealed case class Tree(val branches: Map[Char, (String, Tree)])
   1.215 +    private val empty_tree = Tree(Map())
   1.216 +
   1.217 +    val empty: Lexicon = new Lexicon(empty_tree)
   1.218 +    def apply(elems: String*): Lexicon = empty ++ elems
   1.219 +  }
   1.220 +
   1.221 +  final class Lexicon private(rep: Lexicon.Tree)
   1.222 +  {
   1.223 +    /* auxiliary operations */
   1.224 +
   1.225 +    private def content(tree: Lexicon.Tree, result: List[String]): List[String] =
   1.226 +      (result /: tree.branches.toList) ((res, entry) =>
   1.227 +        entry match { case (_, (s, tr)) =>
   1.228 +          if (s.isEmpty) content(tr, res) else content(tr, s :: res) })
   1.229 +
   1.230 +    private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
   1.231 +    {
   1.232 +      val len = str.length
   1.233 +      def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
   1.234 +      {
   1.235 +        if (i < len) {
   1.236 +          tree.branches.get(str.charAt(i)) match {
   1.237 +            case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
   1.238 +            case None => None
   1.239 +          }
   1.240 +        } else Some(tip, tree)
   1.241 +      }
   1.242 +      look(rep, false, 0)
   1.243 +    }
   1.244 +
   1.245 +    def completions(str: CharSequence): List[String] =
   1.246 +      lookup(str) match {
   1.247 +        case Some((true, tree)) => content(tree, List(str.toString))
   1.248 +        case Some((false, tree)) => content(tree, Nil)
   1.249 +        case None => Nil
   1.250 +      }
   1.251 +
   1.252 +
   1.253 +    /* pseudo Set methods */
   1.254 +
   1.255 +    def iterator: Iterator[String] = content(rep, Nil).sorted.iterator
   1.256 +
   1.257 +    override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
   1.258 +
   1.259 +    def empty: Lexicon = Lexicon.empty
   1.260 +    def isEmpty: Boolean = rep.branches.isEmpty
   1.261 +
   1.262 +    def contains(elem: String): Boolean =
   1.263 +      lookup(elem) match {
   1.264 +        case Some((tip, _)) => tip
   1.265 +        case _ => false
   1.266 +      }
   1.267 +
   1.268 +
   1.269 +    /* add elements */
   1.270 +
   1.271 +    def + (elem: String): Lexicon =
   1.272 +      if (contains(elem)) this
   1.273 +      else {
   1.274 +        val len = elem.length
   1.275 +        def extend(tree: Lexicon.Tree, i: Int): Lexicon.Tree =
   1.276 +          if (i < len) {
   1.277 +            val c = elem.charAt(i)
   1.278 +            val end = (i + 1 == len)
   1.279 +            tree.branches.get(c) match {
   1.280 +              case Some((s, tr)) =>
   1.281 +                Lexicon.Tree(tree.branches +
   1.282 +                  (c -> (if (end) elem else s, extend(tr, i + 1))))
   1.283 +              case None =>
   1.284 +                Lexicon.Tree(tree.branches +
   1.285 +                  (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
   1.286 +            }
   1.287 +          }
   1.288 +          else tree
   1.289 +        new Lexicon(extend(rep, 0))
   1.290 +      }
   1.291 +
   1.292 +    def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
   1.293 +
   1.294 +
   1.295 +    /* scan */
   1.296 +
   1.297 +    def scan(in: Reader[Char]): String =
   1.298 +    {
   1.299 +      val source = in.source
   1.300 +      val offset = in.offset
   1.301 +      val len = source.length - offset
   1.302 +
   1.303 +      def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String =
   1.304 +      {
   1.305 +        if (i < len) {
   1.306 +          tree.branches.get(source.charAt(offset + i)) match {
   1.307 +            case Some((s, tr)) => scan_tree(tr, if (s.isEmpty) result else s, i + 1)
   1.308 +            case None => result
   1.309 +          }
   1.310 +        }
   1.311 +        else result
   1.312 +      }
   1.313 +      scan_tree(rep, "", 0)
   1.314 +    }
   1.315 +  }
   1.316  }
     2.1 --- a/src/Pure/Isar/completion.scala	Fri Feb 14 14:52:50 2014 +0100
     2.2 +++ b/src/Pure/Isar/completion.scala	Fri Feb 14 15:42:27 2014 +0100
     2.3 @@ -185,8 +185,8 @@
     2.4      line: CharSequence): Option[Completion.Result] =
     2.5    {
     2.6      val raw_result =
     2.7 -      abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
     2.8 -        case abbrevs_lex.Success(reverse_a, _) =>
     2.9 +      Scan.Parsers.parse(Scan.Parsers.keyword(abbrevs_lex), new Library.Reverse(line)) match {
    2.10 +        case Scan.Parsers.Success(reverse_a, _) =>
    2.11            val abbrevs = abbrevs_map.get_list(reverse_a)
    2.12            abbrevs match {
    2.13              case Nil => None
     3.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Feb 14 14:52:50 2014 +0100
     3.2 +++ b/src/Pure/Isar/outer_syntax.scala	Fri Feb 14 15:42:27 2014 +0100
     3.3 @@ -128,10 +128,8 @@
     3.4  
     3.5    def scan(input: Reader[Char]): List[Token] =
     3.6    {
     3.7 -    import lexicon._
     3.8 -
     3.9 -    parseAll(rep(token(is_command)), input) match {
    3.10 -      case Success(tokens, _) => tokens
    3.11 +    Scan.Parsers.parseAll(Scan.Parsers.rep(Scan.Parsers.token(lexicon, is_command)), input) match {
    3.12 +      case Scan.Parsers.Success(tokens, _) => tokens
    3.13        case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
    3.14      }
    3.15    }
    3.16 @@ -141,15 +139,13 @@
    3.17  
    3.18    def scan_context(input: CharSequence, context: Scan.Context): (List[Token], Scan.Context) =
    3.19    {
    3.20 -    import lexicon._
    3.21 -
    3.22      var in: Reader[Char] = new CharSequenceReader(input)
    3.23      val toks = new mutable.ListBuffer[Token]
    3.24      var ctxt = context
    3.25      while (!in.atEnd) {
    3.26 -      parse(token_context(is_command, ctxt), in) match {
    3.27 -        case Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
    3.28 -        case NoSuccess(_, rest) =>
    3.29 +      Scan.Parsers.parse(Scan.Parsers.token_context(lexicon, is_command, ctxt), in) match {
    3.30 +        case Scan.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
    3.31 +        case Scan.Parsers.NoSuccess(_, rest) =>
    3.32            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    3.33        }
    3.34      }
     4.1 --- a/src/Pure/Isar/token.scala	Fri Feb 14 14:52:50 2014 +0100
     4.2 +++ b/src/Pure/Isar/token.scala	Fri Feb 14 15:42:27 2014 +0100
     4.3 @@ -100,11 +100,11 @@
     4.4    def is_end: Boolean = is_keyword && source == "end"
     4.5  
     4.6    def content: String =
     4.7 -    if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
     4.8 -    else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
     4.9 -    else if (kind == Token.Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source)
    4.10 -    else if (kind == Token.Kind.CARTOUCHE) Scan.Lexicon.empty.cartouche_content(source)
    4.11 -    else if (kind == Token.Kind.COMMENT) Scan.Lexicon.empty.comment_content(source)
    4.12 +    if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
    4.13 +    else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source)
    4.14 +    else if (kind == Token.Kind.VERBATIM) Scan.Parsers.verbatim_content(source)
    4.15 +    else if (kind == Token.Kind.CARTOUCHE) Scan.Parsers.cartouche_content(source)
    4.16 +    else if (kind == Token.Kind.COMMENT) Scan.Parsers.comment_content(source)
    4.17      else source
    4.18  
    4.19    def text: (String, String) =
     5.1 --- a/src/Pure/Thy/thy_header.scala	Fri Feb 14 14:52:50 2014 +0100
     5.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Feb 14 15:42:27 2014 +0100
     5.3 @@ -82,13 +82,13 @@
     5.4  
     5.5    def read(reader: Reader[Char]): Thy_Header =
     5.6    {
     5.7 -    val token = lexicon.token(_ => false)
     5.8 +    val token = Scan.Parsers.token(lexicon, _ => false)
     5.9      val toks = new mutable.ListBuffer[Token]
    5.10  
    5.11      @tailrec def scan_to_begin(in: Reader[Char])
    5.12      {
    5.13        token(in) match {
    5.14 -        case lexicon.Success(tok, rest) =>
    5.15 +        case Scan.Parsers.Success(tok, rest) =>
    5.16            toks += tok
    5.17            if (!tok.is_begin) scan_to_begin(rest)
    5.18          case _ =>