--- a/src/Pure/ML/ml_context.ML Mon Oct 22 13:59:41 2007 +0200
+++ b/src/Pure/ML/ml_context.ML Mon Oct 22 15:24:55 2007 +0200
@@ -198,8 +198,15 @@
(* basic antiquotations *)
+local
+
+fun context x = (Scan.state >> Context.proof_of) x;
+
val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()"));
+val _ = inline_antiq "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) =>
+ ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
+
val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
@@ -216,11 +223,14 @@
("cprop",
"Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
-val _ = inline_antiq "type_name"
- ((Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
+fun type_ syn = (context -- Scan.lift Args.name >> (fn (ctxt, c) =>
#1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
+ |> syn ? Sign.base_name
|> ML_Syntax.print_string));
+val _ = inline_antiq "type_name" (type_ false);
+val _ = inline_antiq "type_syntax" (type_ true);
+
fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
#1 (Term.dest_Const (Consts.read_const (ProofContext.consts_of ctxt) c))
|> syn ? ProofContext.const_syntax_name ctxt
@@ -229,6 +239,7 @@
val _ = inline_antiq "const_name" (const false);
val _ = inline_antiq "const_syntax" (const true);
+in val _ = () end;
(** fact references **)