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