src/Tools/Code/code_target.ML
changeset 38926 24f82786cc57
parent 38925 ced825abdc1d
child 38927 544f4702d621
equal deleted inserted replaced
38925:ced825abdc1d 38926:24f82786cc57
    99        Symreltab.join (K snd) (instance1, instance2)),
    99        Symreltab.join (K snd) (instance1, instance2)),
   100     (Symtab.join (K snd) (tyco1, tyco2),
   100     (Symtab.join (K snd) (tyco1, tyco2),
   101        Symtab.join (K snd) (const1, const2))
   101        Symtab.join (K snd) (const1, const2))
   102   );
   102   );
   103 
   103 
   104 type serializer = Token.T list          (*arguments*)
   104 type serializer = Token.T list (*arguments*) -> {
   105   -> (string -> string)                 (*labelled_name*)
   105     labelled_name: string -> string,
   106   -> string list                        (*reserved symbols*)
   106     reserved_syms: string list,
   107   -> (string * Pretty.T) list           (*includes*)
   107     includes: (string * Pretty.T) list,
   108   -> bool                               (*singleton module*)
   108     single_module: bool,
   109   -> (string -> string option)          (*module aliasses*)
   109     module_alias: string -> string option,
   110   -> (string -> string option)          (*class syntax*)
   110     class_syntax: string -> string option,
   111   -> (string -> Code_Printer.tyco_syntax option)
   111     tyco_syntax: string -> Code_Printer.tyco_syntax option,
   112   -> (string -> Code_Printer.activated_const_syntax option)
   112     const_syntax: string -> Code_Printer.activated_const_syntax option,
   113   -> Code_Thingol.program
   113     program: Code_Thingol.program,
   114   -> (string list * string list)        (*selected statements*)
   114     names: string list,
       
   115     presentation_names: string list }
   115   -> serialization;
   116   -> serialization;
   116 
   117 
   117 datatype description = Fundamental of { serializer: serializer,
   118 datatype description = Fundamental of { serializer: serializer,
   118       literals: literals,
   119       literals: literals,
   119       check: { env_var: string, make_destination: Path.T -> Path.T,
   120       check: { env_var: string, make_destination: Path.T -> Path.T,
   275     val empty_funs = filter_out (member (op =) abortable)
   276     val empty_funs = filter_out (member (op =) abortable)
   276       (Code_Thingol.empty_funs program3);
   277       (Code_Thingol.empty_funs program3);
   277     val _ = if null empty_funs then () else error ("No code equations for "
   278     val _ = if null empty_funs then () else error ("No code equations for "
   278       ^ commas (map (Sign.extern_const thy) empty_funs));
   279       ^ commas (map (Sign.extern_const thy) empty_funs));
   279   in
   280   in
   280     serializer args (Code_Thingol.labelled_name thy program2) reserved includes
   281     serializer args {
   281       (is_some module_name) (if is_some module_name then K module_name else Symtab.lookup module_alias)
   282       labelled_name = Code_Thingol.labelled_name thy program2,
   282       (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
   283       reserved_syms = reserved,
   283       program4 (names1, presentation_names) width
   284       includes = includes,
       
   285       single_module = is_some module_name,
       
   286       module_alias = if is_some module_name then K module_name else Symtab.lookup module_alias,
       
   287       class_syntax = Symtab.lookup class',
       
   288       tyco_syntax = Symtab.lookup tyco',
       
   289       const_syntax = Symtab.lookup const',
       
   290       program = program3,
       
   291       names = names1,
       
   292       presentation_names = presentation_names } width
   284   end;
   293   end;
   285 
   294 
   286 fun mount_serializer thy target some_width raw_module_name args naming program names destination =
   295 fun mount_serializer thy target some_width raw_module_name args naming program names destination =
   287   let
   296   let
   288     val ((targets, abortable), default_width) = Targets.get thy;
   297     val ((targets, abortable), default_width) = Targets.get thy;