src/Pure/ML/ml_antiquotation.ML
author wenzelm
Mon, 18 Aug 2014 12:17:31 +0200
changeset 57978 8f4a332500e4
parent 57832 5b48f2047c24
child 58011 bc6bced136e5
permissions -rw-r--r--
Added tag Isabelle2014-RC4 for changeset 113b43b84412
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56072
31e427387ab5 tuned signature -- clarified module name;
wenzelm
parents: 56071
diff changeset
     1
(*  Title:      Pure/ML/ml_antiquotation.ML
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     3
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
     4
ML antiquotations.
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     5
*)
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     6
56072
31e427387ab5 tuned signature -- clarified module name;
wenzelm
parents: 56071
diff changeset
     7
signature ML_ANTIQUOTATION =
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     8
sig
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     9
  val variant: string -> Proof.context -> string * Proof.context
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    10
  val declaration: binding -> 'a context_parser ->
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    11
    (Args.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    12
    theory -> theory
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43326
diff changeset
    13
  val inline: binding -> string context_parser -> theory -> theory
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43326
diff changeset
    14
  val value: binding -> string context_parser -> theory -> theory
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    15
end;
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    16
56072
31e427387ab5 tuned signature -- clarified module name;
wenzelm
parents: 56071
diff changeset
    17
structure ML_Antiquotation: ML_ANTIQUOTATION =
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    18
struct
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    19
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    20
(* unique names *)
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    21
57832
5b48f2047c24 clarified compile-time use of ML_print_depth;
wenzelm
parents: 56811
diff changeset
    22
val init_context = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
48776
37cd53e69840 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents: 48646
diff changeset
    23
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36950
diff changeset
    24
structure Names = Proof_Data
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    25
(
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    26
  type T = Name.context;
48776
37cd53e69840 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents: 48646
diff changeset
    27
  fun init _ = init_context;
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    28
);
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    29
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    30
fun variant a ctxt =
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    31
  let
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36950
diff changeset
    32
    val names = Names.get ctxt;
56811
b66639331db5 optional case enforcement
haftmann
parents: 56436
diff changeset
    33
    val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names;
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36950
diff changeset
    34
    val ctxt' = Names.put names' ctxt;
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    35
  in (b, ctxt') end;
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    36
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    37
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    38
(* define antiquotations *)
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    39
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    40
fun declaration name scan body =
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    41
  ML_Context.add_antiquotation name
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    42
    (fn src => fn orig_ctxt =>
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    43
      let val (x, _) = Args.syntax scan src orig_ctxt
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    44
      in body src x orig_ctxt end);
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    45
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53163
diff changeset
    46
fun inline name scan =
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    47
  declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    48
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53163
diff changeset
    49
fun value name scan =
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    50
  declaration name scan (fn _ => fn s => fn ctxt =>
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 56002
diff changeset
    51
    let
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 56002
diff changeset
    52
      val (a, ctxt') = variant (Binding.name_of name) ctxt;
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 56002
diff changeset
    53
      val env = "val " ^ a ^ " = " ^ s ^ ";\n";
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 56002
diff changeset
    54
      val body = "Isabelle." ^ a;
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 56002
diff changeset
    55
    in (K (env, body), ctxt') end);
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    56
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    57
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    58
(* basic antiquotations *)
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    59
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53170
diff changeset
    60
val _ = Theory.setup
56436
30ccec1e82fb more source positions;
wenzelm
parents: 56205
diff changeset
    61
 (declaration (Binding.make ("here", @{here})) (Scan.succeed ())
56071
2ffdedb0c044 added ML antiquotation @{here};
wenzelm
parents: 56069
diff changeset
    62
    (fn src => fn () => fn ctxt =>
2ffdedb0c044 added ML antiquotation @{here};
wenzelm
parents: 56069
diff changeset
    63
      let
2ffdedb0c044 added ML antiquotation @{here};
wenzelm
parents: 56069
diff changeset
    64
        val (a, ctxt') = variant "position" ctxt;
2ffdedb0c044 added ML antiquotation @{here};
wenzelm
parents: 56069
diff changeset
    65
        val (_, pos) = Args.name_of_src src;
2ffdedb0c044 added ML antiquotation @{here};
wenzelm
parents: 56069
diff changeset
    66
        val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
2ffdedb0c044 added ML antiquotation @{here};
wenzelm
parents: 56069
diff changeset
    67
        val body = "Isabelle." ^ a;
2ffdedb0c044 added ML antiquotation @{here};
wenzelm
parents: 56069
diff changeset
    68
      in (K (env, body), ctxt') end) #>
2ffdedb0c044 added ML antiquotation @{here};
wenzelm
parents: 56069
diff changeset
    69
56436
30ccec1e82fb more source positions;
wenzelm
parents: 56205
diff changeset
    70
  value (Binding.make ("binding", @{here}))
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56072
diff changeset
    71
    (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
46948
aae5566d6756 added ML antiquotation @{keyword};
wenzelm
parents: 43794
diff changeset
    72
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    73
end;
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    74