src/Pure/ML/ml_antiquotation.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 64556 851ae0e7b09c
child 67146 909dcdec2122
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@56072
     1
(*  Title:      Pure/ML/ml_antiquotation.ML
wenzelm@27340
     2
    Author:     Makarius
wenzelm@27340
     3
wenzelm@56205
     4
ML antiquotations.
wenzelm@27340
     5
*)
wenzelm@27340
     6
wenzelm@56072
     7
signature ML_ANTIQUOTATION =
wenzelm@27340
     8
sig
wenzelm@56205
     9
  val declaration: binding -> 'a context_parser ->
wenzelm@58011
    10
    (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
wenzelm@56205
    11
    theory -> theory
wenzelm@43560
    12
  val inline: binding -> string context_parser -> theory -> theory
wenzelm@43560
    13
  val value: binding -> string context_parser -> theory -> theory
wenzelm@27340
    14
end;
wenzelm@27340
    15
wenzelm@56072
    16
structure ML_Antiquotation: ML_ANTIQUOTATION =
wenzelm@27340
    17
struct
wenzelm@27340
    18
wenzelm@56205
    19
(* define antiquotations *)
wenzelm@56205
    20
wenzelm@56205
    21
fun declaration name scan body =
wenzelm@56205
    22
  ML_Context.add_antiquotation name
wenzelm@56205
    23
    (fn src => fn orig_ctxt =>
wenzelm@58011
    24
      let val (x, _) = Token.syntax scan src orig_ctxt
wenzelm@56205
    25
      in body src x orig_ctxt end);
wenzelm@27340
    26
wenzelm@53169
    27
fun inline name scan =
wenzelm@56205
    28
  declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
wenzelm@27340
    29
wenzelm@53169
    30
fun value name scan =
wenzelm@59112
    31
  declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name));
wenzelm@27340
    32
wenzelm@27340
    33
wenzelm@56205
    34
(* basic antiquotations *)
wenzelm@27340
    35
wenzelm@53171
    36
val _ = Theory.setup
wenzelm@64556
    37
 (declaration (Binding.make ("here", \<^here>)) (Scan.succeed ())
wenzelm@59112
    38
    (fn src => fn () =>
wenzelm@59112
    39
      ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
wenzelm@56071
    40
wenzelm@64556
    41
  inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
wenzelm@62662
    42
wenzelm@64556
    43
  value (Binding.make ("binding", \<^here>))
wenzelm@62850
    44
    (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
wenzelm@62850
    45
wenzelm@64556
    46
  value (Binding.make ("cartouche", \<^here>))
wenzelm@62850
    47
    (Scan.lift Args.cartouche_input >> (fn source =>
wenzelm@62850
    48
      "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
wenzelm@62850
    49
        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
wenzelm@46948
    50
wenzelm@27340
    51
end;