# HG changeset patch
# User wenzelm
# Date 1267273938 -3600
# Node ID ba804f4c82c647a177e24654d435a320b489c240
# Parent  11f58c600707fdeed0a66238674d8d7d58df06e2
read_class: perform actual read, with source position;

diff -r 11f58c600707 -r ba804f4c82c6 src/Pure/sign.ML
--- 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 *)