support for isabelle update -u control_cartouches;
authorwenzelm
Fri Jan 04 21:49:06 2019 +0100 (8 months ago)
changeset 69592a80d8ec6c998
parent 69591 cc6a21413f8a
child 69593 3dda49e08b9d
support for isabelle update -u control_cartouches;
NEWS
etc/options
src/HOL/Library/LaTeXsugar.thy
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/value_command.ML
src/Pure/General/antiquote.ML
src/Pure/General/symbol.ML
src/Pure/ML/ml_antiquotation.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/ML/ml_context.ML
src/Pure/PIDE/resources.ML
src/Pure/Thy/document_antiquotation.ML
src/Pure/Thy/document_antiquotations.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/jedit.ML
src/Pure/Tools/named_theorems.ML
src/Pure/Tools/plugin.ML
src/Pure/Tools/rail.ML
src/Pure/simplifier.ML
     1.1 --- a/NEWS	Thu Jan 03 22:30:41 2019 +0100
     1.2 +++ b/NEWS	Fri Jan 04 21:49:06 2019 +0100
     1.3 @@ -171,6 +171,10 @@
     1.4  section "Theory update". Theory sessions are specified as in "isabelle
     1.5  dump".
     1.6  
     1.7 +* The command-line tool "isabelle update -u control_cartouches" changes
     1.8 +antiquotations into control-symbol format (where possible): @{NAME}
     1.9 +becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\<open>ARG\<close>.
    1.10 +
    1.11  * Support for Isabelle command-line tools defined in Isabelle/Scala.
    1.12  Instances of class Isabelle_Scala_Tools may be configured via the shell
    1.13  function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
     2.1 --- a/etc/options	Thu Jan 03 22:30:41 2019 +0100
     2.2 +++ b/etc/options	Fri Jan 04 21:49:06 2019 +0100
     2.3 @@ -285,6 +285,9 @@
     2.4  option update_mixfix_cartouches : bool = false
     2.5    -- "update mixfix templates to use cartouches instead of double quotes"
     2.6  
     2.7 +option update_control_cartouches : bool = false
     2.8 +  -- "update antiquotations to use control symbol with cartouche argument"
     2.9 +
    2.10  
    2.11  section "Build Database"
    2.12  
     3.1 --- a/src/HOL/Library/LaTeXsugar.thy	Thu Jan 03 22:30:41 2019 +0100
     3.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jan 04 21:49:06 2019 +0100
     3.3 @@ -97,7 +97,8 @@
     3.4    "_asm" :: "prop \<Rightarrow> asms" ("_")
     3.5  
     3.6  setup \<open>
     3.7 -  Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
     3.8 +  Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>const_typ\<close>
     3.9 +    (Scan.lift Args.embedded_inner_syntax)
    3.10      (fn ctxt => fn c =>
    3.11        let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
    3.12          Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jan 03 22:30:41 2019 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Jan 04 21:49:06 2019 +0100
     4.3 @@ -983,7 +983,8 @@
     4.4    end;
     4.5  
     4.6  fun fp_antiquote_setup binding =
     4.7 -  Thy_Output.antiquotation_pretty_source binding (Args.type_name {proper = true, strict = true})
     4.8 +  Thy_Output.antiquotation_pretty_source_embedded binding
     4.9 +    (Args.type_name {proper = true, strict = true})
    4.10      (fn ctxt => fn fcT_name =>
    4.11         (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
    4.12           NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
     5.1 --- a/src/HOL/Tools/value_command.ML	Thu Jan 03 22:30:41 2019 +0100
     5.2 +++ b/src/HOL/Tools/value_command.ML	Fri Jan 04 21:49:06 2019 +0100
     5.3 @@ -73,7 +73,7 @@
     5.4        >> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t)));
     5.5  
     5.6  val _ = Theory.setup
     5.7 -  (Thy_Output.antiquotation_pretty_source \<^binding>\<open>value\<close>
     5.8 +  (Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value\<close>
     5.9      (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    5.10      (fn ctxt => fn ((name, style), t) =>
    5.11        Thy_Output.pretty_term ctxt (style (value_select name ctxt t)))
     6.1 --- a/src/Pure/General/antiquote.ML	Thu Jan 03 22:30:41 2019 +0100
     6.2 +++ b/src/Pure/General/antiquote.ML	Fri Jan 04 21:49:06 2019 +0100
     6.3 @@ -14,6 +14,7 @@
     6.4    val text_range: text_antiquote list -> Position.range
     6.5    val split_lines: text_antiquote list -> text_antiquote list list
     6.6    val antiq_reports: 'a antiquote list -> Position.report list
     6.7 +  val update_reports: bool -> Position.T -> string list -> Position.report_text list
     6.8    val scan_control: control scanner
     6.9    val scan_antiq: antiq scanner
    6.10    val scan_antiquote: text_antiquote scanner
    6.11 @@ -71,6 +72,30 @@
    6.12           (pos, Markup.language_antiquotation)]);
    6.13  
    6.14  
    6.15 +(* update *)
    6.16 +
    6.17 +fun update_reports embedded pos src =
    6.18 +  let
    6.19 +    val n = length src;
    6.20 +    val no_arg = n = 1;
    6.21 +    val embedded_arg = n = 2 andalso embedded;
    6.22 +    val control =
    6.23 +      (case src of
    6.24 +        name :: _ =>
    6.25 +          if Symbol.is_ascii_identifier name andalso name <> "cartouche" andalso
    6.26 +            (no_arg orelse embedded_arg)
    6.27 +          then SOME (Symbol.control_prefix ^ name ^ Symbol.control_suffix)
    6.28 +          else NONE
    6.29 +      | [] => NONE);
    6.30 +    val arg = if embedded_arg then cartouche (nth src 1) else "";
    6.31 +  in
    6.32 +    (case control of
    6.33 +      SOME sym => [((pos, Markup.update), sym ^ arg)]
    6.34 +    | NONE => [])
    6.35 +  end;
    6.36 +
    6.37 +
    6.38 +
    6.39  (* scan *)
    6.40  
    6.41  open Basic_Symbol_Pos;
     7.1 --- a/src/Pure/General/symbol.ML	Thu Jan 03 22:30:41 2019 +0100
     7.2 +++ b/src/Pure/General/symbol.ML	Fri Jan 04 21:49:06 2019 +0100
     7.3 @@ -23,6 +23,8 @@
     7.4    val is_symbolic: symbol -> bool
     7.5    val is_symbolic_char: symbol -> bool
     7.6    val is_printable: symbol -> bool
     7.7 +  val control_prefix: string
     7.8 +  val control_suffix: string
     7.9    val is_control: symbol -> bool
    7.10    val eof: symbol
    7.11    val is_eof: symbol -> bool
    7.12 @@ -135,8 +137,11 @@
    7.13    if is_char s then 32 <= ord s andalso ord s <= Char.ord #"~"
    7.14    else is_utf8 s orelse raw_symbolic s;
    7.15  
    7.16 +val control_prefix = "\092<^";
    7.17 +val control_suffix = ">";
    7.18 +
    7.19  fun is_control s =
    7.20 -  String.isPrefix "\092<^" s andalso String.isSuffix ">" s;
    7.21 +  String.isPrefix control_prefix s andalso String.isSuffix control_suffix s;
    7.22  
    7.23  
    7.24  (* input source control *)
     8.1 --- a/src/Pure/ML/ml_antiquotation.ML	Thu Jan 03 22:30:41 2019 +0100
     8.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Fri Jan 04 21:49:06 2019 +0100
     8.3 @@ -9,8 +9,13 @@
     8.4    val declaration: binding -> 'a context_parser ->
     8.5      (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
     8.6      theory -> theory
     8.7 +  val declaration_embedded: binding -> 'a context_parser ->
     8.8 +    (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
     8.9 +    theory -> theory
    8.10    val inline: binding -> string context_parser -> theory -> theory
    8.11 +  val inline_embedded: binding -> string context_parser -> theory -> theory
    8.12    val value: binding -> string context_parser -> theory -> theory
    8.13 +  val value_embedded: binding -> string context_parser -> theory -> theory
    8.14  end;
    8.15  
    8.16  structure ML_Antiquotation: ML_ANTIQUOTATION =
    8.17 @@ -18,17 +23,32 @@
    8.18  
    8.19  (* define antiquotations *)
    8.20  
    8.21 -fun declaration name scan body =
    8.22 -  ML_Context.add_antiquotation name
    8.23 +local
    8.24 +
    8.25 +fun gen_declaration name embedded scan body =
    8.26 +  ML_Context.add_antiquotation name embedded
    8.27      (fn src => fn orig_ctxt =>
    8.28        let val (x, _) = Token.syntax scan src orig_ctxt
    8.29        in body src x orig_ctxt end);
    8.30  
    8.31 -fun inline name scan =
    8.32 -  declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
    8.33 +fun gen_inline name embedded scan =
    8.34 +  gen_declaration name embedded scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
    8.35 +
    8.36 +fun gen_value name embedded scan =
    8.37 +  gen_declaration name embedded scan (fn _ => ML_Context.value_decl (Binding.name_of name));
    8.38 +
    8.39 +in
    8.40  
    8.41 -fun value name scan =
    8.42 -  declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name));
    8.43 +fun declaration name = gen_declaration name false;
    8.44 +fun declaration_embedded name = gen_declaration name true;
    8.45 +
    8.46 +fun inline name = gen_inline name false;
    8.47 +fun inline_embedded name = gen_inline name true;
    8.48 +
    8.49 +fun value name = gen_value name false;
    8.50 +fun value_embedded name = gen_value name true;
    8.51 +
    8.52 +end;
    8.53  
    8.54  
    8.55  (* basic antiquotations *)
    8.56 @@ -40,15 +60,15 @@
    8.57  
    8.58    inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
    8.59  
    8.60 -  value (Binding.make ("binding", \<^here>))
    8.61 +  value_embedded (Binding.make ("binding", \<^here>))
    8.62      (Scan.lift (Parse.input Args.embedded) >> (ML_Syntax.make_binding o Input.source_content)) #>
    8.63  
    8.64 -  value (Binding.make ("cartouche", \<^here>))
    8.65 +  value_embedded (Binding.make ("cartouche", \<^here>))
    8.66      (Scan.lift Args.cartouche_input >> (fn source =>
    8.67        "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
    8.68          ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
    8.69  
    8.70 -  inline (Binding.make ("verbatim", \<^here>))
    8.71 +  inline_embedded (Binding.make ("verbatim", \<^here>))
    8.72      (Scan.lift Args.embedded >> ML_Syntax.print_string));
    8.73  
    8.74  end;
     9.1 --- a/src/Pure/ML/ml_antiquotations.ML	Thu Jan 03 22:30:41 2019 +0100
     9.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Fri Jan 04 21:49:06 2019 +0100
     9.3 @@ -16,7 +16,7 @@
     9.4    ML_Antiquotation.inline \<^binding>\<open>assert\<close>
     9.5      (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
     9.6  
     9.7 -  ML_Antiquotation.declaration \<^binding>\<open>print\<close>
     9.8 +  ML_Antiquotation.declaration_embedded \<^binding>\<open>print\<close>
     9.9      (Scan.lift (Scan.optional Args.embedded "Output.writeln"))
    9.10        (fn src => fn output => fn ctxt =>
    9.11          let
    9.12 @@ -40,18 +40,18 @@
    9.13  (* formal entities *)
    9.14  
    9.15  val _ = Theory.setup
    9.16 - (ML_Antiquotation.value \<^binding>\<open>system_option\<close>
    9.17 + (ML_Antiquotation.value_embedded \<^binding>\<open>system_option\<close>
    9.18      (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
    9.19        (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #>
    9.20  
    9.21 -  ML_Antiquotation.value \<^binding>\<open>theory\<close>
    9.22 +  ML_Antiquotation.value_embedded \<^binding>\<open>theory\<close>
    9.23      (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
    9.24        (Theory.check {long = false} ctxt (name, pos);
    9.25         "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^
    9.26          ML_Syntax.print_string name))
    9.27      || Scan.succeed "Proof_Context.theory_of ML_context") #>
    9.28  
    9.29 -  ML_Antiquotation.value \<^binding>\<open>theory_context\<close>
    9.30 +  ML_Antiquotation.value_embedded \<^binding>\<open>theory_context\<close>
    9.31      (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
    9.32        (Theory.check {long = false} ctxt (name, pos);
    9.33         "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
    9.34 @@ -60,20 +60,25 @@
    9.35    ML_Antiquotation.inline \<^binding>\<open>context\<close>
    9.36      (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #>
    9.37  
    9.38 -  ML_Antiquotation.inline \<^binding>\<open>typ\<close> (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
    9.39 -  ML_Antiquotation.inline \<^binding>\<open>term\<close> (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    9.40 -  ML_Antiquotation.inline \<^binding>\<open>prop\<close> (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    9.41 +  ML_Antiquotation.inline_embedded \<^binding>\<open>typ\<close>
    9.42 +    (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
    9.43  
    9.44 -  ML_Antiquotation.value \<^binding>\<open>ctyp\<close> (Args.typ >> (fn T =>
    9.45 +  ML_Antiquotation.inline_embedded \<^binding>\<open>term\<close>
    9.46 +    (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    9.47 +
    9.48 +  ML_Antiquotation.inline_embedded \<^binding>\<open>prop\<close>
    9.49 +    (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    9.50 +
    9.51 +  ML_Antiquotation.value_embedded \<^binding>\<open>ctyp\<close> (Args.typ >> (fn T =>
    9.52      "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
    9.53  
    9.54 -  ML_Antiquotation.value \<^binding>\<open>cterm\<close> (Args.term >> (fn t =>
    9.55 +  ML_Antiquotation.value_embedded \<^binding>\<open>cterm\<close> (Args.term >> (fn t =>
    9.56      "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    9.57  
    9.58 -  ML_Antiquotation.value \<^binding>\<open>cprop\<close> (Args.prop >> (fn t =>
    9.59 +  ML_Antiquotation.value_embedded \<^binding>\<open>cprop\<close> (Args.prop >> (fn t =>
    9.60      "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    9.61  
    9.62 -  ML_Antiquotation.inline \<^binding>\<open>method\<close>
    9.63 +  ML_Antiquotation.inline_embedded \<^binding>\<open>method\<close>
    9.64      (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
    9.65        ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
    9.66  
    9.67 @@ -81,7 +86,7 @@
    9.68  (* locales *)
    9.69  
    9.70  val _ = Theory.setup
    9.71 - (ML_Antiquotation.inline \<^binding>\<open>locale\<close>
    9.72 + (ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close>
    9.73     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
    9.74        Locale.check (Proof_Context.theory_of ctxt) (name, pos)
    9.75        |> ML_Syntax.print_string)));
    9.76 @@ -95,10 +100,10 @@
    9.77    |> ML_Syntax.print_string);
    9.78  
    9.79  val _ = Theory.setup
    9.80 - (ML_Antiquotation.inline \<^binding>\<open>class\<close> (class false) #>
    9.81 -  ML_Antiquotation.inline \<^binding>\<open>class_syntax\<close> (class true) #>
    9.82 + (ML_Antiquotation.inline_embedded \<^binding>\<open>class\<close> (class false) #>
    9.83 +  ML_Antiquotation.inline_embedded \<^binding>\<open>class_syntax\<close> (class true) #>
    9.84  
    9.85 -  ML_Antiquotation.inline \<^binding>\<open>sort\<close>
    9.86 +  ML_Antiquotation.inline_embedded \<^binding>\<open>sort\<close>
    9.87      (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
    9.88        ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
    9.89  
    9.90 @@ -119,13 +124,13 @@
    9.91      in ML_Syntax.print_string res end);
    9.92  
    9.93  val _ = Theory.setup
    9.94 - (ML_Antiquotation.inline \<^binding>\<open>type_name\<close>
    9.95 + (ML_Antiquotation.inline_embedded \<^binding>\<open>type_name\<close>
    9.96      (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
    9.97 -  ML_Antiquotation.inline \<^binding>\<open>type_abbrev\<close>
    9.98 +  ML_Antiquotation.inline_embedded \<^binding>\<open>type_abbrev\<close>
    9.99      (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
   9.100 -  ML_Antiquotation.inline \<^binding>\<open>nonterminal\<close>
   9.101 +  ML_Antiquotation.inline_embedded \<^binding>\<open>nonterminal\<close>
   9.102      (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
   9.103 -  ML_Antiquotation.inline \<^binding>\<open>type_syntax\<close>
   9.104 +  ML_Antiquotation.inline_embedded \<^binding>\<open>type_syntax\<close>
   9.105      (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
   9.106  
   9.107  
   9.108 @@ -142,14 +147,14 @@
   9.109      in ML_Syntax.print_string res end);
   9.110  
   9.111  val _ = Theory.setup
   9.112 - (ML_Antiquotation.inline \<^binding>\<open>const_name\<close>
   9.113 + (ML_Antiquotation.inline_embedded \<^binding>\<open>const_name\<close>
   9.114      (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
   9.115 -  ML_Antiquotation.inline \<^binding>\<open>const_abbrev\<close>
   9.116 +  ML_Antiquotation.inline_embedded \<^binding>\<open>const_abbrev\<close>
   9.117      (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
   9.118 -  ML_Antiquotation.inline \<^binding>\<open>const_syntax\<close>
   9.119 +  ML_Antiquotation.inline_embedded \<^binding>\<open>const_syntax\<close>
   9.120      (const_name (fn (_, c) => Lexicon.mark_const c)) #>
   9.121  
   9.122 -  ML_Antiquotation.inline \<^binding>\<open>syntax_const\<close>
   9.123 +  ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close>
   9.124      (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (c, pos)) =>
   9.125        if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   9.126        then ML_Syntax.print_string c
   9.127 @@ -252,7 +257,7 @@
   9.128  (* outer syntax *)
   9.129  
   9.130  val _ = Theory.setup
   9.131 - (ML_Antiquotation.value \<^binding>\<open>keyword\<close>
   9.132 + (ML_Antiquotation.value_embedded \<^binding>\<open>keyword\<close>
   9.133      (Args.context --
   9.134        Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true)))
   9.135        >> (fn (ctxt, (name, pos)) =>
   9.136 @@ -260,7 +265,7 @@
   9.137            (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
   9.138             "Parse.$$$ " ^ ML_Syntax.print_string name)
   9.139          else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
   9.140 -  ML_Antiquotation.value \<^binding>\<open>command_keyword\<close>
   9.141 +  ML_Antiquotation.value_embedded \<^binding>\<open>command_keyword\<close>
   9.142      (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
   9.143        (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
   9.144          SOME markup =>
    10.1 --- a/src/Pure/ML/ml_context.ML	Thu Jan 03 22:30:41 2019 +0100
    10.2 +++ b/src/Pure/ML/ml_context.ML	Fri Jan 04 21:49:06 2019 +0100
    10.3 @@ -11,7 +11,7 @@
    10.4    val variant: string -> Proof.context -> string * Proof.context
    10.5    type decl = Proof.context -> string * string
    10.6    val value_decl: string -> string -> Proof.context -> decl * Proof.context
    10.7 -  val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
    10.8 +  val add_antiquotation: binding -> bool -> (Token.src -> Proof.context -> decl * Proof.context) ->
    10.9      theory -> theory
   10.10    val print_antiquotations: bool -> Proof.context -> unit
   10.11    val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   10.12 @@ -67,7 +67,7 @@
   10.13  
   10.14  structure Antiquotations = Theory_Data
   10.15  (
   10.16 -  type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table;
   10.17 +  type T = (bool * (Token.src -> Proof.context -> decl * Proof.context)) Name_Space.table;
   10.18    val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
   10.19    val extend = I;
   10.20    fun merge data : T = Name_Space.merge_tables data;
   10.21 @@ -78,17 +78,23 @@
   10.22  fun check_antiquotation ctxt =
   10.23    #1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt);
   10.24  
   10.25 -fun add_antiquotation name f thy = thy
   10.26 -  |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
   10.27 +fun add_antiquotation name embedded scan thy = thy
   10.28 +  |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, (embedded, scan)) #> snd);
   10.29  
   10.30  fun print_antiquotations verbose ctxt =
   10.31    Pretty.big_list "ML antiquotations:"
   10.32      (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt)))
   10.33    |> Pretty.writeln;
   10.34  
   10.35 -fun apply_antiquotation src ctxt =
   10.36 -  let val (src', f) = Token.check_src ctxt get_antiquotations src
   10.37 -  in f src' ctxt end;
   10.38 +fun apply_antiquotation pos src ctxt =
   10.39 +  let
   10.40 +    val (src', (embedded, scan)) = Token.check_src ctxt get_antiquotations src;
   10.41 +    val _ =
   10.42 +      if Options.default_bool "update_control_cartouches" then
   10.43 +        Context_Position.reports_text ctxt
   10.44 +          (Antiquote.update_reports embedded pos (map Token.content_of src'))
   10.45 +      else ();
   10.46 +  in scan src' ctxt end;
   10.47  
   10.48  
   10.49  (* parsing and evaluation *)
   10.50 @@ -123,7 +129,7 @@
   10.51            fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
   10.52  
   10.53            fun expand_src range src ctxt =
   10.54 -            let val (decl, ctxt') = apply_antiquotation src ctxt
   10.55 +            let val (decl, ctxt') = apply_antiquotation (#1 range) src ctxt;
   10.56              in (decl #> tokenize range, ctxt') end;
   10.57  
   10.58            fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
    11.1 --- a/src/Pure/PIDE/resources.ML	Thu Jan 03 22:30:41 2019 +0100
    11.2 +++ b/src/Pure/PIDE/resources.ML	Fri Jan 04 21:49:06 2019 +0100
    11.3 @@ -277,16 +277,16 @@
    11.4  in
    11.5  
    11.6  val _ = Theory.setup
    11.7 - (Thy_Output.antiquotation_verbatim \<^binding>\<open>session\<close>
    11.8 + (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>session\<close>
    11.9      (Scan.lift Parse.embedded_position) check_session #>
   11.10 -  Thy_Output.antiquotation_verbatim \<^binding>\<open>doc\<close>
   11.11 +  Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>doc\<close>
   11.12      (Scan.lift Parse.embedded_position) check_doc #>
   11.13 -  Thy_Output.antiquotation_raw \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
   11.14 -  Thy_Output.antiquotation_raw \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
   11.15 -  Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
   11.16 -  ML_Antiquotation.value \<^binding>\<open>path\<close> (ML_antiq check_path) #>
   11.17 -  ML_Antiquotation.value \<^binding>\<open>file\<close> (ML_antiq check_file) #>
   11.18 -  ML_Antiquotation.value \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
   11.19 +  Thy_Output.antiquotation_raw_embedded \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
   11.20 +  Thy_Output.antiquotation_raw_embedded \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
   11.21 +  Thy_Output.antiquotation_raw_embedded \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
   11.22 +  ML_Antiquotation.value_embedded \<^binding>\<open>path\<close> (ML_antiq check_path) #>
   11.23 +  ML_Antiquotation.value_embedded \<^binding>\<open>file\<close> (ML_antiq check_file) #>
   11.24 +  ML_Antiquotation.value_embedded \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
   11.25    ML_Antiquotation.value \<^binding>\<open>master_dir\<close>
   11.26      (Args.theory >> (ML_Syntax.print_path o master_directory)));
   11.27  
    12.1 --- a/src/Pure/Thy/document_antiquotation.ML	Thu Jan 03 22:30:41 2019 +0100
    12.2 +++ b/src/Pure/Thy/document_antiquotation.ML	Fri Jan 04 21:49:06 2019 +0100
    12.3 @@ -26,6 +26,8 @@
    12.4    val check_option: Proof.context -> xstring * Position.T -> string
    12.5    val setup: binding -> 'a context_parser ->
    12.6      ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
    12.7 +  val setup_embedded: binding -> 'a context_parser ->
    12.8 +    ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
    12.9    val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
   12.10    val boolean: string -> bool
   12.11    val integer: string -> int
   12.12 @@ -86,7 +88,7 @@
   12.13  structure Data = Theory_Data
   12.14  (
   12.15    type T =
   12.16 -    (Token.src -> Proof.context -> Latex.text) Name_Space.table *
   12.17 +    (bool * (Token.src -> Proof.context -> Latex.text)) Name_Space.table *
   12.18        (string -> Proof.context -> Proof.context) Name_Space.table;
   12.19    val empty : T =
   12.20      (Name_Space.empty_table Markup.document_antiquotationN,
   12.21 @@ -112,12 +114,16 @@
   12.22  fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
   12.23  fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
   12.24  
   12.25 -fun setup name scan body thy =
   12.26 +fun gen_setup name embedded scan body thy =
   12.27    let
   12.28      fun cmd src ctxt =
   12.29        let val (x, ctxt') = Token.syntax scan src ctxt
   12.30        in body {context = ctxt', source = src, argument = x} end;
   12.31 -  in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> #2)) end;
   12.32 +    val entry = (name, (embedded, cmd));
   12.33 +  in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true entry #> #2)) end;
   12.34 +
   12.35 +fun setup name = gen_setup name false;
   12.36 +fun setup_embedded name = gen_setup name true;
   12.37  
   12.38  fun setup_option name opt thy = thy
   12.39    |> Data.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> #2));
   12.40 @@ -138,7 +144,7 @@
   12.41  val parse_antiq =
   12.42    Parse.!!!
   12.43      (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
   12.44 -  >> (fn ((name, props), args) => (props, name :: args));
   12.45 +  >> (fn ((name, opts), args) => (opts, name :: args));
   12.46  
   12.47  end;
   12.48  
   12.49 @@ -147,9 +153,15 @@
   12.50  
   12.51  local
   12.52  
   12.53 -fun command src ctxt =
   12.54 -  let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
   12.55 -  in f src' ctxt end;
   12.56 +fun command pos (opts, src) ctxt =
   12.57 +  let
   12.58 +    val (src', (embedded, scan)) = Token.check_src ctxt (#1 o get_antiquotations) src;
   12.59 +    val _ =
   12.60 +      if null opts andalso Options.default_bool "update_control_cartouches" then
   12.61 +        Context_Position.reports_text ctxt
   12.62 +          (Antiquote.update_reports embedded pos (map Token.content_of src'))
   12.63 +      else ();
   12.64 +  in scan src' ctxt end;
   12.65  
   12.66  fun option ((xname, pos), s) ctxt =
   12.67    let
   12.68 @@ -157,14 +169,14 @@
   12.69        Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
   12.70    in opt s ctxt end;
   12.71  
   12.72 -fun eval ctxt (opts, src) =
   12.73 +fun eval ctxt pos (opts, src) =
   12.74    let
   12.75      val preview_ctxt = fold option opts (Config.put show_markup false ctxt);
   12.76 -    val _ = command src preview_ctxt;
   12.77 +    val _ = command pos (opts, src) preview_ctxt;
   12.78  
   12.79      val print_ctxt = Context_Position.set_visible false preview_ctxt;
   12.80      val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN];
   12.81 -  in [Print_Mode.with_modes print_modes (fn () => command src print_ctxt) ()] end;
   12.82 +  in [Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) ()] end;
   12.83  
   12.84  in
   12.85  
   12.86 @@ -172,10 +184,11 @@
   12.87    (case antiq of
   12.88      Antiquote.Text ss => eval_text ss
   12.89    | Antiquote.Control {name, body, ...} =>
   12.90 -      eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
   12.91 +      eval ctxt Position.none
   12.92 +        ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
   12.93    | Antiquote.Antiq {range = (pos, _), body, ...} =>
   12.94        let val keywords = Thy_Header.get_keywords' ctxt;
   12.95 -      in eval ctxt (Token.read_antiq keywords parse_antiq (body, pos)) end);
   12.96 +      in eval ctxt pos (Token.read_antiq keywords parse_antiq (body, pos)) end);
   12.97  
   12.98  end;
   12.99  
    13.1 --- a/src/Pure/Thy/document_antiquotations.ML	Thu Jan 03 22:30:41 2019 +0100
    13.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Fri Jan 04 21:49:06 2019 +0100
    13.3 @@ -62,7 +62,7 @@
    13.4  fun pretty_theory ctxt (name, pos) =
    13.5    (Theory.check {long = true} ctxt (name, pos); Pretty.str name);
    13.6  
    13.7 -val basic_entity = Thy_Output.antiquotation_pretty_source;
    13.8 +val basic_entity = Thy_Output.antiquotation_pretty_source_embedded;
    13.9  
   13.10  fun basic_entities name scan pretty =
   13.11    Document_Antiquotation.setup name scan
   13.12 @@ -132,7 +132,7 @@
   13.13  local
   13.14  
   13.15  fun control_antiquotation name s1 s2 =
   13.16 -  Thy_Output.antiquotation_raw name (Scan.lift Args.cartouche_input)
   13.17 +  Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
   13.18      (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false});
   13.19  
   13.20  in
   13.21 @@ -158,7 +158,7 @@
   13.22    Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
   13.23  
   13.24  fun text_antiquotation name =
   13.25 -  Thy_Output.antiquotation_raw name (Scan.lift Args.text_input)
   13.26 +  Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
   13.27      (fn ctxt => fn text =>
   13.28        let
   13.29          val _ = report_text ctxt text;
   13.30 @@ -169,7 +169,7 @@
   13.31        end);
   13.32  
   13.33  val theory_text_antiquotation =
   13.34 -  Thy_Output.antiquotation_raw \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
   13.35 +  Thy_Output.antiquotation_raw_embedded \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
   13.36      (fn ctxt => fn text =>
   13.37        let
   13.38          val keywords = Thy_Header.get_keywords' ctxt;
   13.39 @@ -243,7 +243,7 @@
   13.40  (* verbatim text *)
   13.41  
   13.42  val _ = Theory.setup
   13.43 -  (Thy_Output.antiquotation_verbatim \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
   13.44 +  (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
   13.45      (fn ctxt => fn text =>
   13.46        let
   13.47          val _ =
   13.48 @@ -257,7 +257,7 @@
   13.49  local
   13.50  
   13.51  fun ml_text name ml =
   13.52 -  Thy_Output.antiquotation_verbatim name (Scan.lift Args.text_input)
   13.53 +  Thy_Output.antiquotation_verbatim_embedded name (Scan.lift Args.text_input)
   13.54      (fn ctxt => fn text =>
   13.55        let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text)
   13.56        in #1 (Input.source_content text) end);
   13.57 @@ -287,7 +287,7 @@
   13.58  (* URLs *)
   13.59  
   13.60  val _ = Theory.setup
   13.61 -  (Thy_Output.antiquotation_raw \<^binding>\<open>url\<close> (Scan.lift Args.embedded_position)
   13.62 +  (Thy_Output.antiquotation_raw_embedded \<^binding>\<open>url\<close> (Scan.lift Args.embedded_position)
   13.63      (fn ctxt => fn (url, pos) =>
   13.64        let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)]
   13.65        in Latex.enclose_block "\\url{" "}" [Latex.string url] end));
    14.1 --- a/src/Pure/Thy/thy_output.ML	Thu Jan 03 22:30:41 2019 +0100
    14.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Jan 04 21:49:06 2019 +0100
    14.3 @@ -27,12 +27,20 @@
    14.4    val pretty_items_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
    14.5    val antiquotation_pretty:
    14.6      binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
    14.7 +  val antiquotation_pretty_embedded:
    14.8 +    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
    14.9    val antiquotation_pretty_source:
   14.10      binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   14.11 +  val antiquotation_pretty_source_embedded:
   14.12 +    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   14.13    val antiquotation_raw:
   14.14      binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
   14.15 +  val antiquotation_raw_embedded:
   14.16 +    binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
   14.17    val antiquotation_verbatim:
   14.18      binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
   14.19 +  val antiquotation_verbatim_embedded:
   14.20 +    binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
   14.21  end;
   14.22  
   14.23  structure Thy_Output: THY_OUTPUT =
   14.24 @@ -525,19 +533,40 @@
   14.25  
   14.26  (* antiquotation variants *)
   14.27  
   14.28 -fun antiquotation_pretty name scan f =
   14.29 -  Document_Antiquotation.setup name scan
   14.30 -    (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
   14.31 +local
   14.32  
   14.33 -fun antiquotation_pretty_source name scan f =
   14.34 -  Document_Antiquotation.setup name scan
   14.35 +fun gen_setup name embedded =
   14.36 +  if embedded
   14.37 +  then Document_Antiquotation.setup_embedded name
   14.38 +  else Document_Antiquotation.setup name;
   14.39 +
   14.40 +fun gen_antiquotation_pretty name embedded scan f =
   14.41 +  gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
   14.42 +
   14.43 +fun gen_antiquotation_pretty_source name embedded scan f =
   14.44 +  gen_setup name embedded scan
   14.45      (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
   14.46  
   14.47 -fun antiquotation_raw name scan f =
   14.48 -  Document_Antiquotation.setup name scan
   14.49 -    (fn {context = ctxt, argument = x, ...} => f ctxt x);
   14.50 +fun gen_antiquotation_raw name embedded scan f =
   14.51 +  gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
   14.52 +
   14.53 +fun gen_antiquotation_verbatim name embedded scan f =
   14.54 +  gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
   14.55 +
   14.56 +in
   14.57  
   14.58 -fun antiquotation_verbatim name scan f =
   14.59 -  antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt);
   14.60 +fun antiquotation_pretty name = gen_antiquotation_pretty name false;
   14.61 +fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
   14.62 +
   14.63 +fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
   14.64 +fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
   14.65 +
   14.66 +fun antiquotation_raw name = gen_antiquotation_raw name false;
   14.67 +fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
   14.68 +
   14.69 +fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
   14.70 +fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
   14.71  
   14.72  end;
   14.73 +
   14.74 +end;
    15.1 --- a/src/Pure/Tools/jedit.ML	Thu Jan 03 22:30:41 2019 +0100
    15.2 +++ b/src/Pure/Tools/jedit.ML	Fri Jan 04 21:49:06 2019 +0100
    15.3 @@ -74,7 +74,7 @@
    15.4  
    15.5  val _ =
    15.6    Theory.setup
    15.7 -    (Thy_Output.antiquotation_verbatim \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position)
    15.8 +    (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position)
    15.9        (fn ctxt => fn (name, pos) =>
   15.10          let
   15.11            val _ =
    16.1 --- a/src/Pure/Tools/named_theorems.ML	Thu Jan 03 22:30:41 2019 +0100
    16.2 +++ b/src/Pure/Tools/named_theorems.ML	Fri Jan 04 21:49:06 2019 +0100
    16.3 @@ -103,7 +103,7 @@
    16.4  (* ML antiquotation *)
    16.5  
    16.6  val _ = Theory.setup
    16.7 -  (ML_Antiquotation.inline \<^binding>\<open>named_theorems\<close>
    16.8 +  (ML_Antiquotation.inline_embedded \<^binding>\<open>named_theorems\<close>
    16.9      (Args.context -- Scan.lift Args.embedded_position >>
   16.10        (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
   16.11  
    17.1 --- a/src/Pure/Tools/plugin.ML	Thu Jan 03 22:30:41 2019 +0100
    17.2 +++ b/src/Pure/Tools/plugin.ML	Fri Jan 04 21:49:06 2019 +0100
    17.3 @@ -40,7 +40,7 @@
    17.4    #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt));
    17.5  
    17.6  val _ = Theory.setup
    17.7 -  (ML_Antiquotation.inline \<^binding>\<open>plugin\<close>
    17.8 +  (ML_Antiquotation.inline_embedded \<^binding>\<open>plugin\<close>
    17.9      (Args.context -- Scan.lift Args.embedded_position >> (ML_Syntax.print_string o uncurry check)));
   17.10  
   17.11  
    18.1 --- a/src/Pure/Tools/rail.ML	Thu Jan 03 22:30:41 2019 +0100
    18.2 +++ b/src/Pure/Tools/rail.ML	Fri Jan 04 21:49:06 2019 +0100
    18.3 @@ -384,7 +384,7 @@
    18.4    in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end;
    18.5  
    18.6  val _ = Theory.setup
    18.7 -  (Thy_Output.antiquotation_raw \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
    18.8 +  (Thy_Output.antiquotation_raw_embedded \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
    18.9      (fn ctxt => output_rules ctxt o read ctxt));
   18.10  
   18.11  end;
    19.1 --- a/src/Pure/simplifier.ML	Thu Jan 03 22:30:41 2019 +0100
    19.2 +++ b/src/Pure/simplifier.ML	Fri Jan 04 21:49:06 2019 +0100
    19.3 @@ -114,7 +114,7 @@
    19.4  val the_simproc = Name_Space.get o get_simprocs;
    19.5  
    19.6  val _ = Theory.setup
    19.7 -  (ML_Antiquotation.value \<^binding>\<open>simproc\<close>
    19.8 +  (ML_Antiquotation.value_embedded \<^binding>\<open>simproc\<close>
    19.9      (Args.context -- Scan.lift Args.embedded_position
   19.10        >> (fn (ctxt, name) =>
   19.11          "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));