summaryrefslogtreecommitdiff
path: root/library/lib.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-01-03 16:26:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2008-01-03 16:26:12 +0000
commit2281410e38ef99d025ea77194585a9bc019fdaa9 (patch)
tree71ba76741c3ab6b752be876565dc34b0b0138dc5 /library/lib.ml
parent4767d724d489a7ad67f696e9401e70b9f9ae2143 (diff)
Imported Upstream version 8.1.pl3+dfsgupstream/8.1.pl3+dfsg
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml50
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"