src/Pure/ML/ml_antiquote.ML
author wenzelm
Wed, 21 Jul 2010 15:02:51 +0200
changeset 37868 59eed00bfd8e
parent 37304 645f849eefa7
child 40110 93e7935d4cb5
permissions -rw-r--r--
ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state; recovered @{theory_ref NAME} (cf. 1f09a22a1027);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/ml_antiquote.ML
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     3
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     4
Common ML antiquotations.
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     5
*)
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     6
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     7
signature ML_ANTIQUOTE =
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
     8
sig
30513
1796b8ea88aa eliminated type Args.T;
wenzelm
parents: 30364
diff changeset
     9
  val macro: string -> Proof.context context_parser -> unit
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    10
  val variant: string -> Proof.context -> string * Proof.context
30513
1796b8ea88aa eliminated type Args.T;
wenzelm
parents: 30364
diff changeset
    11
  val inline: string -> string context_parser -> unit
1796b8ea88aa eliminated type Args.T;
wenzelm
parents: 30364
diff changeset
    12
  val declaration: string -> string -> string context_parser -> unit
1796b8ea88aa eliminated type Args.T;
wenzelm
parents: 30364
diff changeset
    13
  val value: string -> string context_parser -> unit
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    14
end;
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    15
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    16
structure ML_Antiquote: ML_ANTIQUOTE =
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    17
struct
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    18
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    19
(** generic tools **)
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    20
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    21
(* ML names *)
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    22
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36950
diff changeset
    23
structure Names = Proof_Data
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    24
(
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    25
  type T = Name.context;
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    26
  fun init _ = ML_Syntax.reserved;
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    27
);
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    28
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    29
fun variant a ctxt =
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    30
  let
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36950
diff changeset
    31
    val names = Names.get ctxt;
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    32
    val ([b], names') = Name.variants [a] names;
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36950
diff changeset
    33
    val ctxt' = Names.put names' ctxt;
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    34
  in (b, ctxt') end;
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    35
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    36
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    37
(* specific antiquotations *)
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    38
27379
c706b7201826 added macro interface;
wenzelm
parents: 27370
diff changeset
    39
fun macro name scan = ML_Context.add_antiq name
27868
a28b3cd0077b ML_Context.add_antiq: pass position;
wenzelm
parents: 27809
diff changeset
    40
  (fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
35019
1ec0a3ff229e simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents: 33519
diff changeset
    41
    (Context.Proof ctxt, fn background => (K ("", ""), background)))));
