Merge branch 'trunk' into pr379

4 files changed, 61 insertions, 61 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 4fd29a94de..ddd2ed6afa 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -97,21 +97,30 @@ let segment_of_objects prefix =
 
 let initial_prefix = default_library,(Names.initial_path,Names.DirPath.empty)
 
-let lib_stk = ref ([] : library_segment)
+type lib_state = {
+  comp_name   : Names.DirPath.t option;
+  lib_stk     : library_segment;
+  path_prefix : Names.DirPath.t * (Names.module_path * Names.DirPath.t);
+}
 
-let comp_name = ref None
+let initial_lib_state = {
+  comp_name   = None;
+  lib_stk     = [];
+  path_prefix = initial_prefix;
+}
+
+let lib_state = ref initial_lib_state
 
 let library_dp () =
-  match !comp_name with Some m -> m | None -> default_library
+  match !lib_state.comp_name with Some m -> m | None -> default_library
 
 (* [path_prefix] is a pair of absolute dirpath and a pair of current
    module path and relative section path *)
-let path_prefix = ref initial_prefix
 
-let cwd () = fst !path_prefix
-let current_prefix () = snd !path_prefix
-let current_mp () = fst (snd !path_prefix)
-let current_sections () = snd (snd !path_prefix)
+let cwd () = fst !lib_state.path_prefix
+let current_prefix () = snd !lib_state.path_prefix
+let current_mp () = fst (snd !lib_state.path_prefix)
+let current_sections () = snd (snd !lib_state.path_prefix)
 
 let sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
 let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
@@ -132,7 +141,7 @@ let make_kn id =
   let mp,dir = current_prefix () in
   Names.make_kn mp dir (Names.Label.of_id id)
 
-let make_oname id = Libnames.make_oname !path_prefix id
+let make_oname id = Libnames.make_oname !lib_state.path_prefix id
 
 let recalc_path_prefix () =
   let rec recalc = function
@@ -142,18 +151,18 @@ let recalc_path_prefix () =
     | _::l -> recalc l
     | [] -> initial_prefix
   in
-  path_prefix := recalc !lib_stk
+  lib_state := { !lib_state with path_prefix = recalc !lib_state.lib_stk }
 
 let pop_path_prefix () =
-  let dir,(mp,sec) = !path_prefix in
-  path_prefix := pop_dirpath dir, (mp, pop_dirpath sec)
+  let dir,(mp,sec) = !lib_state.path_prefix in
+  lib_state := { !lib_state with path_prefix = pop_dirpath dir, (mp, pop_dirpath sec)}
 
 let find_entry_p p =
   let rec find = function
     | [] -> raise Not_found
     | ent::l -> if p ent then ent else find l
   in
-  find !lib_stk
+  find !lib_state.lib_stk
 
 let split_lib_gen test =
   let rec collect after equal = function
@@ -174,7 +183,7 @@ let split_lib_gen test =
 		| _ -> findeq (hd::after) before)
     | [] -> None
   in
-    match findeq [] !lib_stk with
+    match findeq [] !lib_state.lib_stk with
       | None -> error "no such entry"
       | Some r -> r
 
@@ -199,10 +208,10 @@ let split_lib_at_opening sp =
 (* Adding operations. *)
 
 let add_entry sp node =
-  lib_stk := (sp,node) :: !lib_stk
+  lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk }
 
 let pull_to_head oname =
-  lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk
+  lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk }
 
 let anonymous_id =
   let n = ref 0 in
@@ -277,7 +286,7 @@ let start_mod is_type export id mp fs =
   if exists then
     user_err ~hdr:"open_module" (pr_id id ++ str " already exists");
   add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
-  path_prefix := prefix;
+  lib_state := { !lib_state with path_prefix = prefix} ;
   prefix
 
 let start_module = start_mod false
@@ -299,16 +308,16 @@ let end_mod is_type =
     with Not_found -> error "No opened modules."
   in
   let (after,mark,before) = split_lib_at_opening oname in
-  lib_stk := before;
+  lib_state := { !lib_state with lib_stk = before };
   add_entry oname (ClosedModule (List.rev (mark::after)));
-  let prefix = !path_prefix in
+  let prefix = !lib_state.path_prefix in
   recalc_path_prefix ();
   (oname, prefix, fs, after)
 
 let end_module () = end_mod false
 let end_modtype () = end_mod true
 
-let contents () = !lib_stk
+let contents () = !lib_state.lib_stk
 
 let contents_after sp = let (after,_,_) = split_lib sp in after
 
@@ -316,14 +325,14 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
 
 (* TODO: use check_for_module ? *)
 let start_compilation s mp =
-  if !comp_name != None then
+  if !lib_state.comp_name != None then
     error "compilation unit is already started";
   if not (Names.DirPath.is_empty (current_sections ())) then
     error "some sections are already opened";
   let prefix = s, (mp, Names.DirPath.empty) in
   let () = add_anonymous_entry (CompilingLibrary prefix) in
-  comp_name := Some s;
-  path_prefix := prefix
+  lib_state := { !lib_state with comp_name = Some s;
+                                 path_prefix = prefix }
 
 let end_compilation_checks dir =
   let _ =
@@ -344,7 +353,7 @@ let end_compilation_checks dir =
     with Not_found -> anomaly (Pp.str "No module declared")
   in
   let _ =
-    match !comp_name with
+    match !lib_state.comp_name with
       | None -> anomaly (Pp.str "There should be a module name...")
       | Some m ->
 	  if not (Names.DirPath.equal m dir) then anomaly
