src/Tools/Code/code_target.ML
changeset 34248 6fb7dd3fd81a
parent 34173 458ced35abb8
child 36121 86b952fc31da
     1.1 --- a/src/Tools/Code/code_target.ML	Mon Jan 04 14:09:57 2010 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Jan 04 14:09:58 2010 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4  fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
     1.5  fun the_module_alias (Target { module_alias , ... }) = module_alias;
     1.6  
     1.7 -structure CodeTargetData = Theory_Data
     1.8 +structure Targets = Theory_Data
     1.9  (
    1.10    type T = (target Symtab.table * string list) * int;
    1.11    val empty = ((Symtab.empty, []), 80);
    1.12 @@ -163,17 +163,17 @@
    1.13        Library.merge (op =) (exc1, exc2)), Int.max (width1, width2));
    1.14  );
    1.15  
    1.16 -val abort_allowed = snd o fst o CodeTargetData.get;
    1.17 +val abort_allowed = snd o fst o Targets.get;
    1.18  
    1.19 -val the_default_width = snd o CodeTargetData.get;
    1.20 +val the_default_width = snd o Targets.get;
    1.21  
    1.22 -fun assert_target thy target = if Symtab.defined ((fst o fst) (CodeTargetData.get thy)) target
    1.23 +fun assert_target thy target = if Symtab.defined ((fst o fst) (Targets.get thy)) target
    1.24    then target
    1.25    else error ("Unknown code target language: " ^ quote target);
    1.26  
    1.27  fun put_target (target, seri) thy =
    1.28    let
    1.29 -    val lookup_target = Symtab.lookup ((fst o fst) (CodeTargetData.get thy));
    1.30 +    val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
    1.31      val _ = case seri
    1.32       of Extends (super, _) => if is_some (lookup_target super) then ()
    1.33            else error ("Unknown code target language: " ^ quote super)
    1.34 @@ -189,11 +189,10 @@
    1.35        else (); 
    1.36    in
    1.37      thy
    1.38 -    |> (CodeTargetData.map o apfst o apfst oo Symtab.map_default)
    1.39 +    |> (Targets.map o apfst o apfst o Symtab.update)
    1.40            (target, make_target ((serial (), seri), (([], Symtab.empty),
    1.41              (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
    1.42                Symtab.empty))))
    1.43 -          ((map_target o apfst o apsnd o K) seri)
    1.44    end;
    1.45  
    1.46  fun add_target (target, seri) = put_target (target, Serializer seri);
    1.47 @@ -205,7 +204,7 @@
    1.48      val _ = assert_target thy target;
    1.49    in
    1.50      thy
    1.51 -    |> (CodeTargetData.map o apfst o apfst o Symtab.map_entry target o map_target) f
    1.52 +    |> (Targets.map o apfst o apfst o Symtab.map_entry target o map_target) f
    1.53    end;
    1.54  
    1.55  fun map_reserved target =
    1.56 @@ -217,7 +216,7 @@
    1.57  fun map_module_alias target =
    1.58    map_target_data target o apsnd o apsnd o apsnd;
    1.59  
    1.60 -fun set_default_code_width k = (CodeTargetData.map o apsnd) (K k);
    1.61 +fun set_default_code_width k = (Targets.map o apsnd) (K k);
    1.62  
    1.63  
    1.64  (** serializer usage **)
    1.65 @@ -226,7 +225,7 @@
    1.66  
    1.67  fun the_literals thy =
    1.68    let
    1.69 -    val ((targets, _), _) = CodeTargetData.get thy;
    1.70 +    val ((targets, _), _) = Targets.get thy;
    1.71      fun literals target = case Symtab.lookup targets target
    1.72       of SOME data => (case the_serializer data
    1.73           of Serializer (_, literals) => literals
    1.74 @@ -284,7 +283,7 @@
    1.75  
    1.76  fun mount_serializer thy alt_serializer target some_width module args naming program names =
    1.77    let
    1.78 -    val ((targets, abortable), default_width) = CodeTargetData.get thy;
    1.79 +    val ((targets, abortable), default_width) = Targets.get thy;
    1.80      fun collapse_hierarchy target =
    1.81        let
    1.82          val data = case Symtab.lookup targets target
    1.83 @@ -457,7 +456,7 @@
    1.84  fun gen_allow_abort prep_const raw_c thy =
    1.85    let
    1.86      val c = prep_const thy raw_c;
    1.87 -  in thy |> (CodeTargetData.map o apfst o apsnd) (insert (op =) c) end;
    1.88 +  in thy |> (Targets.map o apfst o apsnd) (insert (op =) c) end;
    1.89  
    1.90  
    1.91  (* concrete syntax *)