diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-11 15:36:18 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-11 15:36:18 +0000 |
commit | 7cde682014e0dd179ae3bed029a07c8bf0c71157 (patch) | |
tree | 55a5928dc7cd035700275fcfcb41c8221027db37 /library/declaremods.ml | |
parent | b3ebb256717364d6d6ed631cd7830e46a8ab6863 (diff) |
Print Module (Type) M now tries to print more details
"Print Module M" prints now by default both a signature
(fields with their types) and a body (fields with their types
and transparent bodies).
"Print Module Type M" could be used both when M is a module
or a module Type, it will only display th signature of M.
The earlier minimalist behavior (printing only the field names)
could be reactivated by option "Set Short Module Printing".
For the moment, the content of internal sub-modules and sub-modtypes
are not displayed.
Note: this commit is an experiment, many sitations are still
unsupported. When such situations are encountered, Print Module
will fall back on the earlier minimalist behavior. This might
occur in particular in presence of "with" annotations, or in the
conjonction of a non-global module (i.e. functor or module type)
and internal sub-modules.
Side effects of this commit:
- a better compare function for global_reference, with no
allocations at each comparison
- Nametab.the_globrevtab is now searched according to user part only
of a kernel_name
- The printing of an inductive block is now in Printer, and rely less
on the Nametab. Instead, we use identifiers in mind_typename and
mind_consnames. Note that Print M.indu will not display anymore
the pseudo-code "Inductive M.indu ..." but rather "Inductive indu..."
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14117 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.ml')
-rw-r--r-- | library/declaremods.ml | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 68d928aef..2b29868bd 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -525,6 +525,24 @@ let process_module_bindings argids args = in List.iter2 process_arg argids args +(* Same with module_type_body *) + +let rec seb2mse = function + | SEBident mp -> MSEident mp + | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s') + | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp)) + | SEBwith (s,With_definition_body(l,cb)) -> + (match cb.const_body with + | Def c -> MSEwith(seb2mse s,With_Definition(l,Declarations.force c)) + | _ -> assert false) + | _ -> failwith "seb2mse: received a non-atomic seb" + +let process_module_seb_binding mbid seb = + process_module_bindings [id_of_mbid mbid] + [mbid, + (seb2mse seb, + { ann_inline = DefaultInline; ann_scope_subst = [] })] + let intern_args interp_modtype (idl,(arg,ann)) = let inl = inline_annot ann in let lib_dir = Lib.library_dp() in |