src/Tools/Code/code_target.ML
changeset 38917 c7da3cc88135
parent 38916 c0b857a04758
child 38918 48d62f237944
equal deleted inserted replaced
38916:c0b857a04758 38917:c7da3cc88135
    23   type serialization
    23   type serialization
    24   val parse_args: 'a parser -> Token.T list -> 'a
    24   val parse_args: 'a parser -> Token.T list -> 'a
    25   val serialization: (int -> Path.T option -> 'a -> unit)
    25   val serialization: (int -> Path.T option -> 'a -> unit)
    26     -> (int -> 'a -> string * string option list)
    26     -> (int -> 'a -> string * string option list)
    27     -> 'a -> int -> serialization
    27     -> 'a -> int -> serialization
       
    28 
    28   val serialize: theory -> string -> int option -> string option -> Token.T list
    29   val serialize: theory -> string -> int option -> string option -> Token.T list
    29     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    30     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    30   val serialize_custom: theory -> string * serializer -> string option
    31   val serialize_custom: theory -> string * serializer -> string option
    31     -> Code_Thingol.naming -> Code_Thingol.program -> string list
    32     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    32     -> string * string option list
    33   val check: theory -> string list
    33   val the_literals: theory -> string -> literals
    34     -> Code_Thingol.naming -> Code_Thingol.program -> string -> bool -> Token.T list -> unit
    34   val file: Path.T option -> serialization -> unit
       
    35   val string: string list -> serialization -> string
       
    36   val code_of: theory -> string -> int option -> string
    35   val code_of: theory -> string -> int option -> string
    37     -> string list -> (Code_Thingol.naming -> string list) -> string
    36     -> string list -> (Code_Thingol.naming -> string list) -> string * string option list
    38   val set_default_code_width: int -> theory -> theory
    37   val set_default_code_width: int -> theory -> theory
    39   val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    38   val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
       
    39   val the_literals: theory -> string -> literals
    40 
    40 
    41   val allow_abort: string -> theory -> theory
    41   val allow_abort: string -> theory -> theory
    42   type tyco_syntax = Code_Printer.tyco_syntax
    42   type tyco_syntax = Code_Printer.tyco_syntax
    43   type const_syntax = Code_Printer.const_syntax
    43   type const_syntax = Code_Printer.const_syntax
    44   val add_syntax_class: string -> class -> string option -> theory -> theory
    44   val add_syntax_class: string -> class -> string option -> theory -> theory
    62 (** basics **)
    62 (** basics **)
    63 
    63 
    64 datatype destination = File of Path.T option | String of string list;
    64 datatype destination = File of Path.T option | String of string list;
    65 type serialization = destination -> (string * string option list) option;
    65 type serialization = destination -> (string * string option list) option;
    66 
    66 
    67 fun file some_path f = (f (File some_path); ());
       
    68 fun string stmt_names f = fst (the (f (String stmt_names)));
       
    69 
       
    70 fun stmt_names_of_destination (String stmt_names) = stmt_names
    67 fun stmt_names_of_destination (String stmt_names) = stmt_names
    71   | stmt_names_of_destination _ = [];
    68   | stmt_names_of_destination _ = [];
    72 
    69 
    73 fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
    70 fun serialization output _ pretty width (File some_path) = (output width some_path pretty; NONE)
    74   | serialization _ string pretty width (String _) = SOME (string width pretty);
    71   | serialization _ string pretty width (String _) = SOME (string width pretty);
       
    72 
       
    73 fun file some_path f = f (File some_path);
       
    74 fun string stmt_names f = the (f (String stmt_names));
    75 
    75 
    76 
    76 
    77 (** theory data **)
    77 (** theory data **)
    78 
    78 
    79 datatype name_syntax_table = NameSyntaxTable of {
    79 datatype name_syntax_table = NameSyntaxTable of {