Restructuration et simplification des fonctions d'affichage, de détypage

et d'"externalisation"; standardisation du nom des fonctions d'affichage


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 60 insertions, 35 deletions

diff --git a/parsing/printer.mli b/parsing/printer.mli
index 4890b1bea..f3cdfda47 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -21,51 +21,76 @@ open Nametab
 open Termops
 open Evd
 open Proof_type
+open Rawterm
 (*i*)
 
 (* These are the entry points for printing terms, context, tac, ... *)
 
-val prterm_env      : env -> constr -> std_ppcmds
-val prterm_env_at_top : env -> constr -> std_ppcmds
-val prterm          : constr -> std_ppcmds
-val prtype_env      : env -> types -> std_ppcmds
-val prtype          : types -> std_ppcmds
-val prjudge_env     :
-  env -> Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
-val prjudge         : Environ.unsafe_judgment -> std_ppcmds * std_ppcmds
-
-val pr_rawterm       : Rawterm.rawconstr -> std_ppcmds
-val pr_cases_pattern : Rawterm.cases_pattern -> std_ppcmds
-
-val pr_constant     : env -> constant -> std_ppcmds
-val pr_existential  : env -> existential -> std_ppcmds
-val pr_constructor  : env -> constructor -> std_ppcmds
-val pr_inductive    : env -> inductive -> std_ppcmds
-val pr_global       : global_reference -> std_ppcmds
+(* Terms *)
+
+val pr_lconstr_env         : env -> constr -> std_ppcmds
+val pr_lconstr_env_at_top  : env -> constr -> std_ppcmds
+val pr_lconstr             : constr -> std_ppcmds
+
+val pr_constr_env          : env -> constr -> std_ppcmds
+val pr_constr              : constr -> std_ppcmds
+
+val pr_ltype_env           : env -> types -> std_ppcmds
+val pr_ltype               : types -> std_ppcmds
+
+val pr_type_env            : env -> types -> std_ppcmds
+val pr_type                : types -> std_ppcmds
+
+val pr_ljudge_env          : env -> unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge              : unsafe_judgment -> std_ppcmds * std_ppcmds
+
+val pr_lrawconstr_env      : env -> rawconstr -> std_ppcmds
+val pr_lrawconstr          : rawconstr -> std_ppcmds
+
+val pr_rawconstr_env       : env -> rawconstr -> std_ppcmds
+val pr_rawconstr           : rawconstr -> std_ppcmds
+
+val pr_constr_pattern_env  : env -> constr_pattern -> std_ppcmds
+val pr_constr_pattern      : constr_pattern -> std_ppcmds
+
+val pr_cases_pattern       : cases_pattern -> std_ppcmds
+
+(* Printing global references using names as short as possible *)
+
+val pr_global_env          : Idset.t -> global_reference -> std_ppcmds
+val pr_global              : global_reference -> std_ppcmds
+
+val pr_constant            : env -> constant -> std_ppcmds
+val pr_existential         : env -> existential -> std_ppcmds
+val pr_constructor         : env -> constructor -> std_ppcmds
+val pr_inductive           : env -> inductive -> std_ppcmds
 val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds
-val pr_pattern      : constr_pattern -> std_ppcmds
-val pr_pattern_env  : env -> names_context -> constr_pattern -> std_ppcmds
 
-val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds
+(* Contexts *)
 
-val pr_var_decl     : env -> named_declaration -> std_ppcmds
-val pr_rel_decl     : env -> rel_declaration -> std_ppcmds
+val pr_ne_context_of       : std_ppcmds -> env -> std_ppcmds
 
-val pr_named_context : env -> named_context -> std_ppcmds
-val pr_named_context_of : env -> std_ppcmds
-val pr_rel_context  : env -> rel_context -> std_ppcmds
-val pr_rel_context_of  : env -> std_ppcmds
-val pr_context_of   : env -> std_ppcmds
+val pr_var_decl            : env -> named_declaration -> std_ppcmds
+val pr_rel_decl            : env -> rel_declaration -> std_ppcmds
 
-val emacs_str       : string -> string
+val pr_named_context       : env -> named_context -> std_ppcmds
+val pr_named_context_of    : env -> std_ppcmds
+val pr_rel_context         : env -> rel_context -> std_ppcmds
+val pr_rel_context_of      : env -> std_ppcmds
+val pr_context_of          : env -> std_ppcmds
 
 (* Proofs *)
-val pr_goal : goal -> std_ppcmds
-val pr_subgoals : evar_map -> goal list -> std_ppcmds
-val pr_subgoal   : int -> goal list -> std_ppcmds
 
-val pr_open_subgoals    : unit -> std_ppcmds
-val pr_nth_open_subgoal : int -> std_ppcmds
-val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds
+val pr_goal                : goal -> std_ppcmds
+val pr_subgoals            : evar_map -> goal list -> std_ppcmds
+val pr_subgoal             : int -> goal list -> std_ppcmds
 
-val pr_prim_rule : prim_rule -> std_ppcmds
+val pr_open_subgoals       : unit -> std_ppcmds
+val pr_nth_open_subgoal    : int -> std_ppcmds
+val pr_evars_int           : int -> (evar * evar_info) list -> std_ppcmds
+
+val pr_prim_rule           : prim_rule -> std_ppcmds
+
+(* Emacs/proof general support *)
+
+val emacs_str       : string -> string