--- a/NEWS Mon Dec 08 16:04:50 2014 +0100
+++ b/NEWS Mon Dec 08 22:42:12 2014 +0100
@@ -218,6 +218,9 @@
*** ML ***
+* Cartouches within ML sources are turned into values of type
+Input.source (with formal position information).
+
* Proper context for various elementary tactics: assume_tac,
match_tac, compose_tac, Splitter.split_tac etc. Minor
INCOMPATIBILITY.
--- a/src/HOL/ex/Cartouche_Examples.thy Mon Dec 08 16:04:50 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Mon Dec 08 22:42:12 2014 +0100
@@ -260,4 +260,15 @@
lemma "A \<and> B \<longrightarrow> B \<and> A"
by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+)
+
+subsection \<open>ML syntax: input source\<close>
+
+ML \<open>
+ val s: Input.source = \<open>abc\<close>;
+ writeln ("Look here!" ^ Position.here (Input.pos_of s));
+
+ \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
+ if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());
+\<close>
+
end
--- a/src/Pure/General/antiquote.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/General/antiquote.ML Mon Dec 08 22:42:12 2014 +0100
@@ -8,7 +8,6 @@
sig
type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
datatype 'a antiquote = Text of 'a | Antiq of antiq
- val is_text: 'a antiquote -> bool
val antiq_reports: antiq -> Position.report list
val antiquote_reports: ('a -> Position.report_text list) ->
'a antiquote list -> Position.report_text list
@@ -25,9 +24,6 @@
type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range};
datatype 'a antiquote = Text of 'a | Antiq of antiq;
-fun is_text (Text _) = true
- | is_text _ = false;
-
(* reports *)
--- a/src/Pure/General/symbol_pos.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Mon Dec 08 22:42:12 2014 +0100
@@ -37,7 +37,7 @@
(T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
type text = string
val implode: T list -> text
- val implode_range: Position.T -> Position.T -> T list -> text * Position.range
+ val implode_range: Position.range -> T list -> text * Position.range
val explode: text * Position.T -> T list
val scan_ident: T list -> T list * T list
val is_identifier: string -> bool
@@ -238,7 +238,7 @@
val implode = implode o pad;
-fun implode_range pos1 pos2 syms =
+fun implode_range (pos1, pos2) syms =
let val syms' = (("", pos1) :: syms @ [("", pos2)])
in (implode syms', range syms') end;
--- a/src/Pure/Isar/token.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/Isar/token.ML Mon Dec 08 22:42:12 2014 +0100
@@ -542,7 +542,7 @@
Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot);
fun token_range k (pos1, (ss, pos2)) =
- Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
+ Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot);
fun scan_token keywords = !!! "bad input"
(Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
--- a/src/Pure/ML/ml_antiquotation.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/ML/ml_antiquotation.ML Mon Dec 08 22:42:12 2014 +0100
@@ -6,7 +6,6 @@
signature ML_ANTIQUOTATION =
sig
- val variant: string -> Proof.context -> string * Proof.context
val declaration: binding -> 'a context_parser ->
(Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
theory -> theory
@@ -17,24 +16,6 @@
structure ML_Antiquotation: ML_ANTIQUOTATION =
struct
-(* unique names *)
-
-val init_context = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
-
-structure Names = Proof_Data
-(
- type T = Name.context;
- fun init _ = init_context;
-);
-
-fun variant a ctxt =
- let
- val names = Names.get ctxt;
- val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names;
- val ctxt' = Names.put names' ctxt;
- in (b, ctxt') end;
-
-
(* define antiquotations *)
fun declaration name scan body =
@@ -47,25 +28,15 @@
declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
fun value name scan =
- declaration name scan (fn _ => fn s => fn ctxt =>
- let
- val (a, ctxt') = variant (Binding.name_of name) ctxt;
- val env = "val " ^ a ^ " = " ^ s ^ ";\n";
- val body = "Isabelle." ^ a;
- in (K (env, body), ctxt') end);
+ declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name));
(* basic antiquotations *)
val _ = Theory.setup
(declaration (Binding.make ("here", @{here})) (Scan.succeed ())
- (fn src => fn () => fn ctxt =>
- let
- val (a, ctxt') = variant "position" ctxt;
- val (_, pos) = Token.name_of_src src;
- val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
- val body = "Isabelle." ^ a;
- in (K (env, body), ctxt') end) #>
+ (fn src => fn () =>
+ ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
value (Binding.make ("binding", @{here}))
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
--- a/src/Pure/ML/ml_antiquotations.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Mon Dec 08 22:42:12 2014 +0100
@@ -20,7 +20,7 @@
(fn src => fn output => fn ctxt =>
let
val (_, pos) = Token.name_of_src src;
- val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
+ val (a, ctxt') = ML_Context.variant "output" ctxt;
val env =
"val " ^ a ^ ": string -> unit =\n\
\ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
@@ -30,16 +30,6 @@
in (K (env, body), ctxt') end));
-(* embedded source *)
-
-val _ = Theory.setup
- (ML_Antiquotation.value @{binding source}
- (Scan.lift Args.text_source_position >> (fn source =>
- "Input.source " ^ Bool.toString (Input.is_delimited source) ^ " " ^
- ML_Syntax.print_string (Input.text_of source) ^ " " ^
- ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
-
-
(* formal entities *)
val _ = Theory.setup
--- a/src/Pure/ML/ml_context.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Mon Dec 08 22:42:12 2014 +0100
@@ -13,7 +13,9 @@
val thms: xstring -> thm list
val exec: (unit -> unit) -> Context.generic -> Context.generic
val check_antiquotation: Proof.context -> xstring * Position.T -> string
+ val variant: string -> Proof.context -> string * Proof.context
type decl = Proof.context -> string * string
+ val value_decl: string -> string -> Proof.context -> decl * Proof.context
val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
theory -> theory
val print_antiquotations: Proof.context -> unit
@@ -50,9 +52,38 @@
(** ML antiquotations **)
+(* unique names *)
+
+structure Names = Proof_Data
+(
+ type T = Name.context;
+ val init_names = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
+ fun init _ = init_names;
+);
+
+fun variant a ctxt =
+ let
+ val names = Names.get ctxt;
+ val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names;
+ val ctxt' = Names.put names' ctxt;
+ in (b, ctxt') end;
+
+
+(* decl *)
+
+type decl = Proof.context -> string * string; (*final context -> ML env, ML body*)
+
+fun value_decl a s ctxt =
+ let
+ val (b, ctxt') = variant a ctxt;
+ val env = "val " ^ b ^ " = " ^ s ^ ";\n";
+ val body = "Isabelle." ^ b;
+ fun decl (_: Proof.context) = (env, body);
+ in (decl, ctxt') end;
+
+
(* theory data *)
-type decl = Proof.context -> string * string; (*final context -> ML env, ML body*)
structure Antiquotations = Theory_Data
(
type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table;
@@ -101,6 +132,9 @@
val end_env = ML_Lex.tokenize "end;";
val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
+fun expanding (Antiquote.Text tok) = ML_Lex.is_cartouche tok
+ | expanding (Antiquote.Antiq _) = true;
+
in
fun eval_antiquotes (ants, pos) opt_context =
@@ -112,20 +146,32 @@
val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
val ((ml_env, ml_body), opt_ctxt') =
- if forall Antiquote.is_text ants
+ if forall (not o expanding) ants
then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
else
let
- fun no_decl _ = ([], []);
+ fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
- fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
- | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
+ fun expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
let
val keywords = Thy_Header.get_keywords' ctxt;
val (decl, ctxt') =
apply_antiquotation (Token.read_antiq keywords antiq (ss, #1 range)) ctxt;
- val decl' = decl #> apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
- in (decl', ctxt') end;
+ in (decl #> tokenize range, ctxt') end
+ | 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);
val ctxt =
(case opt_ctxt of
--- a/src/Pure/ML/ml_lex.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Mon Dec 08 22:42:12 2014 +0100
@@ -9,12 +9,14 @@
val keywords: string list
datatype token_kind =
Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
- Space | Comment | Error of string | EOF
+ Space | Cartouche | 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
+ val range_of: token -> Position.range
val pos_of: token -> Position.T
val end_pos_of: token -> Position.T
val kind_of: token -> token_kind
@@ -62,7 +64,7 @@
datatype token_kind =
Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
- Space | Comment | Error of string | EOF;
+ Space | Cartouche | Comment | Error of string | EOF;
datatype token = Token of Position.range * (token_kind * string);
@@ -70,9 +72,10 @@
(* position *)
fun set_range range (Token (_, x)) = Token (range, x);
+fun range_of (Token (range, _)) = range;
-fun pos_of (Token ((pos, _), _)) = pos;
-fun end_pos_of (Token ((_, pos), _)) = pos;
+val pos_of = #1 o range_of;
+val end_pos_of = #2 o range_of;
(* stopper *)
@@ -100,6 +103,9 @@
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;
@@ -121,6 +127,9 @@
Error msg => error msg
| _ => content_of tok);
+
+(* flatten *)
+
fun flatten_content (tok :: (toks as tok' :: _)) =
Symbol.escape (check_content_of tok) ::
(if is_improper tok orelse is_improper tok' then flatten_content toks
@@ -145,6 +154,7 @@
| Char => (Markup.ML_char, "")
| String => (if SML then Markup.SML_string else Markup.ML_string, "")
| Space => (Markup.empty, "")
+ | Cartouche => (Markup.ML_cartouche, "")
| Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
| Error msg => (Markup.bad, msg)
| EOF => (Markup.empty, "");
@@ -284,11 +294,17 @@
scan_ident >> token Ident ||
scan_type_var >> token Type_Var));
-val scan_antiq = Antiquote.scan_antiq >> Antiquote.Antiq || scan_ml >> Antiquote.Text;
+val scan_sml = scan_ml >> Antiquote.Text;
+
+val scan_ml_antiq =
+ Antiquote.scan_antiq >> Antiquote.Antiq ||
+ Symbol_Pos.scan_cartouche err_prefix >> (Antiquote.Text o token Cartouche) ||
+ scan_ml >> Antiquote.Text;
fun recover msg =
(recover_char ||
recover_string ||
+ Symbol_Pos.recover_cartouche ||
Symbol_Pos.recover_comment ||
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
>> (single o token (Error msg));
@@ -307,7 +323,7 @@
val pos2 = Position.advance Symbol.space pos1;
in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
- val scan = if SML then scan_ml >> Antiquote.Text else scan_antiq;
+ val scan = if SML then scan_sml else scan_ml_antiq;
fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok)
| check _ = ();
val input =
--- a/src/Pure/ML/ml_lex.scala Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala Mon Dec 08 22:42:12 2014 +0100
@@ -50,6 +50,7 @@
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 ANTIQ = Value("antiquotation")
val ANTIQ_START = Value("antiquotation: start")
@@ -133,6 +134,15 @@
}
+ /* 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] =
@@ -145,10 +155,11 @@
/* delimited token */
private def delimited_token: Parser[Token] =
- ml_char | (ml_string | ml_comment)
+ ml_char | (ml_string | (ml_cartouche | ml_comment))
private val recover_delimited: Parser[Token] =
- (recover_ml_char | (recover_ml_string | recover_comment)) ^^ (x => Token(Kind.ERROR, x))
+ (recover_ml_char | (recover_ml_string | (recover_cartouche | recover_comment))) ^^
+ (x => Token(Kind.ERROR, x))
private def other_token: Parser[Token] =
@@ -246,8 +257,9 @@
if (SML) ml_string_line(ctxt) | (ml_comment_line(ctxt) | other)
else
ml_string_line(ctxt) |
- (ml_comment_line(ctxt) |
- (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
+ (ml_cartouche_line(ctxt) |
+ (ml_comment_line(ctxt) |
+ (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other)))))
}
}
--- a/src/Pure/ML/ml_thms.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML Mon Dec 08 22:42:12 2014 +0100
@@ -42,16 +42,12 @@
val _ = Theory.setup
(ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse.attribs)
(fn _ => fn raw_srcs => fn ctxt =>
- let
- val i = serial ();
-
- val (a, ctxt') = ctxt
- |> ML_Antiquotation.variant "attributes"
- ||> put_attributes (i, Attrib.check_attribs ctxt raw_srcs);
- val ml =
- ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
- string_of_int i ^ ";\n", "Isabelle." ^ a);
- in (K ml, ctxt') end));
+ let val i = serial () in
+ ctxt
+ |> put_attributes (i, Attrib.check_attribs ctxt raw_srcs)
+ |> ML_Context.value_decl "attributes"
+ ("ML_Thms.the_attributes ML_context " ^ string_of_int i)
+ end));
(* fact references *)
@@ -59,7 +55,7 @@
fun thm_binding kind is_single thms ctxt =
let
val initial = null (get_thmss ctxt);
- val (name, ctxt') = ML_Antiquotation.variant kind ctxt;
+ val (name, ctxt') = ML_Context.variant kind ctxt;
val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
val ml_body = "Isabelle." ^ name;
--- a/src/Pure/PIDE/markup.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Dec 08 22:42:12 2014 +0100
@@ -99,6 +99,7 @@
val ML_numeralN: string val ML_numeral: T
val ML_charN: string val ML_char: T
val ML_stringN: string val ML_string: T
+ val ML_cartoucheN: string val ML_cartouche: T
val ML_commentN: string val ML_comment: T
val SML_stringN: string val SML_string: T
val SML_commentN: string val SML_comment: T
@@ -427,6 +428,7 @@
val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
val (ML_charN, ML_char) = markup_elem "ML_char";
val (ML_stringN, ML_string) = markup_elem "ML_string";
+val (ML_cartoucheN, ML_cartouche) = markup_elem "ML_cartouche";
val (ML_commentN, ML_comment) = markup_elem "ML_comment";
val (SML_stringN, SML_string) = markup_elem "SML_string";
val (SML_commentN, SML_comment) = markup_elem "SML_comment";
--- a/src/Pure/PIDE/markup.scala Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Mon Dec 08 22:42:12 2014 +0100
@@ -241,6 +241,7 @@
val ML_NUMERAL = "ML_numeral"
val ML_CHAR = "ML_char"
val ML_STRING = "ML_string"
+ val ML_CARTOUCHE = "ML_cartouche"
val ML_COMMENT = "ML_comment"
val SML_STRING = "SML_string"
val SML_COMMENT = "SML_comment"
--- a/src/Tools/jEdit/src/rendering.scala Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Mon Dec 08 22:42:12 2014 +0100
@@ -106,6 +106,7 @@
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,
@@ -727,6 +728,7 @@
Markup.ML_NUMERAL -> inner_numeral_color,
Markup.ML_CHAR -> inner_quoted_color,
Markup.ML_STRING -> inner_quoted_color,
+ Markup.ML_CARTOUCHE -> inner_cartouche_color,
Markup.ML_COMMENT -> inner_comment_color,
Markup.SML_STRING -> inner_quoted_color,
Markup.SML_COMMENT -> inner_comment_color)