# HG changeset patch
# User wenzelm
# Date 1303574967 -7200
# Node ID 1f7e39bdf0f682b4747f9cddcd6293a2c5d47dba
# Parent  bbce02fcba60866c5a6598eea0d046a2c7c68a4b
more reports and error positions;

diff -r bbce02fcba60 -r 1f7e39bdf0f6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Apr 23 17:02:12 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 23 18:09:27 2011 +0200
@@ -366,6 +366,7 @@
     val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
       handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
     val _ = Context_Position.report ctxt pos (Markup.tclass c);
+    val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
   in c end;
 
 
@@ -466,6 +467,7 @@
       if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
       else ();
     val _ = Context_Position.report ctxt pos (Markup.const d);
+    val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
   in t end;
 
 in
@@ -481,14 +483,15 @@
     else
       let
         val d = intern_type ctxt c;
-        val decl = Type.the_decl tsig d;
-        val _ = Context_Position.report ctxt pos (Markup.tycon d);
-        fun err () = error ("Bad type name: " ^ quote d);
+        val decl = Type.the_decl tsig d handle ERROR msg => error (msg ^ Position.str_of pos);
+        fun err () = error ("Bad type name: " ^ quote d ^ Position.str_of pos);
         val args =
           (case decl of
             Type.LogicalType n => n
           | Type.Abbreviation (vs, _, _) => if strict then err () else length vs
           | Type.Nonterminal => if strict then err () else 0);
+        val _ = Context_Position.report ctxt pos (Markup.tycon d);
+        val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.type_space tsig) d);
       in Type (d, replicate args dummyT) end
   end;