src/Tools/Code/code_target.ML
changeset 55149 626d8f08d479
parent 55147 bce3dbc11f95
child 55150 0940309ed8f1
     1.1 --- a/src/Tools/Code/code_target.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -202,7 +202,7 @@
     1.4    description: description,
     1.5    reserved: string list,
     1.6    identifiers: identifier_data,
     1.7 -  printings: (Code_Printer.const_syntax, Code_Printer.tyco_syntax, string, unit, unit,
     1.8 +  printings: (Code_Printer.activated_const_syntax, Code_Printer.tyco_syntax, string, unit, unit,
     1.9      (Pretty.T * string list)) Code_Symbol.data
    1.10  };
    1.11  
    1.12 @@ -325,11 +325,6 @@
    1.13      val (modify, data) = collapse_hierarchy thy target;
    1.14    in (default_width, data, modify) end;
    1.15  
    1.16 -fun activate_symbol_syntax thy literals printings =
    1.17 -  (Code_Symbol.symbols_of printings,
    1.18 -    (Symtab.lookup (Code_Symbol.mapped_const_data (Code_Printer.activate_const_syntax thy literals) printings),
    1.19 -      Code_Symbol.lookup_type_constructor_data printings, Code_Symbol.lookup_type_class_data printings))
    1.20 -
    1.21  fun project_program thy syms_hidden syms1 program2 =
    1.22    let
    1.23      val ctxt = Proof_Context.init_global thy;
    1.24 @@ -344,11 +339,10 @@
    1.25      val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
    1.26    in (syms4, program4) end;
    1.27  
    1.28 -fun prepare_serializer thy (serializer : serializer) literals reserved identifiers
    1.29 +fun prepare_serializer thy (serializer : serializer) reserved identifiers
    1.30      printings module_name args proto_program syms =
    1.31    let
    1.32 -    val (syms_hidden, (const_syntax, tyco_syntax, class_syntax)) =
    1.33 -      activate_symbol_syntax thy literals printings;
    1.34 +    val syms_hidden = Code_Symbol.symbols_of printings;
    1.35      val (syms_all, program) = project_program thy syms_hidden syms proto_program;
    1.36      fun select_include (name, (content, cs)) =
    1.37        if null cs orelse exists (fn c => member (op =) syms_all (Code_Symbol.Constant c)) cs
    1.38 @@ -360,9 +354,9 @@
    1.39        reserved_syms = reserved,
    1.40        identifiers = identifiers,
    1.41        includes = includes,
    1.42 -      const_syntax = const_syntax,
    1.43 -      tyco_syntax = tyco_syntax,
    1.44 -      class_syntax = class_syntax },
    1.45 +      const_syntax = Code_Symbol.lookup_constant_data printings,
    1.46 +      tyco_syntax = Code_Symbol.lookup_type_constructor_data printings,
    1.47 +      class_syntax = Code_Symbol.lookup_type_class_data printings },
    1.48        program)
    1.49    end;
    1.50  
    1.51 @@ -372,7 +366,7 @@
    1.52      val serializer = case the_description data
    1.53       of Fundamental seri => #serializer seri;
    1.54      val (prepared_serializer, prepared_program) =
    1.55 -      prepare_serializer thy serializer (the_literals thy target)
    1.56 +      prepare_serializer thy serializer
    1.57          (the_reserved data) (the_identifiers data) (the_printings data)
    1.58          module_name args (modify program) syms
    1.59      val width = the_default default_width some_width;
    1.60 @@ -559,12 +553,12 @@
    1.61  
    1.62  (* checking of syntax *)
    1.63  
    1.64 -fun check_const_syntax thy c syn =
    1.65 +fun check_const_syntax thy target c syn =
    1.66    if Code_Printer.requires_args syn > Code.args_number thy c
    1.67    then error ("Too many arguments in syntax for constant " ^ quote c)
    1.68 -  else syn;
    1.69 +  else Code_Printer.activate_const_syntax thy (the_literals thy target) c syn;
    1.70  
    1.71 -fun check_tyco_syntax thy tyco syn =
    1.72 +fun check_tyco_syntax thy target tyco syn =
    1.73    if fst syn <> Sign.arity_number thy tyco
    1.74    then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
    1.75    else syn;
    1.76 @@ -608,12 +602,12 @@
    1.77  fun arrange_printings prep_const thy =
    1.78    let
    1.79      fun arrange check (sym, target_syns) =
    1.80 -      map (fn (target, some_syn) => (target, (sym, Option.map (check thy sym) some_syn))) target_syns;
    1.81 +      map (fn (target, some_syn) => (target, (sym, Option.map (check thy target sym) some_syn))) target_syns;
    1.82    in
    1.83      Code_Symbol.maps_attr'
    1.84        (arrange check_const_syntax) (arrange check_tyco_syntax)
    1.85 -        (arrange ((K o K) I)) (arrange ((K o K) I)) (arrange ((K o K) I))
    1.86 -        (arrange (fn thy => fn _ => fn (raw_content, raw_cs) =>
    1.87 +        (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
    1.88 +        (arrange (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) =>
    1.89            (Code_Printer.str raw_content, map (prep_const thy) raw_cs)))
    1.90    end;
    1.91  
    1.92 @@ -633,7 +627,7 @@
    1.93    let
    1.94      val _ = legacy_feature "prefer \"code_printing\" for custom serialisations"
    1.95      val x = prep_x thy raw_x;
    1.96 -  in set_printing (target, Symbol (x, Option.map (prep_syn thy x) some_raw_syn)) thy end;
    1.97 +  in set_printing (target, Symbol (x, Option.map (prep_syn thy target x) some_raw_syn)) thy end;
    1.98  
    1.99  fun gen_add_const_syntax prep_const =
   1.100    gen_add_syntax Code_Symbol.Constant prep_const check_const_syntax;
   1.101 @@ -642,14 +636,14 @@
   1.102    gen_add_syntax Code_Symbol.Type_Constructor prep_tyco check_tyco_syntax;
   1.103  
   1.104  fun gen_add_class_syntax prep_class =
   1.105 -  gen_add_syntax Code_Symbol.Type_Class prep_class ((K o K) I);
   1.106 +  gen_add_syntax Code_Symbol.Type_Class prep_class ((K o K o K) I);
   1.107  
   1.108  fun gen_add_instance_syntax prep_inst =
   1.109 -  gen_add_syntax Code_Symbol.Class_Instance prep_inst ((K o K) I);
   1.110 +  gen_add_syntax Code_Symbol.Class_Instance prep_inst ((K o K o K) I);
   1.111  
   1.112  fun gen_add_include prep_const target (name, some_content) thy =
   1.113    gen_add_syntax Code_Symbol.Module (K I)
   1.114 -    (fn thy => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
   1.115 +    (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
   1.116      target name some_content thy;
   1.117  
   1.118