read_class: perform actual read, with source position;

--- a/src/Pure/sign.ML	Sat Feb 27 13:32:05 2010 +0100
+++ b/src/Pure/sign.ML	Sat Feb 27 13:32:18 2010 +0100
@@ -404,8 +404,13 @@
 
 (* classes *)
 
-fun read_class thy c = certify_class thy (intern_class thy c)
-  handle TYPE (msg, _, _) => error msg;
+fun read_class thy text =
+  let
+    val (syms, pos) = Syntax.read_token text;
+    val c = certify_class thy (intern_class thy (Symbol_Pos.content syms))
+      handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
+    val _ = Position.report (Markup.tclass c) pos;
+  in c end;
 
 
 (* type arities *)