@@ -355,8 +364,8 @@ let end_compilation_checks dir =
 
 let end_compilation oname =
   let (after,mark,before) = split_lib_at_opening oname in
-  comp_name := None;
-  !path_prefix,after
+  lib_state := { !lib_state with comp_name = None };
+  !lib_state.path_prefix,after
 
 (* Returns true if we are inside an opened module or module type *)
 
@@ -514,7 +523,7 @@ let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore ()
 let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore ()
 
 let open_section id =
-  let olddir,(mp,oldsec) = !path_prefix in
+  let olddir,(mp,oldsec) = !lib_state.path_prefix in
   let dir = add_dirpath_suffix olddir id in
   let prefix = dir, (mp, add_dirpath_suffix oldsec id) in
   if Nametab.exists_section dir then
@@ -523,7 +532,7 @@ let open_section id =
   add_entry (make_oname id) (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
-  path_prefix := prefix;
+  lib_state := { !lib_state with path_prefix = prefix };
   if !Flags.xml_export then Hook.get f_xml_open_section id;
   add_section ()
 
@@ -549,8 +558,8 @@ let close_section () =
       error "No opened section."
   in
   let (secdecls,mark,before) = split_lib_at_opening oname in
-  lib_stk := before;
-  let full_olddir = fst !path_prefix in
+  lib_state := { !lib_state with lib_stk = before };
+  let full_olddir = fst !lib_state.path_prefix in
   pop_path_prefix ();
   add_entry oname (ClosedSection (List.rev (mark::secdecls)));
   if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname));
@@ -561,7 +570,7 @@ let close_section () =
 
 (* State and initialization. *)
 
-type frozen = Names.DirPath.t option * library_segment
+type frozen = lib_state
 
 let freeze ~marshallable =
   match marshallable with
@@ -578,18 +587,15 @@ let freeze ~marshallable =
                Some(n,OpenedSection(op,Summary.empty_frozen))
         | n, ClosedSection _ -> Some (n,ClosedSection [])
         | _, FrozenState _ -> None)
-      !lib_stk in
-    !comp_name, lib_stk
+      !lib_state.lib_stk in
+    { !lib_state with lib_stk }
   | _ ->
-    !comp_name, !lib_stk
+    !lib_state
 
-let unfreeze (mn,stk) =
-  comp_name := mn;
-  lib_stk := stk;
-  recalc_path_prefix ()
+let unfreeze st = lib_state := st
 
 let init () =
-  unfreeze (None,[]);
+  unfreeze initial_lib_state;
   Summary.init_summaries ();
   add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *)
 
diff --git a/library/libobject.ml b/library/libobject.ml
index caa03c85be..8757ca08c6 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -91,16 +91,8 @@ let declare_object_full odecl =
 			     dyn_rebuild_function = rebuild };
   (infun,outfun)
 
-(* The "try .. with .. " allows for correct printing when calling
-   declare_object a loading time.
-*)
-
-let declare_object odecl =
-  try fst (declare_object_full odecl)
-  with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
-let declare_object_full odecl =
-  try declare_object_full odecl
-  with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
+let declare_object odecl = fst (declare_object_full odecl)
+let declare_object_full odecl = declare_object_full odecl
 
 (* this function describes how the cache, load, open, and export functions
    are triggered. *)
diff --git a/library/nameops.ml b/library/nameops.ml
index 6020db33d9..098f5112fd 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -61,7 +61,7 @@ let make_ident sa = function
         if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n)
         else sa ^ "_" ^ (string_of_int n) in
       Id.of_string s
-  | None -> Id.of_string (String.copy sa)
+  | None -> Id.of_string sa
 
 let root_of_id id =
   let suffixstart = cut_ident true id in
@@ -92,20 +92,20 @@ let increment_subscript id =
 	add (carrypos-1)
       end
       else begin
-	let newid = String.copy id in
-	String.fill newid (carrypos+1) (len-1-carrypos) '0';
-	newid.[carrypos] <- Char.chr (Char.code c + 1);
+	let newid = Bytes.of_string id in
+	Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+	Bytes.set newid carrypos (Char.chr (Char.code c + 1));
 	newid
       end
     else begin
-      let newid = id^"0" in
+      let newid = Bytes.of_string (id^"0") in
       if carrypos < len-1 then begin
-	String.fill newid (carrypos+1) (len-1-carrypos) '0';
-	newid.[carrypos+1] <- '1'
+	Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+	Bytes.set newid (carrypos+1) '1'
       end;
       newid
     end
-  in Id.of_string (add (len-1))
+  in Id.of_bytes (add (len-1))
 
 let has_subscript id =
   let id = Id.to_string id in
@@ -113,9 +113,9 @@ let has_subscript id =
 
 let forget_subscript id =
   let numstart = cut_ident false id in
-  let newid = String.make (numstart+1) '0' in
+  let newid = Bytes.make (numstart+1) '0' in
   String.blit (Id.to_string id) 0 newid 0 numstart;
-  (Id.of_string newid)
+  (Id.of_bytes newid)
 
 let add_suffix id s = Id.of_string (Id.to_string id ^ s)
 let add_prefix s id = Id.of_string (s ^ Id.to_string id)
diff --git a/library/summary.ml b/library/summary.ml
index 6efa07f388..2ec4760d64 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -107,8 +107,10 @@ let unfreeze_summaries fs =
     try fold id decl state
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
-      Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
-        (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e));
+      Feedback.msg_error
+        Pp.(seq [str "Error unfrezing summay %s\n%s\n%!";
+                 str (name_of_summary id);
+                 CErrors.iprint e]);
       iraise e
   in
   (** We rely on the order of the frozen list, and the order of folding *)