summaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/lib.ml50
-rw-r--r--library/nametab.ml12
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)