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;
     1 (*  Title:      Pure/ML/ml_antiquotation.ML
     2     Author:     Makarius
     3 
     4 ML antiquotations.
     5 *)
     6 
     7 signature ML_ANTIQUOTATION =
     8 sig
     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
    14 end;
    15 
    16 structure ML_Antiquotation: ML_ANTIQUOTATION =
    17 struct
    18 
    19 (* define antiquotations *)
    20 
    21 fun 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 
    27 fun inline name scan =
    28   declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
    29 
    30 fun value name scan =
    31   declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name));
    32 
    33 
    34 (* basic antiquotations *)
    35 
    36 val _ = 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.name) >> 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 
    51 end;