# HG changeset patch
# User wenzelm
# Date 1393788020 -3600
# Node ID ee71b2687c4bfa3c3efdc4a0865a2b95840599f1
# Parent  e120a15b0ee6a3993d5fe2d4c4c026fbbd10d6c9
more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;

diff -r e120a15b0ee6 -r ee71b2687c4b src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 02 19:45:38 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 02 20:20:20 2014 +0100
@@ -377,11 +377,15 @@
 fun read_class ctxt text =
   let
     val tsig = tsig_of ctxt;
-    val (s, pos) = Symbol_Pos.source_content (Syntax.read_token text);
-    val c = Type.cert_class tsig (Type.intern_class tsig s)
-      handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
-    val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
-  in c end;
+    val class_space = Type.class_space tsig;
+
+    val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+    val name = Type.cert_class tsig (Type.intern_class tsig xname)
+      handle TYPE (msg, _, _) =>
+       (Completion.report (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos));
+        error (msg ^ Position.here pos));
+    val _ = Context_Position.report ctxt pos (Name_Space.markup class_space name);
+  in name end;
 
 
 (* types *)