diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 50 | ||||
| -rw-r--r-- | library/nametab.ml | 12 |
2 files changed, 37 insertions, 25 deletions
diff --git a/library/lib.ml b/library/lib.ml index 213a1d19..4a4e90c1 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 9488 2007-01-17 11:11:58Z herbelin $ *) +(* $Id: lib.ml 10269 2007-10-29 11:09:43Z notin $ *) open Pp open Util @@ -237,14 +237,18 @@ let end_module id = let oname,nametab = try match find_entry_p is_something_opened with | oname,OpenedModule (_,_,nametab) -> - let sp = fst oname in - let id' = basename sp in - if id<>id' then error "this is not the last opened module"; - oname,nametab - | _,OpenedModtype _ -> - error "there are some open module types" - | _,OpenedSection _ -> - error "there are some open sections" + let id' = basename (fst oname) in + if id<>id' then + errorlabstrm "end_module" (str "last opened module is " ++ pr_id id'); + oname,nametab + | oname,OpenedModtype _ -> + let id' = basename (fst oname) in + errorlabstrm "end_module" + (str "module type " ++ pr_id id' ++ str " is still opened") + | oname,OpenedSection _ -> + let id' = basename (fst oname) in + errorlabstrm "end_module" + (str "section " ++ pr_id id' ++ str " is still opened") | _ -> assert false with Not_found -> error "no opened modules" @@ -271,14 +275,19 @@ let start_modtype id mp nametab = let end_modtype id = let sp,nametab = try match find_entry_p is_something_opened with - | sp,OpenedModtype (_,nametab) -> - let id' = basename (fst sp) in - if id<>id' then error "this is not the last opened module"; - sp,nametab - | _,OpenedModule _ -> - error "there are some open modules" - | _,OpenedSection _ -> - error "there are some open sections" + | oname,OpenedModtype (_,nametab) -> + let id' = basename (fst oname) in + if id<>id' then + errorlabstrm "end_modtype" (str "last opened module type is " ++ pr_id id'); + oname,nametab + | oname,OpenedModule _ -> + let id' = basename (fst oname) in + errorlabstrm "end_modtype" + (str "module " ++ pr_id id' ++ str " is still opened") + | oname,OpenedSection _ -> + let id' = basename (fst oname) in + errorlabstrm "end_modtype" + (str "section " ++ pr_id id' ++ str " is still opened") | _ -> assert false with Not_found -> error "no opened module types" @@ -487,9 +496,10 @@ let close_section id = let oname,fs = try match find_entry_p is_something_opened with | oname,OpenedSection (_,fs) -> - if id <> basename (fst oname) then - error "this is not the last opened section"; - (oname,fs) + let id' = basename (fst oname) in + if id <> id' then + errorlabstrm "close_section" (str "last opened section is " ++ pr_id id'); + (oname,fs) | _ -> assert false with Not_found -> error "no opened section" diff --git a/library/nametab.ml b/library/nametab.ml index 96280e8b..4e4e9b91 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nametab.ml 8642 2006-03-17 10:09:02Z notin $ *) +(* $Id: nametab.ml 10270 2007-10-29 14:48:33Z notin $ *) open Util open Pp @@ -107,8 +107,9 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - warning ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!"); + Options.if_verbose + warning ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!"); current | Nothing | Relative _ -> Relative (uname,o) @@ -146,8 +147,9 @@ let rec push_exactly uname o level (current,dirmap) = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - warning ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!"); + Options.if_verbose + warning ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!"); current | Nothing | Relative _ -> Relative (uname,o) |