Bug fixed: the include_paths were no longer handled properly when matita was

launched outside a development. E.g.: ./matita library/nat/times.ma was no
longer working (./matita -I library library/nat/times.ma was)

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index a0d0944ca0c8d770375b8395db59c6a211225b54..d628af98dff7b237331bb4ca094087a9e41438ec 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -79,18 +79,6 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
  parsed_text st
 =
   let module TAPp = GrafiteAstPp in
-  let include_ = 
-    match guistuff.filenamedata with
-    | None,None -> []
-    | None,Some devel -> [MatitamakeLib.root_for_development devel ]
-    | Some f,_ -> 
-        match MatitamakeLib.development_for_dir (Filename.dirname f) with
-        | None -> []
-        | Some devel -> [MatitamakeLib.root_for_development devel ]
-  in
-  let include_ =
-    include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
-  in
   let parsed_text_length = String.length parsed_text in
   let loc, ex = 
     match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
@@ -215,7 +203,7 @@ let pp_eager_statement_ast =
   GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
     ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
  
-let rec eval_macro (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
+let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
   let module TAPp = GrafiteAstPp in
   let module MQ = MetadataQuery in
   let module MDB = LibraryDb in
@@ -290,8 +278,8 @@ let rec eval_macro (buffer : GText.buffer) guistuff lexicon_status grafite_statu
           let loc = HExtlib.floc_of_loc (0,text_len) in
           let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
           let res,_parsed_text_len =
-           eval_statement buffer guistuff lexicon_status grafite_status
-            user_goal script statement
+           eval_statement include_paths buffer guistuff lexicon_status
+            grafite_status user_goal script statement
           in
            (* we need to replace all the parsed_text *)
            res,String.length parsed_text
@@ -318,7 +306,7 @@ let rec eval_macro (buffer : GText.buffer) guistuff lexicon_status grafite_statu
   | TA.Search_pat (_, search_kind, str) -> failwith "not implemented"
   | TA.Search_term (_, search_kind, term) -> failwith "not implemented"
                                 
-and eval_executable (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script loc ex
+and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script loc ex
 =
  let module TAPp = GrafiteAstPp in
  let module MD = GrafiteDisambiguator in
@@ -354,10 +342,10 @@ and eval_executable (buffer : GText.buffer) guistuff lexicon_status grafite_stat
           None -> []
         | Some n -> GrafiteTypes.get_proof_context grafite_status n in
       let grafite_status,macro = lazy_macro context in
-       eval_macro buffer guistuff lexicon_status grafite_status user_goal
-        unparsed_text parsed_text script macro
+       eval_macro include_paths buffer guistuff lexicon_status grafite_status
+        user_goal unparsed_text parsed_text script macro
 
-and eval_statement (buffer : GText.buffer) guistuff lexicon_status
+and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
  grafite_status user_goal script statement
 =
   let (lexicon_status,st), unparsed_text =
@@ -365,9 +353,7 @@ and eval_statement (buffer : GText.buffer) guistuff lexicon_status
     | `Raw text ->
         if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
         GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
-         ~include_paths:(Helm_registry.get_list
-           Helm_registry.string "matita.includes")
-         lexicon_status, text
+         ~include_paths lexicon_status, text
     | `Ast (st, text) -> (lexicon_status, st), text
   in
   let text_of_loc loc =
@@ -386,8 +372,8 @@ and eval_statement (buffer : GText.buffer) guistuff lexicon_status
       let s = String.sub unparsed_text parsed_text_length remain_len in
       let s,len = 
        try
-        eval_statement buffer guistuff lexicon_status grafite_status user_goal
-         script (`Raw s)
+        eval_statement include_paths buffer guistuff lexicon_status
+         grafite_status user_goal script (`Raw s)
        with
           HExtlib.Localized (floc, exn) ->
            HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn
@@ -402,8 +388,8 @@ and eval_statement (buffer : GText.buffer) guistuff lexicon_status
       | [] -> [], 0)
   | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
      let parsed_text, parsed_text_length = text_of_loc loc in
-      eval_executable buffer guistuff lexicon_status grafite_status user_goal
-       unparsed_text parsed_text script loc ex
+      eval_executable include_paths buffer guistuff lexicon_status
+       grafite_status user_goal unparsed_text parsed_text script loc ex
   
 let fresh_script_id =
   let i = ref 0 in
@@ -419,6 +405,7 @@ class script  ~(source_view: GSourceView.source_view)
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
 let initial_statuses =
+ (* these include_paths are used only to load the initial notation *)
  let include_paths =
   Helm_registry.get_list Helm_registry.string "matita.includes" in
  let lexicon_status =
@@ -428,6 +415,9 @@ let initial_statuses =
   grafite_status,lexicon_status
 in
 object (self)
+  val mutable include_paths =
+   Helm_registry.get_list Helm_registry.string "matita.includes"
+
   val scriptId = fresh_script_id ()
   
   val guistuff = {
@@ -484,8 +474,8 @@ object (self)
    HLog.debug ("evaluating: " ^ first_line s ^ " ...");
    let (entries, parsed_len) = 
     try
-     eval_statement buffer guistuff self#lexicon_status self#grafite_status
-      userGoal self (`Raw s)
+     eval_statement include_paths buffer guistuff self#lexicon_status
+      self#grafite_status userGoal self (`Raw s)
     with End_of_file -> raise Margin
    in
    let new_statuses, new_statements =
@@ -598,8 +588,17 @@ object (self)
     
   method assignFileName file =
     let abspath = MatitaMisc.absolute_path file in
-    let devel = MatitamakeLib.development_for_dir (Filename.dirname abspath) in
-    guistuff.filenamedata <- Some abspath, devel
+    let dirname = Filename.dirname abspath in
+    let devel = MatitamakeLib.development_for_dir dirname in
+    guistuff.filenamedata <- Some abspath, devel;
+    let include_ = 
+     match MatitamakeLib.development_for_dir dirname with
+        None -> []
+      | Some devel -> [MatitamakeLib.root_for_development devel] in
+    let include_ =
+     include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+    in
+     include_paths <- include_
     
   method saveToFile () =
     let oc = open_out self#getFilename in
@@ -650,10 +649,19 @@ object (self)
   method template () =
     let template = HExtlib.input_file BuildTimeConf.script_template in 
     buffer#insert ~iter:(buffer#get_iter `START) template;
-    guistuff.filenamedata <- 
-      (None,MatitamakeLib.development_for_dir (Unix.getcwd ()));
-    buffer#set_modified false;
-    set_star (Filename.basename self#ppFilename) false
+    let development = MatitamakeLib.development_for_dir (Unix.getcwd ()) in
+    guistuff.filenamedata <- (None,development);
+    let include_ = 
+     match development with
+        None -> []
+      | Some devel -> [MatitamakeLib.root_for_development devel ]
+    in
+    let include_ =
+     include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+    in
+     include_paths <- include_ ;
+     buffer#set_modified false;
+     set_star (Filename.basename self#ppFilename) false
 
   method goto (pos: [`Top | `Bottom | `Cursor]) () =
     let old_locked_mark =
@@ -767,9 +775,7 @@ object (self)
       if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
       let lexicon_status,st =
        GrafiteParser.parse_statement (Ulexing.from_utf8_string s)
-        ~include_paths:(Helm_registry.get_list
-          Helm_registry.string "matita.includes")
-        lexicon_status
+        ~include_paths lexicon_status
       in
       match st with
         GrafiteParser.LNone loc