1(*  Title:      Pure/ML/ml_antiquotation.ML
2    Author:     Makarius
3
4ML antiquotations.
5*)
6
7signature ML_ANTIQUOTATION =
8sig
9  val declaration: binding -> 'a context_parser ->
10    (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
11    theory -> theory
12  val inline: binding -> string context_parser -> theory -> theory
13  val value: binding -> string context_parser -> theory -> theory
14end;
15
16structure ML_Antiquotation: ML_ANTIQUOTATION =
17struct
18
19(* define antiquotations *)
20
21fun declaration name scan body =
22  ML_Context.add_antiquotation name
23    (fn src => fn orig_ctxt =>
24      let val (x, _) = Token.syntax scan src orig_ctxt
25      in body src x orig_ctxt end);
26
27fun inline name scan =
28  declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
29
30fun value name scan =
31  declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name));
32
33
34(* basic antiquotations *)
35
36val _ = Theory.setup
37 (declaration (Binding.make ("here", \<^here>)) (Scan.succeed ())
38    (fn src => fn () =>
39      ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
40
41  inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
42
43  value (Binding.make ("binding", \<^here>))
44    (Scan.lift (Parse.position Args.embedded) >> ML_Syntax.make_binding) #>
45
46  value (Binding.make ("cartouche", \<^here>))
47    (Scan.lift Args.cartouche_input >> (fn source =>
48      "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
49        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
50
51end;
52