removed all Developments related stuff in glade file,

[helm.git] / matita / matitaScript.ml

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index fbe8730c43bfd4f90b156b3e7457488ba575ed8d..1a7c86bb858fa7800df793a888520583f598891b 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -114,9 +114,12 @@ let wrap_with_make include_paths g f x =
       (* we know that someone was able to include the .ma, get the baseuri
        * but was unable to get the compilation output 'xfilename' *)
       let root, buri, _, tgt = 
-        Librarian.baseuri_of_script ~include_paths mafilename
+        try
+          Librarian.baseuri_of_script ~include_paths mafilename
+        with Librarian.NoRootFor _ -> raise exn
       in
-      if MatitacLib.Make.make root [tgt] then f x else raise exn
+      if MatitacLib.Make.make root [tgt] then f x 
+      else raise (Failure ("Compiling: " ^ tgt))
 ;;
 
 let eval_with_engine include_paths 
@@ -688,7 +691,6 @@ class script  ~(source_view: GSourceView.source_view)
               ~set_star
               ~ask_confirmation
               ~urichooser 
-              ~rootcreator 
               () =
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
@@ -730,7 +732,8 @@ object (self)
   method has_name = filename_ <> None
   
   method include_paths =
-    include_paths_
+    include_paths_ @ 
+    Helm_registry.get_list Helm_registry.string "matita.includes"
 
   method private curdir =
     try
@@ -791,6 +794,7 @@ object (self)
 
   method private _advance ?statement () =
    let s = match statement with Some s -> s | None -> self#getFuture in
+   if self#bos then LibraryClean.clean_baseuris [self#buri_of_current_file];
    HLog.debug ("evaluating: " ^ first_line s ^ " ...");
    let entries, newtext, parsed_len = 
     try
@@ -935,7 +939,7 @@ object (self)
     HLog.debug ("Moving to " ^ Sys.getcwd ())
     
   method saveToFile () =
-    if self#has_name && buffer#modified then
+    if self#has_name then
       let oc = open_out self#filename in
       output_string oc (buffer#get_text ~start:buffer#start_iter
                         ~stop:buffer#end_iter ());
@@ -943,8 +947,7 @@ object (self)
       set_star false;
       buffer#set_modified false
     else
-      if self#has_name then HLog.debug "No need to save"
-      else HLog.error "Can't save, no filename selected"
+      HLog.error "Can't save, no filename selected"
   
   method private _saveToBackupFile () =
     if buffer#modified then
@@ -1143,10 +1146,10 @@ end
 
 let _script = ref None
 
-let script ~source_view ~mathviewer ~urichooser ~rootcreator ~ask_confirmation ~set_star ()
+let script ~source_view ~mathviewer ~urichooser ~ask_confirmation ~set_star ()
 =
   let s = new script 
-    ~source_view ~mathviewer ~ask_confirmation ~urichooser ~rootcreator ~set_star () 
+    ~source_view ~mathviewer ~ask_confirmation ~urichooser ~set_star () 
   in
   _script := Some s;
   s