Bug fixed and code refactoring: now both matitac and matita include files

correctly by re-generating ~include_paths in the same way and every time a
file is opened (either by matitaScript or by assert_ng itself).

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index f65c8432a4000f3dc9f28031eb0d5a03bc2c4174..7bce06884ae091378d6d228811e2c1b474fae28c 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -159,6 +159,24 @@ let baseuri_of_script ~include_paths fname =
     raise (Failure ("File not found: "^fname))
 ;;
 
+(* given a path to a ma file inside the include_paths, returns the
+   new include_paths associated to that file *)
+let read_include_paths ~include_paths file =
+ try 
+   let root, _buri, _fname, _tgt = 
+     Librarian.baseuri_of_script ~include_paths:[] file in 
+   let includes =
+    try
+     Str.split (Str.regexp " ") 
+      (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+    with Not_found -> []
+   in
+   let rc = root :: includes in
+    List.iter (HLog.debug) rc; rc
+ with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+  []
+;;
+
 let rec get_ast status ~compiling ~asserted ~include_paths strm = 
   match GrafiteParser.parse_statement status strm with
      (GrafiteAst.Executable
@@ -294,10 +312,20 @@ and compile ~compiling ~asserted ~include_paths fname =
       clean_exit baseuri exn
 
 and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
- let _,baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
+ let root,baseuri,fullmapath,_ =
+  Librarian.baseuri_of_script ~include_paths mapath in
  if List.mem fullmapath asserted then asserted,false
  else
   begin
+   let include_paths =
+    let includes =
+     try
+      Str.split (Str.regexp " ") 
+       (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+     with Not_found -> []
+    in
+     root::includes @
+      Helm_registry.get_list Helm_registry.string "matita.includes" in
    let baseuri = NUri.uri_of_string baseuri in
    let ngtime_of baseuri =
     let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
@@ -322,6 +350,8 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
             in
              asserted, b || b1
               || let _,baseuri,_,_ =
+                   (*CSC: bug here? include_paths should be empty and
+                          mapath should be absolute *)
                    Librarian.baseuri_of_script ~include_paths mapath in
                  let baseuri = NUri.uri_of_string baseuri in
                   (match ngtime_of baseuri with

diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli
index d412d3ad03b1555a49cfe0c565bb80789eea25f5..2b8d9fd8c7708722fb45ec6d33f722b72623bd20 100644 (file)
--- a/matita/matita/matitaEngine.mli
+++ b/matita/matita/matitaEngine.mli
@@ -52,3 +52,7 @@ val eval_ast :
    (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) option) list
 
 val assert_ng: include_paths:string list -> string -> bool
+
+(* given a path to a ma file inside the include_paths, returns the
+   new include_paths associated to that file *)
+val read_include_paths: include_paths:string list -> string -> string list

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index af3cdf12eb15c7a1381e3e3af84f295838974b20..13668a8aecc318d7df036bf406467826e8bb639a 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -264,21 +264,6 @@ let initial_statuses current baseuri =
    | None -> ());
   status
 in
-let read_include_paths file =
- try 
-   let root, _buri, _fname, _tgt = 
-     Librarian.baseuri_of_script ~include_paths:[] file in 
-   let includes =
-    try
-     Str.split (Str.regexp " ") 
-      (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
-    with Not_found -> []
-   in
-   let rc = root :: includes in
-    List.iter (HLog.debug) rc; rc
- with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
-  []
-in
 let default_buri = "cic:/matita/tests" in
 let default_fname = ".unnamed.ma" in
 object (self)
@@ -822,7 +807,7 @@ object (self)
        let f = Librarian.absolutize file in
         tab_label#set_text (Filename.basename f);
         filename_ <- Some f;
-        include_paths_ <- read_include_paths f;
+        include_paths_ <- MatitaEngine.read_include_paths ~include_paths:[] f;
         self#reset_buffer
 
   method set_star b =