# HG changeset patch
# User wenzelm
# Date 1292621036 -3600
# Node ID 78c3e472bb35c9942603838d559db662d6c0a4d1
# Parent  42f24340ae53a5e08f86690547773e17431414ed
extra checking of name bindings for classes, types, consts;
tuned;

diff -r 42f24340ae53 -r 78c3e472bb35 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Fri Dec 17 20:21:35 2010 +0100
+++ b/src/Pure/General/binding.ML	Fri Dec 17 22:23:56 2010 +0100
@@ -30,6 +30,8 @@
   val prefix: bool -> string -> binding -> binding
   val conceal: binding -> binding
   val str_of: binding -> string
+  val bad: binding -> string
+  val check: binding -> unit
 end;
 
 structure Binding: BINDING =
@@ -127,6 +129,16 @@
   qualified_name_of binding
   |> Markup.markup (Position.markup (pos_of binding) (Markup.binding (name_of binding)));
 
+
+(* check *)
+
+fun bad binding =
+  "Bad name binding: " ^ quote (str_of binding) ^ Position.str_of (pos_of binding);
+
+fun check binding =
+  if Symbol.is_ident (Symbol.explode (name_of binding)) then ()
+  else legacy_feature (bad binding);
+
 end;
 end;
 
diff -r 42f24340ae53 -r 78c3e472bb35 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Dec 17 20:21:35 2010 +0100
+++ b/src/Pure/General/name_space.ML	Fri Dec 17 22:23:56 2010 +0100
@@ -266,11 +266,11 @@
 
 (* full name *)
 
+fun err_bad binding = error (Binding.bad binding);
+
 fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
   | transform_binding _ = I;
 
-fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
-
 fun name_spec (naming as Naming {path, ...}) raw_binding =
   let
     val binding = transform_binding naming raw_binding;
diff -r 42f24340ae53 -r 78c3e472bb35 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri Dec 17 20:21:35 2010 +0100
+++ b/src/Pure/consts.ML	Fri Dec 17 22:23:56 2010 +0100
@@ -235,6 +235,7 @@
   map_consts (fn (decls, constraints, rev_abbrevs) =>
     let
       val decl = {T = declT, typargs = typargs_of declT};
+      val _ = Binding.check b;
       val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
@@ -287,6 +288,7 @@
       let
         val decl = {T = T, typargs = typargs_of T};
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
+        val _ = Binding.check b;
         val (_, decls') = decls
           |> Name_Space.define true naming (b, (decl, SOME abbr));
         val rev_abbrevs' = rev_abbrevs
diff -r 42f24340ae53 -r 78c3e472bb35 src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Dec 17 20:21:35 2010 +0100
+++ b/src/Pure/type.ML	Fri Dec 17 22:23:56 2010 +0100
@@ -418,10 +418,10 @@
 
 fun typ_match tsig =
   let
-    fun match (T0 as TVar (v, S), T) subs = 
+    fun match (T0 as TVar (v, S), T) subs =
           (case lookup subs (v, S) of
             NONE =>
-              if of_sort tsig (T, S) 
+              if of_sort tsig (T, S)
               then if T0 = T then subs (*types already identical; don't create cycle!*)
                    else Vartab.update_new (v, (S, T)) subs
               else raise TYPE_MATCH
@@ -582,6 +582,7 @@
     let
       val cs' = map (cert_class tsig) cs
         handle TYPE (msg, _, _) => error msg;
+      val _ = Binding.check c;
       val (c', space') = space |> Name_Space.declare true naming c;
       val classes' = classes |> Sorts.add_class pp (c', cs');
     in ((space', classes'), default, types) end);
@@ -627,7 +628,7 @@
 local
 
 fun new_decl naming (c, decl) types =
-  #2 (Name_Space.define true naming (c, decl) types);
+  (Binding.check c; #2 (Name_Space.define true naming (c, decl) types));
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let