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;
| _ -> 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 ->
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
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";