# HG changeset patch
# User wenzelm
# Date 1267273958 -3600
# Node ID 041bb8d18916ea1ca11a641eac0d83f383cc6966
# Parent  ba804f4c82c647a177e24654d435a320b489c240
ML antiquotations for type classes;

diff -r ba804f4c82c6 -r 041bb8d18916 NEWS
--- a/NEWS	Sat Feb 27 13:32:18 2010 +0100
+++ b/NEWS	Sat Feb 27 13:32:38 2010 +0100
@@ -177,6 +177,11 @@
 
 *** ML ***
 
+* Antiquotations for type classes:
+
+    @{class NAME}         -- type class
+    @{class_syntax NAME}  -- syntax representation of any of the above
+
 * Antiquotations for type constructors:
 
     @{type_name NAME}     -- logical type (as before)
diff -r ba804f4c82c6 -r 041bb8d18916 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sat Feb 27 13:32:18 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Sat Feb 27 13:32:38 2010 +0100
@@ -73,9 +73,6 @@
 
 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
 
-val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
-  ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
-
 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
 val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
@@ -103,6 +100,20 @@
     "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
 
 
+(* type classes *)
+
+fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) =>
+  Sign.read_class thy s
+  |> syn ? Long_Name.base_name   (* FIXME authentic syntax *)
+  |> ML_Syntax.print_string);
+
+val _ = inline "class" (class false);
+val _ = inline "class_syntax" (class true);
+
+val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
+  ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
+
+
 (* type constructors *)
 
 fun type_const kind check = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>