--- 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}
--- 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
--- 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;
-
--- 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)
}
}
-
--- 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,