completed support for "-nodb", now also matitaclean and its library work with that...

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 4e48df8072d13a027ea5dac975936fa884d91d1f..61d69cbb9ace3b7770692205870fd840749e29b2 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -660,13 +660,15 @@ let disambiguate_obj status obj =
   let status = MatitaSync.set_proof_aliases status diff in
   status, cic
   
-let disambiguate_command status = function
+let disambiguate_command status =
+  function
   | GrafiteAst.Alias _
   | GrafiteAst.Default _
   | GrafiteAst.Drop _
   | GrafiteAst.Dump _
   | GrafiteAst.Include _
   | GrafiteAst.Interpretation _
+  | GrafiteAst.Metadata _
   | GrafiteAst.Notation _
   | GrafiteAst.Qed _
   | GrafiteAst.Render _
@@ -714,26 +716,29 @@ let eval_command opts status cmd =
        raise (IncludedFileNotCompiled moopath);
      !eval_from_moo_ref status moopath (fun _ _ -> ());
      !status
+  | GrafiteAst.Metadata (loc, m) ->
+      (match m with
+      | GrafiteAst.Dependency uri -> MatitaTypes.add_moo_metadata [m] status
+      | GrafiteAst.Baseuri _ -> status)
   | GrafiteAst.Set (loc, name, value) -> 
-      let value = 
-        if name = "baseuri" then
-          let v = MatitaMisc.strip_trailing_slash value in
-          try
-            ignore (String.index v ' ');
-            command_error "baseuri can't contain spaces"
-          with Not_found -> v
-        else
-          value
+      let status = 
+        if name = "baseuri" then begin
+          let value = 
+            let v = MatitaMisc.strip_trailing_slash value in
+            try
+              ignore (String.index v ' ');
+              command_error "baseuri can't contain spaces"
+            with Not_found -> v
+          in
+          if not (MatitaMisc.is_empty value) && opts.clean_baseuri then begin
+            MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
+            MatitaLog.message ("cleaning baseuri " ^ value);
+            MatitacleanLib.clean_baseuris [value]
+          end;
+          add_moo_metadata [GrafiteAst.Baseuri value] status
+        end else
+          status
       in
-      if not (MatitaMisc.is_empty value) then
-        begin
-          MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
-          if opts.clean_baseuri then
-            begin 
-              MatitaLog.message ("cleaning baseuri " ^ value);
-              MatitacleanLib.clean_baseuris [value]
-            end
-        end;
       set_option status name value
   | GrafiteAst.Drop loc -> raise Drop
   | GrafiteAst.Qed loc ->
@@ -772,13 +777,20 @@ let eval_command opts status cmd =
       MatitaSync.set_proof_aliases status diff
   | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
   | GrafiteAst.Dump _ -> assert false   (* ZACK: to be removed *)
-  | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
-      let status' = add_moo_content [stm] status in
+  | GrafiteAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm ->
+      let status = add_moo_content [stm] status in
+      let uris =
+        List.map
+          (fun uri -> GrafiteAst.Dependency (UriManager.buri_of_uri uri))
+          (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern)
+      in
       let diff =
        [DisambiguateTypes.Symbol (symbol, 0),
          DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
       in
-      MatitaSync.set_proof_aliases status' diff
+      let status = MatitaSync.set_proof_aliases status diff in
+      let status = MatitaTypes.add_moo_metadata uris status in
+      status
   | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
@@ -871,7 +883,6 @@ let eval_executable opts status ex =
 
 let eval_comment status c = status
             
-
 let eval_ast 
   ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st 
 =
@@ -884,21 +895,30 @@ let eval_ast
   | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex
   | GrafiteAst.Comment (_,c) -> eval_comment status c
 
-let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname
-  cb
+let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname cb
 =
-  let moo = MatitaMoo.load_moo fname in
+  let ast_of_cmd cmd =
+    GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
+      GrafiteAst.Command (DisambiguateTypes.dummy_floc,
+        (GrafiteAst.reash_cmd_uris cmd)))
+  in
+  let moo, metadata = MatitaMoo.load_moo fname in
   List.iter 
     (fun ast -> 
+      let ast = ast_of_cmd ast in
+      cb !status ast;
+      status :=
+        eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast)
+    moo;
+  List.iter
+    (fun m ->
       let ast =
-        GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
-          GrafiteAst.Command (DisambiguateTypes.dummy_floc,
-            (GrafiteAst.reash_cmd_uris ast)))
+        ast_of_cmd (GrafiteAst.Metadata (DisambiguateTypes.dummy_floc, m))
       in
       cb !status ast;
       status :=
         eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast)
-    moo
+    metadata
 
 let eval_from_stream 
   ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
@@ -952,7 +972,7 @@ let initial_status =
   lazy {
     aliases = DisambiguateTypes.Environment.empty;
     multi_aliases = DisambiguateTypes.Environment.empty;
-    moo_content_rev = [];
+    moo_content_rev = [], [];
     proof_status = No_proof;
     options = default_options ();
     objects = [];