src/Pure/General/scan.scala
changeset 44570 58bb7ca5c7a2
parent 44569 5130dfe1b7be
child 46123 6de58d947e57
equal deleted inserted replaced
44569:5130dfe1b7be 44570:58bb7ca5c7a2
   159     }.named("keyword")
   159     }.named("keyword")
   160 
   160 
   161 
   161 
   162     /* symbol range */
   162     /* symbol range */
   163 
   163 
   164     def symbol_range(pred: String => Boolean, min_count: Int, max_count: Int): Parser[String] =
   164     def symbol_range(pred: Symbol.Symbol => Boolean, min_count: Int, max_count: Int): Parser[String] =
   165       new Parser[String]
   165       new Parser[String]
   166       {
   166       {
   167         def apply(in: Input) =
   167         def apply(in: Input) =
   168         {
   168         {
   169           val start = in.offset
   169           val start = in.offset
   185           if (count < min_count) Failure("bad input", in)
   185           if (count < min_count) Failure("bad input", in)
   186           else Success(in.source.subSequence(start, i).toString, in.drop(i - start))
   186           else Success(in.source.subSequence(start, i).toString, in.drop(i - start))
   187         }
   187         }
   188       }.named("symbol_range")
   188       }.named("symbol_range")
   189 
   189 
   190     def one(pred: String => Boolean): Parser[String] = symbol_range(pred, 1, 1)
   190     def one(pred: Symbol.Symbol => Boolean): Parser[String] =
   191     def many(pred: String => Boolean): Parser[String] = symbol_range(pred, 0, Integer.MAX_VALUE)
   191       symbol_range(pred, 1, 1)
   192     def many1(pred: String => Boolean): Parser[String] = symbol_range(pred, 1, Integer.MAX_VALUE)
   192 
       
   193     def many(pred: Symbol.Symbol => Boolean): Parser[String] =
       
   194       symbol_range(pred, 0, Integer.MAX_VALUE)
       
   195 
       
   196     def many1(pred: Symbol.Symbol => Boolean): Parser[String] =
       
   197       symbol_range(pred, 1, Integer.MAX_VALUE)
   193 
   198 
   194 
   199 
   195     /* quoted strings */
   200     /* quoted strings */
   196 
   201 
   197     private def quoted_body(quote: String): Parser[String] =
   202     private def quoted_body(quote: Symbol.Symbol): Parser[String] =
   198     {
   203     {
   199       rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" |
   204       rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" |
   200         (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString)
   205         (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString)
   201     }
   206     }
   202 
   207 
   203     private def quoted(quote: String): Parser[String] =
   208     private def quoted(quote: Symbol.Symbol): Parser[String] =
   204     {
   209     {
   205       quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z }
   210       quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z }
   206     }.named("quoted")
   211     }.named("quoted")
   207 
   212 
   208     def quoted_content(quote: String, source: String): String =
   213     def quoted_content(quote: Symbol.Symbol, source: String): String =
   209     {
   214     {
   210       require(parseAll(quoted(quote), source).successful)
   215       require(parseAll(quoted(quote), source).successful)
   211       val body = source.substring(1, source.length - 1)
   216       val body = source.substring(1, source.length - 1)
   212       if (body.exists(_ == '\\')) {
   217       if (body.exists(_ == '\\')) {
   213         val content =
   218         val content =
   216         parseAll(content ^^ (_.mkString), body).get
   221         parseAll(content ^^ (_.mkString), body).get
   217       }
   222       }
   218       else body
   223       else body
   219     }
   224     }
   220 
   225 
   221     def quoted_context(quote: String, ctxt: Context): Parser[(String, Context)] =
   226     def quoted_context(quote: Symbol.Symbol, ctxt: Context): Parser[(String, Context)] =
   222     {
   227     {
   223       ctxt match {
   228       ctxt match {
   224         case Finished =>
   229         case Finished =>
   225           quote ~ quoted_body(quote) ~ opt_term(quote) ^^
   230           quote ~ quoted_body(quote) ~ opt_term(quote) ^^
   226             { case x ~ y ~ Some(z) => (x + y + z, Finished)
   231             { case x ~ y ~ Some(z) => (x + y + z, Finished)