allow multiple inheritance of targets

--- a/src/Doc/Codegen/Adaptation.thy	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Doc/Codegen/Adaptation.thy	Fri Dec 05 19:35:36 2014 +0100
@@ -2,8 +2,8 @@
 imports Setup
 begin
 
-setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", I))
-  #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", I)) *}
+setup %invisible {* Code_Target.add_derived_target ("\<SML>", [("SML", I)])
+  #> Code_Target.add_derived_target ("\<SMLdummy>", [("Haskell", I)]) *}
 
 section {* Adaptation to target languages \label{sec:adaptation} *}
 

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Dec 05 19:35:36 2014 +0100
@@ -697,9 +697,9 @@
 
 in
 
-Code_Target.extend_target ("SML_imp", ("SML", imp_program))
-#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
-#> Code_Target.extend_target ("Scala_imp", ("Scala", imp_program))
+Code_Target.add_derived_target ("SML_imp", [("SML", imp_program)])
+#> Code_Target.add_derived_target ("OCaml_imp", [("OCaml", imp_program)])
+#> Code_Target.add_derived_target ("Scala_imp", [("Scala", imp_program)])
 
 end
 

--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Dec 05 19:35:36 2014 +0100
@@ -11,7 +11,7 @@
 
 subsubsection {* Code generation setup *}
 
-setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, I)) *}
+setup {* Code_Target.add_derived_target ("Haskell_Quickcheck", [(Code_Haskell.target, I)]) *}
 
 code_printing
   code_module Typerep \<rightharpoonup> (Haskell_Quickcheck) {*

--- a/src/HOL/Quickcheck_Random.thy	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/HOL/Quickcheck_Random.thy	Fri Dec 05 19:35:36 2014 +0100
@@ -9,7 +9,7 @@
 notation fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
-setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, I)) *}
+setup {* Code_Target.add_derived_target ("Quickcheck", [(Code_Runtime.target, I)]) *}
 
 subsection {* Catching Match exceptions *}
 

--- a/src/Tools/Code/code_haskell.ML	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML	Fri Dec 05 19:35:36 2014 +0100
@@ -499,7 +499,7 @@
       Toplevel.theory (add_monad target raw_bind)));
 
 val setup =
-  Code_Target.add_target
+  Code_Target.add_language
     (target, { serializer = serializer, literals = literals,
       check = { env_var = "ISABELLE_GHC", make_destination = I,
         make_command = fn module_name =>

--- a/src/Tools/Code/code_ml.ML	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Tools/Code/code_ml.ML	Fri Dec 05 19:35:36 2014 +0100
@@ -861,13 +861,13 @@
   );
 
 val setup =
-  Code_Target.add_target
+  Code_Target.add_language
     (target_SML, { serializer = serializer_sml, literals = literals_sml,
       check = { env_var = "ISABELLE_PROCESS",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
         make_command = fn _ =>
           "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
-  #> Code_Target.add_target
+  #> Code_Target.add_language
     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
       check = { env_var = "ISABELLE_OCAML",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),

--- a/src/Tools/Code/code_runtime.ML	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Dec 05 19:35:36 2014 +0100
@@ -68,7 +68,7 @@
 datatype truth = Holds;
 
 val _ = Theory.setup
-  (Code_Target.extend_target (target, (Code_ML.target_SML, I))
+  (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)])
   #> Code_Target.set_printings (Type_Constructor (@{type_name prop},
     [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
   #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds},

--- a/src/Tools/Code/code_scala.ML	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Tools/Code/code_scala.ML	Fri Dec 05 19:35:36 2014 +0100
@@ -424,7 +424,7 @@
 (** Isar setup **)
 
 val setup =
-  Code_Target.add_target
+  Code_Target.add_language
     (target, { serializer = serializer, literals = literals,
       check = { env_var = "SCALA_HOME",
         make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),

--- a/src/Tools/Code/code_target.ML	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Fri Dec 05 19:35:36 2014 +0100
@@ -34,12 +34,10 @@
 
   type serializer
   type literals = Code_Printer.literals
-  val add_target: string * { serializer: serializer, literals: literals,
-    check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
-    -> theory -> theory
-  val extend_target: string *
-      (string * (Code_Thingol.program -> Code_Thingol.program))
-    -> theory -> theory
+  type language
+  type ancestry
+  val add_language: string * language -> theory -> theory
+  val add_derived_target: string * ancestry -> theory -> theory
   val assert_target: Proof.context -> string -> string
   val the_literals: Proof.context -> string -> literals
   type serialization
@@ -208,6 +206,8 @@
 fun exists_target thy = Symtab.defined (fst (Targets.get thy));
 fun lookup_target_data thy = Symtab.lookup (fst (Targets.get thy));
 
+fun fold1 f xs = fold f (tl xs) (hd xs);
+
 fun join_ancestry thy target_name =
   let
     val the_target_data = the o lookup_target_data thy;
@@ -216,8 +216,7 @@
     val modifies = rev (map snd ancestry);
     val modify = fold (curry (op o)) modifies I;
     val datas = rev (map (snd o the_target_data o fst) ancestry) @ [this_data];
-    val data = fold (fn data' => fn data => Code_Printer.merge_data (data, data'))
-      (tl datas) (hd datas);
+    val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas;
   in (modify, (target, data)) end;
 
 fun assert_target ctxt target_name =
@@ -235,17 +234,26 @@
     |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data))  
   end;
 
-fun add_target (target_name, language) =
+fun add_language (target_name, language) =
   allocate_target target_name { serial = serial (), language = language, ancestry = [] };
 
-fun extend_target (target_name, (super, modify)) thy =
+fun add_derived_target (target_name, initial_ancestry) thy =
   let
-    val super_base = case lookup_target_data thy super of
-      NONE => error ("Unknown code target language: " ^ quote super)
-    | SOME (super_base, _) => super_base;
+    val _ = if null initial_ancestry
+      then error "Must derive from existing target(s)" else ();
+    fun the_target_data target_name' = case lookup_target_data thy target_name' of
+      NONE => error ("Unknown code target language: " ^ quote target_name')
+    | SOME target_data' => target_data';
+    val targets = rev (map (fst o the_target_data o fst) initial_ancestry);
+    val supremum = fold1 (fn target' => fn target =>
+      if #serial target = #serial target'
+      then target else error "Incompatible targets") targets;
+    val ancestries = map #ancestry targets @ [initial_ancestry];
+    val ancestry = fold1 (fn ancestry' => fn ancestry =>
+      merge_ancestry (ancestry, ancestry')) ancestries;
   in
-    allocate_target target_name { serial = #serial super_base, language = #language super_base,
-      ancestry = (super, modify) :: #ancestry super_base } thy 
+    allocate_target target_name { serial = #serial supremum, language = #language supremum,
+      ancestry = ancestry } thy 
   end;
   
 fun map_data target_name f thy =