# HG changeset patch
# User wenzelm
# Date 1193059495 -7200
# Node ID 57c717b9dd59843465f8dd5fd094d2b6c2b89e46
# Parent  8072027dc4bbbb684d63cab8b4f05e8115e7eac3
added @{sort}, @{type_syntax} antiquotations;

diff -r 8072027dc4bb -r 57c717b9dd59 NEWS
--- a/NEWS	Mon Oct 22 13:59:41 2007 +0200
+++ b/NEWS	Mon Oct 22 15:24:55 2007 +0200
@@ -1218,6 +1218,7 @@
 formal entities in the source, referring to the context available at
 compile-time.  For example:
 
+ML {* @{sort "{zero,one}"} *}
 ML {* @{typ "'a => 'b"} *}
 ML {* @{term "%x. x"} *}
 ML {* @{prop "x == y"} *}
@@ -1227,6 +1228,7 @@
 ML {* @{thm asm_rl} *}
 ML {* @{thms asm_rl} *}
 ML {* @{type_name c} *}
+ML {* @{type_syntax c} *}
 ML {* @{const_name c} *}
 ML {* @{const_syntax c} *}
 ML {* @{context} *}
diff -r 8072027dc4bb -r 57c717b9dd59 src/Pure/ML/ml_context.ML
--- 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 **)