1. metadata are no longer stored in .moo files.

[helm.git] / helm / ocaml / grafite2 / grafiteEngine.ml

diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml
index fe67c2fc4fb589e112ed4145bccb0ec626765e6c..70fb767a87f419bedb3eeab075351b66f81de789 100644 (file)
--- a/helm/ocaml/grafite2/grafiteEngine.ml
+++ b/helm/ocaml/grafite2/grafiteEngine.ml
@@ -25,7 +25,8 @@
 
 exception Drop
 exception UnableToInclude of string
-exception IncludedFileNotCompiled of string
+exception IncludedFileNotCompiled of string (* file name *)
+exception MetadataNotFound of string        (* file name *)
 
 type options = { 
   do_heavy_checks: bool ; 
@@ -476,15 +477,23 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
   | GrafiteAst.Include (loc, path) ->
      let absolute_path = make_absolute opts.include_paths path in
      let moopath = GrafiteMisc.obj_file_of_script ~basedir absolute_path in
-     let status = ref status in
+     let metadatapath =
+       GrafiteMisc.metadata_file_of_script ~basedir absolute_path in
      if not (Sys.file_exists moopath) then
        raise (IncludedFileNotCompiled moopath);
+     let status =
+       if Helm_registry.get_bool "db.nodb" then
+         if not (Sys.file_exists metadatapath) then
+           raise (MetadataNotFound metadatapath)
+         else
+           GrafiteTypes.add_metadata
+             (LibraryNoDb.load_metadata ~fname:metadatapath) status
+       else
+         status
+     in
+     let status = ref status in
      eval_from_moo.efm_go status moopath;
      !status
-  | GrafiteAst.Metadata (loc, m) ->
-      (match m with
-      | GrafiteAst.Dependency uri -> GrafiteTypes.add_moo_metadata [m] status
-      | GrafiteAst.Baseuri _ -> status)
   | GrafiteAst.Set (loc, name, value) -> 
       let status = 
         if name = "baseuri" then begin
@@ -500,7 +509,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
             HLog.message ("cleaning baseuri " ^ value);
             LibraryClean.clean_baseuris ~basedir [value]
           end;
-          GrafiteTypes.add_moo_metadata [GrafiteAst.Baseuri value] status
+          GrafiteTypes.add_metadata [LibraryNoDb.Baseuri value] status
         end else
           status
       in
@@ -551,7 +560,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
       let status = GrafiteTypes.add_moo_content [stm] status in
       let uris =
         List.map
-          (fun uri -> GrafiteAst.Dependency (UriManager.buri_of_uri uri))
+          (fun uri -> LibraryNoDb.Dependency (UriManager.buri_of_uri uri))
           (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern)
       in
       let diff =
@@ -559,7 +568,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
          DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
       in
       let status = MatitaSync.set_proof_aliases status diff in
-      let status = GrafiteTypes.add_moo_metadata uris status in
+      let status = GrafiteTypes.add_metadata uris status in
       status
   | GrafiteAst.Notation _ as stm -> GrafiteTypes.add_moo_content [stm] status
   | GrafiteAst.Obj (loc,obj) ->
@@ -645,9 +654,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
   let ast_of_cmd cmd =
     GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
       GrafiteAst.Command (DisambiguateTypes.dummy_floc,
-        (GrafiteAst.reash_cmd_uris cmd)))
+        cmd))
   in
-  let moo, metadata = GrafiteMarshal.load_moo fname in
+  let moo = GrafiteMarshal.load_moo fname in
   List.iter 
     (fun ast -> 
       let ast = ast_of_cmd ast in
@@ -656,19 +665,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
          ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic)
          ~disambiguate_command:(fun status cmd -> status,cmd)
          !status ast)
-    moo;
-  List.iter
-    (fun m ->
-      let ast =
-        ast_of_cmd (GrafiteAst.Metadata (DisambiguateTypes.dummy_floc, m))
-      in
-      status :=
-        eval_ast.ea_go
-         ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic)
-         ~disambiguate_command:(fun status cmd -> status,cmd)
-         !status ast)
-    metadata
-
+    moo
 } and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command
   ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st 
 ->