27379
c706b7201826 added macro interface;
wenzelm
parents: 27370
diff changeset
    42
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    43
fun inline name scan = ML_Context.add_antiq name
35019
1ec0a3ff229e simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents: 33519
diff changeset
    44
  (fn _ => scan >> (fn s => fn background => (K ("", s), background)));
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    45
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    46
fun declaration kind name scan = ML_Context.add_antiq name
35019
1ec0a3ff229e simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents: 33519
diff changeset
    47
  (fn _ => scan >> (fn s => fn background =>
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    48
    let
37304
645f849eefa7 allow qualified names;
wenzelm
parents: 37216
diff changeset
    49
      val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    50
      val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
35019
1ec0a3ff229e simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents: 33519
diff changeset
    51
      val body = "Isabelle." ^ a;
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    52
    in (K (env, body), background') end));
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    53
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    54
val value = declaration "val";
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    55
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    56
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    57
30231
b3f3ad327d4d added @{binding} ML antiquotations;
wenzelm
parents: 29606
diff changeset
    58
(** misc antiquotations **)
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    59
36162
0bd034a80a9a added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents: 35670
diff changeset
    60
val _ = inline "make_string" (Scan.succeed ml_make_string);
0bd034a80a9a added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents: 35670
diff changeset
    61
30721
0579dec9f8ba @{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;
wenzelm
parents: 30524
diff changeset
    62
val _ = value "binding"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36162
diff changeset
    63
  (Scan.lift (Parse.position Args.name)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36162
diff changeset
    64
    >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    65
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    66
val _ = value "theory"
37868
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37304
diff changeset
    67
  (Scan.lift Args.name >> (fn name =>
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37304
diff changeset
    68
    "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    69
  || Scan.succeed "ML_Context.the_global_context ()");
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    70
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    71
val _ = value "theory_ref"
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    72
  (Scan.lift Args.name >> (fn name =>
37868
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37304
diff changeset
    73
    "Theory.check_thy (Context.get_theory (ML_Context.the_global_context ()) " ^
59eed00bfd8e ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents: 37304
diff changeset
    74
      ML_Syntax.print_string name ^ ")")
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    75
  || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    76
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    77
val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    78
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    79
val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    80
val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    81
val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    82
27379
c706b7201826 added macro interface;
wenzelm
parents: 27370
diff changeset
    83
val _ = macro "let" (Args.context --
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36162
diff changeset
    84
  Scan.lift
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36162
diff changeset
    85
    (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
27379
c706b7201826 added macro interface;
wenzelm
parents: 27370
diff changeset
    86
    >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
c706b7201826 added macro interface;
wenzelm
parents: 27370
diff changeset
    87
c706b7201826 added macro interface;
wenzelm
parents: 27370
diff changeset
    88
val _ = macro "note" (Args.context :|-- (fn ctxt =>
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36162
diff changeset
    89
  Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
27379
c706b7201826 added macro interface;
wenzelm
parents: 27370
diff changeset
    90
    ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
30761
ac7570d80c3d renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
wenzelm
parents: 30721
diff changeset
    91
  >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
27379
c706b7201826 added macro interface;
wenzelm
parents: 27370
diff changeset
    92
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    93
val _ = value "ctyp" (Args.typ >> (fn T =>
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    94
  "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    95
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    96
val _ = value "cterm" (Args.term >> (fn t =>
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    97
  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    98
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
    99
val _ = value "cprop" (Args.prop >> (fn t =>
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   100
  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   101
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   102
val _ = value "cpat"
27882
eaa9fef9f4c1 Args.name_source(_position) for proper position information;
wenzelm
parents: 27868
diff changeset
   103
  (Args.context -- Scan.lift Args.name_source >> uncurry ProofContext.read_term_pattern >> (fn t =>
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   104
    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   105
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   106
35396
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   107
(* type classes *)
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   108
35670
3007b46c1660 ProofContext.read_class/read_type_name_proper;
wenzelm
parents: 35429
diff changeset
   109
fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
3007b46c1660 ProofContext.read_class/read_type_name_proper;
wenzelm
parents: 35429
diff changeset
   110
  ProofContext.read_class ctxt s
35429
afa8cf9e63d8 authentic syntax for classes and type constructors;
wenzelm
parents: 35401
diff changeset
   111
  |> syn ? Syntax.mark_class
35396
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   112
  |> ML_Syntax.print_string);
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   113
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   114
val _ = inline "class" (class false);
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   115
val _ = inline "class_syntax" (class true);
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   116
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   117
val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   118
  ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   119
041bb8d18916 ML antiquotations for type classes;
wenzelm
parents: 35361
diff changeset
   120
35361
4c7c849b70aa more orthogonal antiquotations for type constructors;
wenzelm
parents: 35262
diff changeset
   121
(* type constructors *)
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   122
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36162
diff changeset
   123
fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
35401
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   124
  >> (fn (ctxt, (s, pos)) =>
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   125
    let
35670
3007b46c1660 ProofContext.read_class/read_type_name_proper;
wenzelm
parents: 35429
diff changeset
   126
      val Type (c, _) = ProofContext.read_type_name_proper ctxt false s;
3007b46c1660 ProofContext.read_class/read_type_name_proper;
wenzelm
parents: 35429
diff changeset
   127
      val decl = Type.the_decl (ProofContext.tsig_of ctxt) c;
35401
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   128
      val res =
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   129
        (case try check (c, decl) of
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   130
          SOME res => res
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   131
        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos));
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   132
    in ML_Syntax.print_string res end);
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   133
35401
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   134
val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   135
val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   136
val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
35429
afa8cf9e63d8 authentic syntax for classes and type constructors;
wenzelm
parents: 35401
diff changeset
   137
val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c));
35361
4c7c849b70aa more orthogonal antiquotations for type constructors;
wenzelm
parents: 35262
diff changeset
   138
4c7c849b70aa more orthogonal antiquotations for type constructors;
wenzelm
parents: 35262
diff changeset
   139
4c7c849b70aa more orthogonal antiquotations for type constructors;
wenzelm
parents: 35262
diff changeset
   140
(* constants *)
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   141
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36162
diff changeset
   142
fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
35401
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   143
  >> (fn (ctxt, (s, pos)) =>
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   144
    let
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   145
      val Const (c, _) = ProofContext.read_const_proper ctxt false s;
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   146
      val res = check (ProofContext.consts_of ctxt, c)
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   147
        handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   148
    in ML_Syntax.print_string res end);
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   149
35401
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   150
val _ = inline "const_name" (const_name (fn (consts, c) => (Consts.the_type consts c; c)));
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   151
val _ = inline "const_abbrev" (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c)));
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   152
val _ = inline "const_syntax" (const_name (fn (_, c) => Syntax.mark_const c));
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   153
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   154
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   155
val _ = inline "syntax_const"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36162
diff changeset
   156
  (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
35401
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   157
    if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   158
    else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   159
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   160
val _ = inline "const"
27882
eaa9fef9f4c1 Args.name_source(_position) for proper position information;
wenzelm
parents: 27868
diff changeset
   161
  (Args.context -- Scan.lift Args.name_source -- Scan.optional
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36162
diff changeset
   162
      (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
35139
e1a226a191b6 misc tuning and simplification;
wenzelm
parents: 35111
diff changeset
   163
    >> (fn ((ctxt, raw_c), Ts) =>
e1a226a191b6 misc tuning and simplification;
wenzelm
parents: 35111
diff changeset
   164
      let
35401
bfcbab8592ba clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents: 35396
diff changeset
   165
        val Const (c, _) = ProofContext.read_const_proper ctxt true raw_c;
35139
e1a226a191b6 misc tuning and simplification;
wenzelm
parents: 35111
diff changeset
   166
        val const = Const (c, Consts.instance (ProofContext.consts_of ctxt) (c, Ts));
e1a226a191b6 misc tuning and simplification;
wenzelm
parents: 35111
diff changeset
   167
      in ML_Syntax.atomic (ML_Syntax.print_term const) end));
27340
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   168
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   169
end;
3de9f20f4e28 Common ML antiquotations.
wenzelm
parents:
diff changeset
   170