diff options
author | 2008-01-03 16:26:12 +0000 | |
---|---|---|
committer | 2008-01-03 16:26:12 +0000 | |
commit | be10fbd27424691aec2e27009e8a2702f509e665 (patch) | |
tree | 67e22adb269e653f5c0aac7ac85eb5e995701714 /library/lib.ml | |
parent | da0f849b5c4e1e8682a240d74461340cf8973294 (diff) | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Merge commit 'upstream/8.1.pl3+dfsg'
Diffstat (limited to 'library/lib.ml')
-rw-r--r-- | library/lib.ml | 50 |
1 files changed, 30 insertions, 20 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" |