--- a/NEWS Thu Jan 03 22:30:41 2019 +0100
+++ b/NEWS Fri Jan 04 21:49:06 2019 +0100
@@ -171,6 +171,10 @@
section "Theory update". Theory sessions are specified as in "isabelle
dump".
+* The command-line tool "isabelle update -u control_cartouches" changes
+antiquotations into control-symbol format (where possible): @{NAME}
+becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\<open>ARG\<close>.
+
* Support for Isabelle command-line tools defined in Isabelle/Scala.
Instances of class Isabelle_Scala_Tools may be configured via the shell
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
--- a/etc/options Thu Jan 03 22:30:41 2019 +0100
+++ b/etc/options Fri Jan 04 21:49:06 2019 +0100
@@ -285,6 +285,9 @@
option update_mixfix_cartouches : bool = false
-- "update mixfix templates to use cartouches instead of double quotes"
+option update_control_cartouches : bool = false
+ -- "update antiquotations to use control symbol with cartouche argument"
+
section "Build Database"
--- a/src/HOL/Library/LaTeXsugar.thy Thu Jan 03 22:30:41 2019 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Fri Jan 04 21:49:06 2019 +0100
@@ -97,7 +97,8 @@
"_asm" :: "prop \<Rightarrow> asms" ("_")
setup \<open>
- Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
+ Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>const_typ\<close>
+ (Scan.lift Args.embedded_inner_syntax)
(fn ctxt => fn c =>
let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jan 04 21:49:06 2019 +0100
@@ -983,7 +983,8 @@
end;
fun fp_antiquote_setup binding =
- Thy_Output.antiquotation_pretty_source binding (Args.type_name {proper = true, strict = true})
+ Thy_Output.antiquotation_pretty_source_embedded binding
+ (Args.type_name {proper = true, strict = true})
(fn ctxt => fn fcT_name =>
(case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
--- a/src/HOL/Tools/value_command.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/HOL/Tools/value_command.ML Fri Jan 04 21:49:06 2019 +0100
@@ -73,7 +73,7 @@
>> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t)));
val _ = Theory.setup
- (Thy_Output.antiquotation_pretty_source \<^binding>\<open>value\<close>
+ (Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value\<close>
(Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
(fn ctxt => fn ((name, style), t) =>
Thy_Output.pretty_term ctxt (style (value_select name ctxt t)))
--- a/src/Pure/General/antiquote.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/General/antiquote.ML Fri Jan 04 21:49:06 2019 +0100
@@ -14,6 +14,7 @@
val text_range: text_antiquote list -> Position.range
val split_lines: text_antiquote list -> text_antiquote list list
val antiq_reports: 'a antiquote list -> Position.report list
+ val update_reports: bool -> Position.T -> string list -> Position.report_text list
val scan_control: control scanner
val scan_antiq: antiq scanner
val scan_antiquote: text_antiquote scanner
@@ -71,6 +72,30 @@
(pos, Markup.language_antiquotation)]);
+(* update *)
+
+fun update_reports embedded pos src =
+ let
+ val n = length src;
+ val no_arg = n = 1;
+ val embedded_arg = n = 2 andalso embedded;
+ val control =
+ (case src of
+ name :: _ =>
+ if Symbol.is_ascii_identifier name andalso name <> "cartouche" andalso
+ (no_arg orelse embedded_arg)
+ then SOME (Symbol.control_prefix ^ name ^ Symbol.control_suffix)
+ else NONE
+ | [] => NONE);
+ val arg = if embedded_arg then cartouche (nth src 1) else "";
+ in
+ (case control of
+ SOME sym => [((pos, Markup.update), sym ^ arg)]
+ | NONE => [])
+ end;
+
+
+
(* scan *)
open Basic_Symbol_Pos;
--- a/src/Pure/General/symbol.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/General/symbol.ML Fri Jan 04 21:49:06 2019 +0100
@@ -23,6 +23,8 @@
val is_symbolic: symbol -> bool
val is_symbolic_char: symbol -> bool
val is_printable: symbol -> bool
+ val control_prefix: string
+ val control_suffix: string
val is_control: symbol -> bool
val eof: symbol
val is_eof: symbol -> bool
@@ -135,8 +137,11 @@
if is_char s then 32 <= ord s andalso ord s <= Char.ord #"~"
else is_utf8 s orelse raw_symbolic s;
+val control_prefix = "\092<^";
+val control_suffix = ">";
+
fun is_control s =
- String.isPrefix "\092<^" s andalso String.isSuffix ">" s;
+ String.isPrefix control_prefix s andalso String.isSuffix control_suffix s;
(* input source control *)
--- a/src/Pure/ML/ml_antiquotation.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/ML/ml_antiquotation.ML Fri Jan 04 21:49:06 2019 +0100
@@ -9,8 +9,13 @@
val declaration: binding -> 'a context_parser ->
(Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
theory -> theory
+ val declaration_embedded: binding -> 'a context_parser ->
+ (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
+ theory -> theory
val inline: binding -> string context_parser -> theory -> theory
+ val inline_embedded: binding -> string context_parser -> theory -> theory
val value: binding -> string context_parser -> theory -> theory
+ val value_embedded: binding -> string context_parser -> theory -> theory
end;
structure ML_Antiquotation: ML_ANTIQUOTATION =
@@ -18,17 +23,32 @@
(* define antiquotations *)
-fun declaration name scan body =
- ML_Context.add_antiquotation name
+local
+
+fun gen_declaration name embedded scan body =
+ ML_Context.add_antiquotation name embedded
(fn src => fn orig_ctxt =>
let val (x, _) = Token.syntax scan src orig_ctxt
in body src x orig_ctxt end);
-fun inline name scan =
- declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
+fun gen_inline name embedded scan =
+ gen_declaration name embedded scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
+
+fun gen_value name embedded scan =
+ gen_declaration name embedded scan (fn _ => ML_Context.value_decl (Binding.name_of name));
+
+in
-fun value name scan =
- declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name));
+fun declaration name = gen_declaration name false;
+fun declaration_embedded name = gen_declaration name true;
+
+fun inline name = gen_inline name false;
+fun inline_embedded name = gen_inline name true;
+
+fun value name = gen_value name false;
+fun value_embedded name = gen_value name true;
+
+end;
(* basic antiquotations *)
@@ -40,15 +60,15 @@
inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
- value (Binding.make ("binding", \<^here>))
+ value_embedded (Binding.make ("binding", \<^here>))
(Scan.lift (Parse.input Args.embedded) >> (ML_Syntax.make_binding o Input.source_content)) #>
- value (Binding.make ("cartouche", \<^here>))
+ value_embedded (Binding.make ("cartouche", \<^here>))
(Scan.lift Args.cartouche_input >> (fn source =>
"Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
- inline (Binding.make ("verbatim", \<^here>))
+ inline_embedded (Binding.make ("verbatim", \<^here>))
(Scan.lift Args.embedded >> ML_Syntax.print_string));
end;
--- a/src/Pure/ML/ml_antiquotations.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Fri Jan 04 21:49:06 2019 +0100
@@ -16,7 +16,7 @@
ML_Antiquotation.inline \<^binding>\<open>assert\<close>
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
- ML_Antiquotation.declaration \<^binding>\<open>print\<close>
+ ML_Antiquotation.declaration_embedded \<^binding>\<open>print\<close>
(Scan.lift (Scan.optional Args.embedded "Output.writeln"))
(fn src => fn output => fn ctxt =>
let
@@ -40,18 +40,18 @@
(* formal entities *)
val _ = Theory.setup
- (ML_Antiquotation.value \<^binding>\<open>system_option\<close>
+ (ML_Antiquotation.value_embedded \<^binding>\<open>system_option\<close>
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
(Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #>
- ML_Antiquotation.value \<^binding>\<open>theory\<close>
+ ML_Antiquotation.value_embedded \<^binding>\<open>theory\<close>
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
(Theory.check {long = false} ctxt (name, pos);
"Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))
|| Scan.succeed "Proof_Context.theory_of ML_context") #>
- ML_Antiquotation.value \<^binding>\<open>theory_context\<close>
+ ML_Antiquotation.value_embedded \<^binding>\<open>theory_context\<close>
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
(Theory.check {long = false} ctxt (name, pos);
"Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
@@ -60,20 +60,25 @@
ML_Antiquotation.inline \<^binding>\<open>context\<close>
(Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #>
- ML_Antiquotation.inline \<^binding>\<open>typ\<close> (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
- ML_Antiquotation.inline \<^binding>\<open>term\<close> (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
- ML_Antiquotation.inline \<^binding>\<open>prop\<close> (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>typ\<close>
+ (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
- ML_Antiquotation.value \<^binding>\<open>ctyp\<close> (Args.typ >> (fn T =>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>term\<close>
+ (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
+
+ ML_Antiquotation.inline_embedded \<^binding>\<open>prop\<close>
+ (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
+
+ ML_Antiquotation.value_embedded \<^binding>\<open>ctyp\<close> (Args.typ >> (fn T =>
"Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
- ML_Antiquotation.value \<^binding>\<open>cterm\<close> (Args.term >> (fn t =>
+ ML_Antiquotation.value_embedded \<^binding>\<open>cterm\<close> (Args.term >> (fn t =>
"Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
- ML_Antiquotation.value \<^binding>\<open>cprop\<close> (Args.prop >> (fn t =>
+ ML_Antiquotation.value_embedded \<^binding>\<open>cprop\<close> (Args.prop >> (fn t =>
"Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
- ML_Antiquotation.inline \<^binding>\<open>method\<close>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>method\<close>
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
@@ -81,7 +86,7 @@
(* locales *)
val _ = Theory.setup
- (ML_Antiquotation.inline \<^binding>\<open>locale\<close>
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close>
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
Locale.check (Proof_Context.theory_of ctxt) (name, pos)
|> ML_Syntax.print_string)));
@@ -95,10 +100,10 @@
|> ML_Syntax.print_string);
val _ = Theory.setup
- (ML_Antiquotation.inline \<^binding>\<open>class\<close> (class false) #>
- ML_Antiquotation.inline \<^binding>\<open>class_syntax\<close> (class true) #>
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>class\<close> (class false) #>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>class_syntax\<close> (class true) #>
- ML_Antiquotation.inline \<^binding>\<open>sort\<close>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>sort\<close>
(Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
@@ -119,13 +124,13 @@
in ML_Syntax.print_string res end);
val _ = Theory.setup
- (ML_Antiquotation.inline \<^binding>\<open>type_name\<close>
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>type_name\<close>
(type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
- ML_Antiquotation.inline \<^binding>\<open>type_abbrev\<close>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>type_abbrev\<close>
(type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
- ML_Antiquotation.inline \<^binding>\<open>nonterminal\<close>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>nonterminal\<close>
(type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
- ML_Antiquotation.inline \<^binding>\<open>type_syntax\<close>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>type_syntax\<close>
(type_name "type" (fn (c, _) => Lexicon.mark_type c)));
@@ -142,14 +147,14 @@
in ML_Syntax.print_string res end);
val _ = Theory.setup
- (ML_Antiquotation.inline \<^binding>\<open>const_name\<close>
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>const_name\<close>
(const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
- ML_Antiquotation.inline \<^binding>\<open>const_abbrev\<close>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>const_abbrev\<close>
(const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
- ML_Antiquotation.inline \<^binding>\<open>const_syntax\<close>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>const_syntax\<close>
(const_name (fn (_, c) => Lexicon.mark_const c)) #>
- ML_Antiquotation.inline \<^binding>\<open>syntax_const\<close>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close>
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (c, pos)) =>
if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
then ML_Syntax.print_string c
@@ -252,7 +257,7 @@
(* outer syntax *)
val _ = Theory.setup
- (ML_Antiquotation.value \<^binding>\<open>keyword\<close>
+ (ML_Antiquotation.value_embedded \<^binding>\<open>keyword\<close>
(Args.context --
Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true)))
>> (fn (ctxt, (name, pos)) =>
@@ -260,7 +265,7 @@
(Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
"Parse.$$$ " ^ ML_Syntax.print_string name)
else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
- ML_Antiquotation.value \<^binding>\<open>command_keyword\<close>
+ ML_Antiquotation.value_embedded \<^binding>\<open>command_keyword\<close>
(Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
(case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
SOME markup =>
--- a/src/Pure/ML/ml_context.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/ML/ml_context.ML Fri Jan 04 21:49:06 2019 +0100
@@ -11,7 +11,7 @@
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) ->
+ val add_antiquotation: binding -> bool -> (Token.src -> Proof.context -> decl * Proof.context) ->
theory -> theory
val print_antiquotations: bool -> Proof.context -> unit
val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
@@ -67,7 +67,7 @@
structure Antiquotations = Theory_Data
(
- type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table;
+ type T = (bool * (Token.src -> Proof.context -> decl * Proof.context)) Name_Space.table;
val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
val extend = I;
fun merge data : T = Name_Space.merge_tables data;
@@ -78,17 +78,23 @@
fun check_antiquotation ctxt =
#1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt);
-fun add_antiquotation name f thy = thy
- |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
+fun add_antiquotation name embedded scan thy = thy
+ |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, (embedded, scan)) #> snd);
fun print_antiquotations verbose ctxt =
Pretty.big_list "ML antiquotations:"
(map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt)))
|> Pretty.writeln;
-fun apply_antiquotation src ctxt =
- let val (src', f) = Token.check_src ctxt get_antiquotations src
- in f src' ctxt end;
+fun apply_antiquotation pos src ctxt =
+ let
+ val (src', (embedded, scan)) = Token.check_src ctxt get_antiquotations src;
+ val _ =
+ if Options.default_bool "update_control_cartouches" then
+ Context_Position.reports_text ctxt
+ (Antiquote.update_reports embedded pos (map Token.content_of src'))
+ else ();
+ in scan src' ctxt end;
(* parsing and evaluation *)
@@ -123,7 +129,7 @@
fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
fun expand_src range src ctxt =
- let val (decl, ctxt') = apply_antiquotation src ctxt
+ let val (decl, ctxt') = apply_antiquotation (#1 range) src ctxt;
in (decl #> tokenize range, ctxt') end;
fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
--- a/src/Pure/PIDE/resources.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/PIDE/resources.ML Fri Jan 04 21:49:06 2019 +0100
@@ -277,16 +277,16 @@
in
val _ = Theory.setup
- (Thy_Output.antiquotation_verbatim \<^binding>\<open>session\<close>
+ (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>session\<close>
(Scan.lift Parse.embedded_position) check_session #>
- Thy_Output.antiquotation_verbatim \<^binding>\<open>doc\<close>
+ Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>doc\<close>
(Scan.lift Parse.embedded_position) check_doc #>
- Thy_Output.antiquotation_raw \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
- Thy_Output.antiquotation_raw \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
- Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
- ML_Antiquotation.value \<^binding>\<open>path\<close> (ML_antiq check_path) #>
- ML_Antiquotation.value \<^binding>\<open>file\<close> (ML_antiq check_file) #>
- ML_Antiquotation.value \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
+ Thy_Output.antiquotation_raw_embedded \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
+ Thy_Output.antiquotation_raw_embedded \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
+ Thy_Output.antiquotation_raw_embedded \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
+ ML_Antiquotation.value_embedded \<^binding>\<open>path\<close> (ML_antiq check_path) #>
+ ML_Antiquotation.value_embedded \<^binding>\<open>file\<close> (ML_antiq check_file) #>
+ ML_Antiquotation.value_embedded \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
ML_Antiquotation.value \<^binding>\<open>master_dir\<close>
(Args.theory >> (ML_Syntax.print_path o master_directory)));
--- a/src/Pure/Thy/document_antiquotation.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Thy/document_antiquotation.ML Fri Jan 04 21:49:06 2019 +0100
@@ -26,6 +26,8 @@
val check_option: Proof.context -> xstring * Position.T -> string
val setup: binding -> 'a context_parser ->
({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
+ val setup_embedded: binding -> 'a context_parser ->
+ ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
val boolean: string -> bool
val integer: string -> int
@@ -86,7 +88,7 @@
structure Data = Theory_Data
(
type T =
- (Token.src -> Proof.context -> Latex.text) Name_Space.table *
+ (bool * (Token.src -> Proof.context -> Latex.text)) Name_Space.table *
(string -> Proof.context -> Proof.context) Name_Space.table;
val empty : T =
(Name_Space.empty_table Markup.document_antiquotationN,
@@ -112,12 +114,16 @@
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
-fun setup name scan body thy =
+fun gen_setup name embedded scan body thy =
let
fun cmd src ctxt =
let val (x, ctxt') = Token.syntax scan src ctxt
in body {context = ctxt', source = src, argument = x} end;
- in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> #2)) end;
+ val entry = (name, (embedded, cmd));
+ in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true entry #> #2)) end;
+
+fun setup name = gen_setup name false;
+fun setup_embedded name = gen_setup name true;
fun setup_option name opt thy = thy
|> Data.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> #2));
@@ -138,7 +144,7 @@
val parse_antiq =
Parse.!!!
(Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
- >> (fn ((name, props), args) => (props, name :: args));
+ >> (fn ((name, opts), args) => (opts, name :: args));
end;
@@ -147,9 +153,15 @@
local
-fun command src ctxt =
- let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
- in f src' ctxt end;
+fun command pos (opts, src) ctxt =
+ let
+ val (src', (embedded, scan)) = Token.check_src ctxt (#1 o get_antiquotations) src;
+ val _ =
+ if null opts andalso Options.default_bool "update_control_cartouches" then
+ Context_Position.reports_text ctxt
+ (Antiquote.update_reports embedded pos (map Token.content_of src'))
+ else ();
+ in scan src' ctxt end;
fun option ((xname, pos), s) ctxt =
let
@@ -157,14 +169,14 @@
Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
in opt s ctxt end;
-fun eval ctxt (opts, src) =
+fun eval ctxt pos (opts, src) =
let
val preview_ctxt = fold option opts (Config.put show_markup false ctxt);
- val _ = command src preview_ctxt;
+ val _ = command pos (opts, src) preview_ctxt;
val print_ctxt = Context_Position.set_visible false preview_ctxt;
val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN];
- in [Print_Mode.with_modes print_modes (fn () => command src print_ctxt) ()] end;
+ in [Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) ()] end;
in
@@ -172,10 +184,11 @@
(case antiq of
Antiquote.Text ss => eval_text ss
| Antiquote.Control {name, body, ...} =>
- eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
+ eval ctxt Position.none
+ ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
| Antiquote.Antiq {range = (pos, _), body, ...} =>
let val keywords = Thy_Header.get_keywords' ctxt;
- in eval ctxt (Token.read_antiq keywords parse_antiq (body, pos)) end);
+ in eval ctxt pos (Token.read_antiq keywords parse_antiq (body, pos)) end);
end;
--- a/src/Pure/Thy/document_antiquotations.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Jan 04 21:49:06 2019 +0100
@@ -62,7 +62,7 @@
fun pretty_theory ctxt (name, pos) =
(Theory.check {long = true} ctxt (name, pos); Pretty.str name);
-val basic_entity = Thy_Output.antiquotation_pretty_source;
+val basic_entity = Thy_Output.antiquotation_pretty_source_embedded;
fun basic_entities name scan pretty =
Document_Antiquotation.setup name scan
@@ -132,7 +132,7 @@
local
fun control_antiquotation name s1 s2 =
- Thy_Output.antiquotation_raw name (Scan.lift Args.cartouche_input)
+ Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
(fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false});
in
@@ -158,7 +158,7 @@
Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
fun text_antiquotation name =
- Thy_Output.antiquotation_raw name (Scan.lift Args.text_input)
+ Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
(fn ctxt => fn text =>
let
val _ = report_text ctxt text;
@@ -169,7 +169,7 @@
end);
val theory_text_antiquotation =
- Thy_Output.antiquotation_raw \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
+ Thy_Output.antiquotation_raw_embedded \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
(fn ctxt => fn text =>
let
val keywords = Thy_Header.get_keywords' ctxt;
@@ -243,7 +243,7 @@
(* verbatim text *)
val _ = Theory.setup
- (Thy_Output.antiquotation_verbatim \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
+ (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
(fn ctxt => fn text =>
let
val _ =
@@ -257,7 +257,7 @@
local
fun ml_text name ml =
- Thy_Output.antiquotation_verbatim name (Scan.lift Args.text_input)
+ Thy_Output.antiquotation_verbatim_embedded name (Scan.lift Args.text_input)
(fn ctxt => fn text =>
let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text)
in #1 (Input.source_content text) end);
@@ -287,7 +287,7 @@
(* URLs *)
val _ = Theory.setup
- (Thy_Output.antiquotation_raw \<^binding>\<open>url\<close> (Scan.lift Args.embedded_position)
+ (Thy_Output.antiquotation_raw_embedded \<^binding>\<open>url\<close> (Scan.lift Args.embedded_position)
(fn ctxt => fn (url, pos) =>
let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)]
in Latex.enclose_block "\\url{" "}" [Latex.string url] end));
--- a/src/Pure/Thy/thy_output.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Thy/thy_output.ML Fri Jan 04 21:49:06 2019 +0100
@@ -27,12 +27,20 @@
val pretty_items_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
val antiquotation_pretty:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
+ val antiquotation_pretty_embedded:
+ binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_pretty_source:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
+ val antiquotation_pretty_source_embedded:
+ binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_raw:
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
+ val antiquotation_raw_embedded:
+ binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
val antiquotation_verbatim:
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
+ val antiquotation_verbatim_embedded:
+ binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
end;
structure Thy_Output: THY_OUTPUT =
@@ -525,19 +533,40 @@
(* antiquotation variants *)
-fun antiquotation_pretty name scan f =
- Document_Antiquotation.setup name scan
- (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
+local
-fun antiquotation_pretty_source name scan f =
- Document_Antiquotation.setup name scan
+fun gen_setup name embedded =
+ if embedded
+ then Document_Antiquotation.setup_embedded name
+ else Document_Antiquotation.setup name;
+
+fun gen_antiquotation_pretty name embedded scan f =
+ gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
+
+fun gen_antiquotation_pretty_source name embedded scan f =
+ gen_setup name embedded scan
(fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
-fun antiquotation_raw name scan f =
- Document_Antiquotation.setup name scan
- (fn {context = ctxt, argument = x, ...} => f ctxt x);
+fun gen_antiquotation_raw name embedded scan f =
+ gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
+
+fun gen_antiquotation_verbatim name embedded scan f =
+ gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
+
+in
-fun antiquotation_verbatim name scan f =
- antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt);
+fun antiquotation_pretty name = gen_antiquotation_pretty name false;
+fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
+
+fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
+fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
+
+fun antiquotation_raw name = gen_antiquotation_raw name false;
+fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
+
+fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
+fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
end;
+
+end;
--- a/src/Pure/Tools/jedit.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Tools/jedit.ML Fri Jan 04 21:49:06 2019 +0100
@@ -74,7 +74,7 @@
val _ =
Theory.setup
- (Thy_Output.antiquotation_verbatim \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position)
+ (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position)
(fn ctxt => fn (name, pos) =>
let
val _ =
--- a/src/Pure/Tools/named_theorems.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Tools/named_theorems.ML Fri Jan 04 21:49:06 2019 +0100
@@ -103,7 +103,7 @@
(* ML antiquotation *)
val _ = Theory.setup
- (ML_Antiquotation.inline \<^binding>\<open>named_theorems\<close>
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>named_theorems\<close>
(Args.context -- Scan.lift Args.embedded_position >>
(fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
--- a/src/Pure/Tools/plugin.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Tools/plugin.ML Fri Jan 04 21:49:06 2019 +0100
@@ -40,7 +40,7 @@
#1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt));
val _ = Theory.setup
- (ML_Antiquotation.inline \<^binding>\<open>plugin\<close>
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>plugin\<close>
(Args.context -- Scan.lift Args.embedded_position >> (ML_Syntax.print_string o uncurry check)));
--- a/src/Pure/Tools/rail.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Tools/rail.ML Fri Jan 04 21:49:06 2019 +0100
@@ -384,7 +384,7 @@
in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end;
val _ = Theory.setup
- (Thy_Output.antiquotation_raw \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
+ (Thy_Output.antiquotation_raw_embedded \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
(fn ctxt => output_rules ctxt o read ctxt));
end;
--- a/src/Pure/simplifier.ML Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/simplifier.ML Fri Jan 04 21:49:06 2019 +0100
@@ -114,7 +114,7 @@
val the_simproc = Name_Space.get o get_simprocs;
val _ = Theory.setup
- (ML_Antiquotation.value \<^binding>\<open>simproc\<close>
+ (ML_Antiquotation.value_embedded \<^binding>\<open>simproc\<close>
(Args.context -- Scan.lift Args.embedded_position
>> (fn (ctxt, name) =>
"Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));