X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite2%2FgrafiteTypes.ml;h=c73e8bd3ce395af92af7a52e00b53900ad503adb;hb=a32b0ea407ce62999f8cfa335cb6f4a8f905a38a;hp=2e2daf4e773de903e1561ce19fc2c64810a76e58;hpb=a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5;p=helm.git

diff --git a/helm/ocaml/grafite2/grafiteTypes.ml b/helm/ocaml/grafite2/grafiteTypes.ml
index 2e2daf4e7..c73e8bd3c 100644
--- a/helm/ocaml/grafite2/grafiteTypes.ml
+++ b/helm/ocaml/grafite2/grafiteTypes.ml
@@ -53,6 +53,7 @@ type status = {
   aliases: DisambiguateTypes.environment;
   multi_aliases: DisambiguateTypes.multiple_environment;
   moo_content_rev: GrafiteMarshal.moo;
+  metadata: LibraryNoDb.metadata list;
   proof_status: proof_status;
   options: options;
   objects: UriManager.uri list;
@@ -115,7 +116,7 @@ let get_proof_conclusion status goal =
   | _ -> raise (Statement_error "no ongoing proof")
  
 let add_moo_content cmds status =
-  let content, metadata = status.moo_content_rev in
+  let content = status.moo_content_rev in
   let content' =
     List.fold_right
       (fun cmd acc ->
@@ -132,7 +133,7 @@ let add_moo_content cmds status =
   in
 (*   prerr_endline ("new moo content: " ^ String.concat " " (List.map
     GrafiteAstPp.pp_command content')); *)
-  { status with moo_content_rev = content', metadata }
+  { status with moo_content_rev = content' }
 
 let get_option status name =
   try
@@ -174,26 +175,29 @@ let get_string_option status name =
 
 let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
 
-let add_moo_metadata new_metadata status =
-  let content, metadata = status.moo_content_rev in
-  let metadata' =
-    List.fold_left
-      (fun acc m ->
-        match m with
-        | GrafiteAst.Dependency buri ->
-            let is_self = (* self dependency *)
-              try
-                get_string_option status "baseuri" = buri
-              with Option_error _ -> false  (* baseuri not yet set *)
-            in
-            if is_self
-              || List.exists (GrafiteAst.eq_metadata m) metadata (* duplicate *)
-            then acc
-            else m :: acc
-        | _ -> m :: acc)
-      metadata new_metadata
-  in
-  { status with moo_content_rev = content, metadata' }
+let add_metadata new_metadata status =
+  if Helm_registry.get_bool "db.nodb" then
+    let metadata = status.metadata in
+    let metadata' =
+      List.fold_left
+        (fun acc m ->
+          match m with
+          | LibraryNoDb.Dependency buri ->
+              let is_self = (* self dependency *)
+                try
+                  get_string_option status "baseuri" = buri
+                with Option_error _ -> false  (* baseuri not yet set *)
+              in
+              if is_self (* duplicate *)
+                || List.exists (LibraryNoDb.eq_metadata m) metadata
+              then acc
+              else m :: acc
+          | _ -> m :: acc)
+        metadata new_metadata
+    in
+    { status with metadata = metadata' }
+  else
+    status
 
 let dump_status status = 
   HLog.message "status.aliases:\n";