consolidate const_syntax naming
authorhaftmann
Fri Jul 16 15:55:32 2010 +0200 (2010-07-16)
changeset 3787648116a1764c5
parent 37846 6f8b1bb4d248
child 37877 d4a30d210220
consolidate const_syntax naming
src/Tools/Code/code_printer.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_printer.ML	Fri Jul 16 15:28:23 2010 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Fri Jul 16 15:55:32 2010 +0200
     1.3 @@ -67,20 +67,20 @@
     1.4  
     1.5    type tyco_syntax
     1.6    type simple_const_syntax
     1.7 -  type proto_const_syntax
     1.8    type const_syntax
     1.9 +  type activated_const_syntax
    1.10    val parse_infix: ('a -> 'b) -> lrx * int -> string
    1.11      -> int * ((fixity -> 'b -> Pretty.T)
    1.12      -> fixity -> 'a list -> Pretty.T)
    1.13    val parse_syntax: ('a -> 'b) -> Token.T list
    1.14      -> (int * ((fixity -> 'b -> Pretty.T)
    1.15      -> fixity -> 'a list -> Pretty.T)) option * Token.T list
    1.16 -  val simple_const_syntax: simple_const_syntax -> proto_const_syntax
    1.17 +  val simple_const_syntax: simple_const_syntax -> const_syntax
    1.18    val activate_const_syntax: theory -> literals
    1.19 -    -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
    1.20 +    -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
    1.21    val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
    1.22      -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    1.23 -    -> (string -> const_syntax option)
    1.24 +    -> (string -> activated_const_syntax option)
    1.25      -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
    1.26    val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    1.27      -> thm option -> fixity
    1.28 @@ -243,10 +243,10 @@
    1.29  
    1.30  type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
    1.31    -> fixity -> (iterm * itype) list -> Pretty.T);
    1.32 -type proto_const_syntax = int * (string list * (literals -> string list
    1.33 +type const_syntax = int * (string list * (literals -> string list
    1.34    -> (var_ctxt -> fixity -> iterm -> Pretty.T)
    1.35      -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    1.36 -type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    1.37 +type activated_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    1.38    -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    1.39  
    1.40  fun simple_const_syntax syn =
     2.1 --- a/src/Tools/Code/code_target.ML	Fri Jul 16 15:28:23 2010 +0200
     2.2 +++ b/src/Tools/Code/code_target.ML	Fri Jul 16 15:55:32 2010 +0200
     2.3 @@ -41,11 +41,11 @@
     2.4  
     2.5    val allow_abort: string -> theory -> theory
     2.6    type tyco_syntax = Code_Printer.tyco_syntax
     2.7 -  type proto_const_syntax = Code_Printer.proto_const_syntax
     2.8 +  type const_syntax = Code_Printer.const_syntax
     2.9    val add_syntax_class: string -> class -> string option -> theory -> theory
    2.10    val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
    2.11    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
    2.12 -  val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
    2.13 +  val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
    2.14    val add_reserved: string -> string -> theory -> theory
    2.15    val add_include: string -> string * (string * string list) option -> theory -> theory
    2.16  end;
    2.17 @@ -57,7 +57,7 @@
    2.18  
    2.19  type literals = Code_Printer.literals;
    2.20  type tyco_syntax = Code_Printer.tyco_syntax;
    2.21 -type proto_const_syntax = Code_Printer.proto_const_syntax;
    2.22 +type const_syntax = Code_Printer.const_syntax;
    2.23  
    2.24  
    2.25  (** basics **)
    2.26 @@ -83,7 +83,7 @@
    2.27    class: string Symtab.table,
    2.28    instance: unit Symreltab.table,
    2.29    tyco: Code_Printer.tyco_syntax Symtab.table,
    2.30 -  const: Code_Printer.proto_const_syntax Symtab.table
    2.31 +  const: Code_Printer.const_syntax Symtab.table
    2.32  };
    2.33  
    2.34  fun mk_name_syntax_table ((class, instance), (tyco, const)) =
    2.35 @@ -108,7 +108,7 @@
    2.36    -> (string -> string option)          (*module aliasses*)
    2.37    -> (string -> string option)          (*class syntax*)
    2.38    -> (string -> Code_Printer.tyco_syntax option)
    2.39 -  -> (string -> Code_Printer.const_syntax option)
    2.40 +  -> (string -> Code_Printer.activated_const_syntax option)
    2.41    -> ((Pretty.T -> string) * (Pretty.T -> unit))
    2.42    -> Code_Thingol.program
    2.43    -> string list                        (*selected statements*)