src/Tools/Code/code_target.ML
changeset 37876 48116a1764c5
parent 37844 f26becedaeb1
child 37881 096c8397c989
     1.1 --- a/src/Tools/Code/code_target.ML	Fri Jul 16 15:28:23 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Fri Jul 16 15:55:32 2010 +0200
     1.3 @@ -41,11 +41,11 @@
     1.4  
     1.5    val allow_abort: string -> theory -> theory
     1.6    type tyco_syntax = Code_Printer.tyco_syntax
     1.7 -  type proto_const_syntax = Code_Printer.proto_const_syntax
     1.8 +  type const_syntax = Code_Printer.const_syntax
     1.9    val add_syntax_class: string -> class -> string option -> theory -> theory
    1.10    val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
    1.11    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
    1.12 -  val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
    1.13 +  val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
    1.14    val add_reserved: string -> string -> theory -> theory
    1.15    val add_include: string -> string * (string * string list) option -> theory -> theory
    1.16  end;
    1.17 @@ -57,7 +57,7 @@
    1.18  
    1.19  type literals = Code_Printer.literals;
    1.20  type tyco_syntax = Code_Printer.tyco_syntax;
    1.21 -type proto_const_syntax = Code_Printer.proto_const_syntax;
    1.22 +type const_syntax = Code_Printer.const_syntax;
    1.23  
    1.24  
    1.25  (** basics **)
    1.26 @@ -83,7 +83,7 @@
    1.27    class: string Symtab.table,
    1.28    instance: unit Symreltab.table,
    1.29    tyco: Code_Printer.tyco_syntax Symtab.table,
    1.30 -  const: Code_Printer.proto_const_syntax Symtab.table
    1.31 +  const: Code_Printer.const_syntax Symtab.table
    1.32  };
    1.33  
    1.34  fun mk_name_syntax_table ((class, instance), (tyco, const)) =
    1.35 @@ -108,7 +108,7 @@
    1.36    -> (string -> string option)          (*module aliasses*)
    1.37    -> (string -> string option)          (*class syntax*)
    1.38    -> (string -> Code_Printer.tyco_syntax option)
    1.39 -  -> (string -> Code_Printer.const_syntax option)
    1.40 +  -> (string -> Code_Printer.activated_const_syntax option)
    1.41    -> ((Pretty.T -> string) * (Pretty.T -> unit))
    1.42    -> Code_Thingol.program
    1.43    -> string list                        (*selected statements*)