1.1 --- a/src/Pure/Isar/new_locale.ML	Thu Nov 27 10:26:00 2008 +0100
     1.2 +++ b/src/Pure/Isar/new_locale.ML	Thu Nov 27 10:28:27 2008 +0100
     1.3 @@ -35,6 +35,7 @@
     1.4    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
     1.5    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
     1.6    val add_declaration: string -> declaration -> Proof.context -> Proof.context
     1.7 +  val add_dependency: string -> (string * Morphism.morphism) -> Proof.context -> Proof.context
     1.8  
     1.9    (* Activate locales *)
    1.10    val activate_declarations: theory -> string * Morphism.morphism ->
    1.11 @@ -172,28 +173,24 @@
    1.12  
    1.13  val empty = (Idtab.empty : identifiers);
    1.14  
    1.15 -fun roundup thy (deps, marked) =
    1.16 -(* FIXME simplify code: should probably only get one dep as argument *)
    1.17 +fun add thy (name, morph) (deps, marked) =
    1.18    let
    1.19 -    fun add (name, morph) (deps, marked) =
    1.20 +    val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name;
    1.21 +    val instance = params |>
    1.22 +      map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph);
    1.23 +  in
    1.24 +    if Idtab.defined marked (name, instance)
    1.25 +    then (deps, marked)
    1.26 +    else
    1.27        let
    1.28 -        val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name;
    1.29 -        val instance = params |>
    1.30 -          map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph);
    1.31 +        val dependencies' =
    1.32 +          map (fn ((name, morph'), _) => (name, morph' $>  morph)) dependencies;
    1.33 +        val marked' = Idtab.insert (op =) ((name, instance), ()) marked;
    1.34 +        val (deps', marked'') = fold_rev (add thy) dependencies' ([], marked');
    1.35        in
    1.36 -        if Idtab.defined marked (name, instance)
    1.37 -        then (deps, marked)
    1.38 -        else
    1.39 -          let
    1.40 -            val dependencies' =
    1.41 -              map (fn ((name, morph'), _) => (name, morph' $>  morph)) dependencies;
    1.42 -            val marked' = Idtab.insert (op =) ((name, instance), ()) marked;
    1.43 -            val (deps', marked'') = fold_rev add dependencies' ([], marked');
    1.44 -          in
    1.45 -            (cons (name, morph) deps' @ deps, marked'')
    1.46 -          end
    1.47 +        ((name, morph) :: deps' @ deps, marked'')
    1.48        end
    1.49 -  in fold_rev add deps ([], marked) end;
    1.50 +  end;
    1.51  
    1.52  end;
    1.53  
    1.54 @@ -210,11 +207,9 @@
    1.55    let
    1.56      val name' = intern thy name;
    1.57      val Loc {dependencies, ...} = the_locale thy name';
    1.58 -    val (dependencies', marked) =
    1.59 -      roundup thy ((name', morph) ::
    1.60 -        map (fn ((n, morph'), _) => (n, morph' $> morph)) dependencies, marked);
    1.61 +    val (dependencies', marked') = add thy (name', morph) ([], marked);
    1.62    in
    1.63 -    (marked, ctxt |> fold_rev (activate_decls thy) dependencies')
    1.64 +    (marked', ctxt |> fold_rev (activate_decls thy) dependencies')
    1.65    end;
    1.66  
    1.67  fun activate_notes activ_elem thy (name, morph) input =
    1.68 @@ -232,11 +227,9 @@
    1.69    let
    1.70      val name' = intern thy name;
    1.71      val Loc {dependencies, ...} = the_locale thy name';
    1.72 -    val (dependencies', marked) =
    1.73 -      roundup thy ((name', morph) ::
    1.74 -        map (fn ((n, morph'), _) => (n, morph' $> morph)) dependencies, marked);
    1.75 +    val (dependencies', marked') = add thy (name', morph) ([], marked);
    1.76    in
    1.77 -    (marked, ctxt |> fold_rev (activate_notes activ_elem thy) dependencies')
    1.78 +    (marked', ctxt |> fold_rev (activate_notes activ_elem thy) dependencies')
    1.79    end;
    1.80  
    1.81  fun activate name thy activ_elem input =
    1.82 @@ -244,8 +237,6 @@
    1.83      val name' = intern thy name;
    1.84      val Loc {parameters = (_, params), spec = (asm, defs), dependencies, ...} =
    1.85        the_locale thy name';
    1.86 -    val dependencies' =
    1.87 -      (name', Morphism.identity) :: fst (roundup thy (map fst dependencies, empty));
    1.88    in
    1.89      input |>
    1.90        (if not (null params) then activ_elem (Fixes params) else I) |>
    1.91 @@ -337,5 +328,12 @@
    1.92  
    1.93  end;
    1.94  
    1.95 +(* Dependencies *)
    1.96 +
    1.97 +fun add_dependency loc dep =
    1.98 +  ProofContext.theory (change_locale loc
    1.99 +    (fn (parameters, spec, decls, notes, dependencies) =>
   1.100 +      (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies)));
   1.101 +
   1.102  end;
   1.103