# HG changeset patch
# User haftmann
# Date 1285926369 -7200
# Node ID 5228c6b2027374e89c88716791b42faf8f2951e5
# Parent  c7cec137c48a84886854121bd766f731bd07df5c
check whole target hierarchy for existing reserved symbols

diff -r c7cec137c48a -r 5228c6b20273 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri Oct 01 11:46:09 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Oct 01 11:46:09 2010 +0200
@@ -244,12 +244,10 @@
 
 fun the_literals thy = #literals o the_fundamental thy;
 
-local
-
-fun activate_target thy target =
+fun collapse_hierarchy thy =
   let
-    val ((targets, abortable), default_width) = Targets.get thy;
-    fun collapse_hierarchy target =
+    val ((targets, _), _) = Targets.get thy;
+    fun collapse target = 
       let
         val data = case Symtab.lookup targets target
          of SOME data => data
@@ -257,10 +255,17 @@
       in case the_description data
        of Fundamental _ => (K I, data)
         | Extension (super, modify) => let
-            val (modify', data') = collapse_hierarchy super
+            val (modify', data') = collapse super
           in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end
       end;
-    val (modify, data) = collapse_hierarchy target;
+  in collapse end;
+
+local
+
+fun activate_target thy target =
+  let
+    val ((targets, abortable), default_width) = Targets.get thy;
+    val (modify, data) = collapse_hierarchy thy target;
   in (default_width, abortable, data, modify) end;
 
 fun activate_syntax lookup_name src_tab = Symtab.empty
@@ -537,12 +542,16 @@
       then error ("Too many arguments in syntax for constant " ^ quote c)
       else syn);
 
-fun add_reserved target =
+fun add_reserved target sym thy =
   let
-    fun add sym syms = if member (op =) syms sym
+    val (_, data) = collapse_hierarchy thy target;
+    val _ = if member (op =) (the_reserved data) sym
       then error ("Reserved symbol " ^ quote sym ^ " already declared")
-      else insert (op =) sym syms
-  in map_reserved target o add end;
+      else ();
+  in
+    thy
+    |> map_reserved target (insert (op =) sym)
+  end;
 
 fun gen_add_include read_const target args thy =
   let