From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 22 Mar 2011 17:22:53 +0000 (+0000)
Subject: Bug fixed and code refactoring: now both matitac and matita include files
X-Git-Tag: make_still_working~2554
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d7b5af5d8c6297f191cb644034b5b4cb7dfe86c1;p=helm.git

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 f65c8432a..7bce06884 100644
--- 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 d412d3ad0..2b8d9fd8c 100644
--- 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 af3cdf12e..13668a8ae 100644
--- 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 =