# HG changeset patch # User wenzelm # Date 1446852522 -3600 # Node ID 8323b8e21fe9a1a6d09ccacac23da64d6b26eb39 # Parent 3591274c607eaded1468a06c960668573418883c ML cartouches via control antiquotation; diff -r 3591274c607e -r 8323b8e21fe9 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Fri Nov 06 23:31:50 2015 +0100 +++ b/src/Pure/ML/ml_antiquotations.ML Sat Nov 07 00:28:42 2015 +0100 @@ -10,7 +10,13 @@ (* ML support *) val _ = Theory.setup - (ML_Antiquotation.inline @{binding assert} + (ML_Antiquotation.value @{binding cartouche} + (Args.context -- Scan.lift (Parse.position Args.cartouche_input) >> (fn (ctxt, (source, pos)) => + (Context_Position.report ctxt pos Markup.ML_cartouche; + "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^ + ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source))))) #> + + ML_Antiquotation.inline @{binding assert} (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> ML_Antiquotation.inline @{binding make_string} diff -r 3591274c607e -r 8323b8e21fe9 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Fri Nov 06 23:31:50 2015 +0100 +++ b/src/Pure/ML/ml_context.ML Sat Nov 07 00:28:42 2015 +0100 @@ -132,10 +132,6 @@ fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end"); -fun expanding (Antiquote.Text tok) = ML_Lex.is_cartouche tok - | expanding (Antiquote.Control _) = true - | expanding (Antiquote.Antiq _) = true; - fun eval_antiquotes (ants, pos) opt_context = let val visible = @@ -145,7 +141,7 @@ val opt_ctxt = Option.map Context.proof_of opt_context; val ((ml_env, ml_body), opt_ctxt') = - if forall (not o expanding) ants + if forall (fn Antiquote.Text _ => true | _ => false) ants then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt) else let @@ -155,20 +151,7 @@ let val (decl, ctxt') = apply_antiquotation src ctxt in (decl #> tokenize range, ctxt') end; - fun expand (Antiquote.Text tok) ctxt = - if ML_Lex.is_cartouche tok then - let - val range = ML_Lex.range_of tok; - val text = - Symbol_Pos.explode (ML_Lex.content_of tok, #1 range) - |> Symbol_Pos.cartouche_content - |> Symbol_Pos.implode_range range |> #1; - val (decl, ctxt') = - value_decl "input" - ("Input.source true " ^ ML_Syntax.print_string text ^ " " ^ - ML_Syntax.atomic (ML_Syntax.print_range range)) ctxt; - in (decl #> tokenize range, ctxt') end - else (K ([], [tok]), ctxt) + fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt) | expand (Antiquote.Control {name, range, body}) ctxt = expand_src range (Token.src name (if null body then [] else [Token.read_cartouche body])) ctxt diff -r 3591274c607e -r 8323b8e21fe9 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Fri Nov 06 23:31:50 2015 +0100 +++ b/src/Pure/ML/ml_lex.ML Sat Nov 07 00:28:42 2015 +0100 @@ -9,10 +9,9 @@ val keywords: string list datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | - Space | Cartouche | Comment | Error of string | EOF + Space | Comment | Error of string | EOF eqtype token val stopper: token Scan.stopper - val is_cartouche: token -> bool val is_regular: token -> bool val is_improper: token -> bool val set_range: Position.range -> token -> token @@ -64,7 +63,7 @@ datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | - Space | Cartouche | Comment | Error of string | EOF; + Space | Comment | Error of string | EOF; datatype token = Token of Position.range * (token_kind * string); @@ -103,9 +102,6 @@ fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x) | is_delimiter _ = false; -fun is_cartouche (Token (_, (Cartouche, _))) = true - | is_cartouche _ = false; - fun is_regular (Token (_, (Error _, _))) = false | is_regular (Token (_, (EOF, _))) = false | is_regular _ = true; @@ -150,7 +146,6 @@ | Real => (Markup.ML_numeral, "") | Char => (Markup.ML_char, "") | String => (if SML then Markup.SML_string else Markup.ML_string, "") - | Cartouche => (Markup.ML_cartouche, "") | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "") | Error msg => (Markup.bad, msg) | _ => (Markup.empty, ""); @@ -293,7 +288,6 @@ val scan_sml = scan_ml >> Antiquote.Text; val scan_ml_antiq = - Symbol_Pos.scan_cartouche err_prefix >> (Antiquote.Text o token Cartouche) || Antiquote.scan_control >> Antiquote.Control || Antiquote.scan_antiq >> Antiquote.Antiq || scan_ml >> Antiquote.Text; @@ -363,4 +357,3 @@ end; end; - diff -r 3591274c607e -r 8323b8e21fe9 src/Pure/ML/ml_lex.scala --- a/src/Pure/ML/ml_lex.scala Fri Nov 06 23:31:50 2015 +0100 +++ b/src/Pure/ML/ml_lex.scala Sat Nov 07 00:28:42 2015 +0100 @@ -50,7 +50,6 @@ val CHAR = Value("character") val STRING = Value("quoted string") val SPACE = Value("white space") - val CARTOUCHE = Value("text cartouche") val COMMENT = Value("comment text") val CONTROL = Value("control symbol antiquotation") val ANTIQ = Value("antiquotation") @@ -135,15 +134,6 @@ } - /* ML cartouche */ - - private val ml_cartouche: Parser[Token] = - cartouche ^^ (x => Token(Kind.CARTOUCHE, x)) - - private def ml_cartouche_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = - cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.CARTOUCHE, x), c) } - - /* ML comment */ private val ml_comment: Parser[Token] = @@ -156,7 +146,7 @@ /* delimited token */ private def delimited_token: Parser[Token] = - ml_char | (ml_string | (ml_cartouche | ml_comment)) + ml_char | (ml_string | ml_comment) private val recover_delimited: Parser[Token] = (recover_ml_char | (recover_ml_string | (recover_cartouche | recover_comment))) ^^ @@ -217,7 +207,7 @@ val bad = one(_ => true) ^^ (x => Token(Kind.ERROR, x)) - space | (recover_delimited | (ml_control | (ml_antiq | + space | (ml_control | (recover_delimited | (ml_antiq | (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad)))) } @@ -259,9 +249,8 @@ if (SML) ml_string_line(ctxt) | (ml_comment_line(ctxt) | other) else ml_string_line(ctxt) | - (ml_cartouche_line(ctxt) | - (ml_comment_line(ctxt) | - (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))) + (ml_comment_line(ctxt) | + (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other)))) } } @@ -292,4 +281,3 @@ (toks.toList, ctxt) } } - diff -r 3591274c607e -r 8323b8e21fe9 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Fri Nov 06 23:31:50 2015 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Sat Nov 07 00:28:42 2015 +0100 @@ -115,7 +115,6 @@ ML_Lex.Kind.CHAR -> LITERAL2, ML_Lex.Kind.STRING -> LITERAL1, ML_Lex.Kind.SPACE -> NULL, - ML_Lex.Kind.CARTOUCHE -> COMMENT4, ML_Lex.Kind.COMMENT -> COMMENT1, ML_Lex.Kind.ANTIQ -> NULL, ML_Lex.Kind.ANTIQ_START -> LITERAL4,