support ML antiquotations in Scala;
authorwenzelm
Sun Feb 16 15:38:08 2014 +0100 (2014-02-16 ago)
changeset 5551275c68e05f9ea
parent 55511 984e210d412e
child 55513 6d21415e3909
support ML antiquotations in Scala;
tuned -- more uniform ML vs. Scala;
src/Pure/General/antiquote.ML
src/Pure/General/antiquote.scala
src/Pure/Isar/token.scala
src/Pure/ML/ml_lex.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/antiquote.ML	Sun Feb 16 14:18:14 2014 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Sun Feb 16 15:38:08 2014 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4    val reports_of: ('a -> Position.report_text list) ->
     1.5      'a antiquote list -> Position.report_text list
     1.6    val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
     1.7 -  val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
     1.8 +  val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
     1.9    val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
    1.10  end;
    1.11  
    1.12 @@ -48,7 +48,7 @@
    1.13    Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") ||
    1.14      Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.is_regular s)) >> flat;
    1.15  
    1.16 -val scan_ant =
    1.17 +val scan_antiq_body =
    1.18    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
    1.19    Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
    1.20    Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    1.21 @@ -58,10 +58,10 @@
    1.22  val scan_antiq =
    1.23    Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |--
    1.24      Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
    1.25 -      (Scan.repeat scan_ant -- ($$ "}" |-- Symbol_Pos.scan_pos)))
    1.26 +      (Scan.repeat scan_antiq_body -- ($$ "}" |-- Symbol_Pos.scan_pos)))
    1.27    >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
    1.28  
    1.29 -val scan_text = scan_antiq >> Antiq || scan_txt >> Text;
    1.30 +val scan_antiquote = scan_antiq >> Antiq || scan_txt >> Text;
    1.31  
    1.32  end;
    1.33  
    1.34 @@ -69,7 +69,7 @@
    1.35  (* read *)
    1.36  
    1.37  fun read (syms, pos) =
    1.38 -  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
    1.39 +  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
    1.40      SOME xs => (Position.reports_text (reports_of (K []) xs); xs)
    1.41    | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
    1.42  
     2.1 --- a/src/Pure/General/antiquote.scala	Sun Feb 16 14:18:14 2014 +0100
     2.2 +++ b/src/Pure/General/antiquote.scala	Sun Feb 16 15:38:08 2014 +0100
     2.3 @@ -26,13 +26,16 @@
     2.4      private val txt: Parser[String] =
     2.5        rep1("@" ~ guard(one(s => s != "{")) | many1(s => s != "@")) ^^ (x => x.mkString)
     2.6  
     2.7 -    private val ant: Parser[String] =
     2.8 -      quoted("\"") | (quoted("`") | (cartouche | one(s => s != "}")))
     2.9 +    val antiq_other: Parser[String] =
    2.10 +      many1(s => s != "\"" && s != "`" && s != "}" && !Symbol.is_open(s) && !Symbol.is_close(s))
    2.11 +
    2.12 +    private val antiq_body: Parser[String] =
    2.13 +      quoted("\"") | (quoted("`") | (cartouche | antiq_other))
    2.14  
    2.15      val antiq: Parser[String] =
    2.16 -      "@{" ~ rep(ant) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z }
    2.17 +      "@{" ~ rep(antiq_body) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z }
    2.18  
    2.19 -    val text: Parser[Antiquote] =
    2.20 +    val antiquote: Parser[Antiquote] =
    2.21        antiq ^^ (x => Antiq(x)) | txt ^^ (x => Text(x))
    2.22    }
    2.23  
    2.24 @@ -41,7 +44,7 @@
    2.25  
    2.26    def read(input: CharSequence): List[Antiquote] =
    2.27    {
    2.28 -    Parsers.parseAll(Parsers.rep(Parsers.text), new CharSequenceReader(input)) match {
    2.29 +    Parsers.parseAll(Parsers.rep(Parsers.antiquote), new CharSequenceReader(input)) match {
    2.30        case Parsers.Success(xs, _) => xs
    2.31        case Parsers.NoSuccess(_, next) =>
    2.32          error("Malformed quotation/antiquotation source" +
     3.1 --- a/src/Pure/Isar/token.scala	Sun Feb 16 14:18:14 2014 +0100
     3.2 +++ b/src/Pure/Isar/token.scala	Sun Feb 16 15:38:08 2014 +0100
     3.3 @@ -26,7 +26,7 @@
     3.4      val STRING = Value("string")
     3.5      val ALT_STRING = Value("back-quoted string")
     3.6      val VERBATIM = Value("verbatim text")
     3.7 -    val CARTOUCHE = Value("cartouche")
     3.8 +    val CARTOUCHE = Value("text cartouche")
     3.9      val SPACE = Value("white space")
    3.10      val COMMENT = Value("comment text")
    3.11      val ERROR = Value("bad input")
     4.1 --- a/src/Pure/ML/ml_lex.scala	Sun Feb 16 14:18:14 2014 +0100
     4.2 +++ b/src/Pure/ML/ml_lex.scala	Sun Feb 16 15:38:08 2014 +0100
     4.3 @@ -51,6 +51,13 @@
     4.4      val STRING = Value("quoted string")
     4.5      val SPACE = Value("white space")
     4.6      val COMMENT = Value("comment text")
     4.7 +    val ANTIQ = Value("antiquotation")
     4.8 +    val ANTIQ_START = Value("antiquotation: start")
     4.9 +    val ANTIQ_STOP = Value("antiquotation: stop")
    4.10 +    val ANTIQ_OTHER = Value("antiquotation: other")
    4.11 +    val ANTIQ_STRING = Value("antiquotation: quoted string")
    4.12 +    val ANTIQ_ALT_STRING = Value("antiquotation: back-quoted string")
    4.13 +    val ANTIQ_CARTOUCHE = Value("antiquotation: text cartouche")
    4.14      val ERROR = Value("bad input")
    4.15    }
    4.16  
    4.17 @@ -65,8 +72,9 @@
    4.18    /** parsers **/
    4.19  
    4.20    case object ML_String extends Scan.Line_Context
    4.21 +  case class Antiq(ctxt: Scan.Line_Context) extends Scan.Line_Context
    4.22  
    4.23 -  private object Parsers extends Scan.Parsers
    4.24 +  private object Parsers extends Scan.Parsers with Antiquote.Parsers
    4.25    {
    4.26      /* string material */
    4.27  
    4.28 @@ -192,13 +200,41 @@
    4.29  
    4.30        val keyword = literal(lexicon) ^^ (x => Token(Kind.KEYWORD, x))
    4.31  
    4.32 +      val ml_antiq = antiq ^^ (x => Token(Kind.ANTIQ, x))
    4.33 +
    4.34        val bad = one(_ => true) ^^ (x => Token(Kind.ERROR, x))
    4.35  
    4.36 -      space | (recover_delimited |
    4.37 -        (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad))
    4.38 +      space | (recover_delimited | (ml_antiq |
    4.39 +        (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad)))
    4.40      }
    4.41  
    4.42  
    4.43 +    /* antiquotations (line-oriented) */
    4.44 +
    4.45 +    def ml_antiq_start(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
    4.46 +      ctxt match {
    4.47 +        case Scan.Finished => "@{" ^^ (x => (Token(Kind.ANTIQ_START, x), Antiq(Scan.Finished)))
    4.48 +        case _ => failure("")
    4.49 +      }
    4.50 +
    4.51 +    def ml_antiq_stop(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
    4.52 +      ctxt match {
    4.53 +        case Antiq(Scan.Finished) => "}" ^^ (x => (Token(Kind.ANTIQ_STOP, x), Scan.Finished))
    4.54 +        case _ => failure("")
    4.55 +      }
    4.56 +
    4.57 +    def ml_antiq_body(context: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
    4.58 +      context match {
    4.59 +        case Antiq(ctxt) =>
    4.60 +          (if (ctxt == Scan.Finished) antiq_other ^^ (x => (Token(Kind.ANTIQ_OTHER, x), context))
    4.61 +           else failure("")) |
    4.62 +          quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_STRING, x), Antiq(c)) } |
    4.63 +          quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_ALT_STRING, x), Antiq(c)) } |
    4.64 +          cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), Antiq(c)) }
    4.65 +        case _ => failure("")
    4.66 +      }
    4.67 +
    4.68 +
    4.69      /* token */
    4.70  
    4.71      def token: Parser[Token] = delimited_token | other_token
    4.72 @@ -207,7 +243,9 @@
    4.73      {
    4.74        val other = (ml_char | other_token) ^^ (x => (x, Scan.Finished))
    4.75  
    4.76 -      ml_string_line(ctxt) | (ml_comment_line(ctxt) | other)
    4.77 +      ml_string_line(ctxt) |
    4.78 +        (ml_comment_line(ctxt) |
    4.79 +          (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
    4.80      }
    4.81    }
    4.82  
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 16 14:18:14 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Feb 16 15:38:08 2014 +0100
     5.3 @@ -129,6 +129,13 @@
     5.4        ML_Lex.Kind.STRING -> LITERAL1,
     5.5        ML_Lex.Kind.SPACE -> NULL,
     5.6        ML_Lex.Kind.COMMENT -> COMMENT1,
     5.7 +      ML_Lex.Kind.ANTIQ -> NULL,
     5.8 +      ML_Lex.Kind.ANTIQ_START -> LITERAL4,
     5.9 +      ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
    5.10 +      ML_Lex.Kind.ANTIQ_OTHER -> NULL,
    5.11 +      ML_Lex.Kind.ANTIQ_STRING -> LITERAL1,
    5.12 +      ML_Lex.Kind.ANTIQ_ALT_STRING -> LITERAL2,
    5.13 +      ML_Lex.Kind.ANTIQ_CARTOUCHE -> COMMENT4,
    5.14        ML_Lex.Kind.ERROR -> INVALID
    5.15      ).withDefaultValue(NULL)
    5.16    }