removed all Developments related stuff in glade file,

added matita.includes to the default paths matita uses,
nice error message when a file is not found

diff --git a/components/library/librarian.ml b/components/library/librarian.ml
index 72f8c50db9fcfca38e13070a79271e26206bc771..9a16e814d56527354b66d4e8d5d5bdc6477795a3 100644 (file)
--- a/components/library/librarian.ml
+++ b/components/library/librarian.ml
@@ -41,7 +41,7 @@ let load_root_file rootpath =
   List.map 
     (fun l -> 
       match Str.split (Str.regexp "=") l with
-      | [k;v] -> Pcre.replace ~pat:" " k, Pcre.replace ~pat:" " v
+      | [k;v] -> Pcre.replace ~pat:"^ *" k, Pcre.replace ~pat:" *$" v
       | _ -> raise (Failure ("Malformed root file: " ^ rootpath)))
     lines
 ;;
@@ -70,8 +70,8 @@ let find_root_for ~include_paths file =
      HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
    ensure_trailing_slash root, remove_trailing_slash uri, path
  with Failure "find_in" -> 
-   HLog.error ("Unable to find: "^file^"\nPaths explored:\n");
-   List.iter (fun x -> HLog.error (" - "^x^"\n")) include_paths;
+   HLog.error ("Unable to find: "^file^"\nPaths explored:");
+   List.iter (fun x -> HLog.error (" - "^x)) include_paths;
    raise (NoRootFor file)
 ;;
 
@@ -118,7 +118,9 @@ let load_deps_file f =
       begin
         let l = input_line ic in
         match Str.split (Str.regexp " ") l with
-        | [] -> HLog.error ("malformed deps file: " ^ f); exit 1
+        | [] -> 
+            HLog.error ("Malformed deps file: " ^ f); 
+            raise (Failure ("Malformed deps file: " ^ f)) 
         | he::tl -> deps := (he,tl) :: !deps
       end
     done; !deps
@@ -241,7 +243,8 @@ module Make = functor (F:Format) -> struct
         let todo =
           let local, remote =
             List.partition
-              (fun (file,d) -> d<>[] || F.root_of local_options file = Some root)
+              (fun (file,d) -> 
+                d<>[] || F.root_of local_options file = Some root)
               todo
           in
           remote @ local
@@ -256,7 +259,7 @@ module Make = functor (F:Format) -> struct
               | Some froot ->
                   make froot [file]
               | None -> 
-                  HLog.error ("No root for: "^F.string_of_source_object file);            
+                  HLog.error ("No root for: "^F.string_of_source_object file);
                   false
             in
             if rc then (file::c,f)
@@ -287,9 +290,11 @@ module Make = functor (F:Format) -> struct
 end
   
 let write_deps_file root deps =
-  let oc = open_out "depends" in
-  List.iter (fun (t,d) -> output_string oc (t^" "^String.concat " " d^"\n")) deps;
+  let oc = open_out (root ^ "/depends") in
+  List.iter 
+    (fun (t,d) -> output_string oc (t^" "^String.concat " " d^"\n")) 
+    deps;
   close_out oc;
-  HLog.message ("Generated " ^ Sys.getcwd () ^ "/depends")
+  HLog.message ("Generated: " ^ root ^ "/depends")
 ;;
  

diff --git a/components/library/librarian.mli b/components/library/librarian.mli
index 1c305c2654bf49ee0d338f0710760f909d58afd8..9d042a10618111bee04f9156fe344a86ccb1bb39 100644 (file)
--- a/components/library/librarian.mli
+++ b/components/library/librarian.mli
@@ -1,16 +1,15 @@
 exception NoRootFor of string
 
-val find_root: string -> string
+val absolutize: string -> string 
 
+val find_root: string -> string
 val load_root_file: string -> (string*string) list
 
-val absolutize: string -> string 
-
 (* baseuri_of_script ?(inc:REG[matita.includes]) fname 
  *   -> 
  * root, buri, fullpath, rootrelativepath
  * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a,
- * /home/pippo/devel/a.ma *)
+ * /home/pippo/devel/a.ma, a.ma *)
 val baseuri_of_script: 
   include_paths:string list -> string -> string * string * string * string
 

diff --git a/matita/matita.glade b/matita/matita.glade
index 462d0c64c9db3961498babc5c6d6fd1245f145b1..0eaaaa7800e8a8e2bcb5aba2bfcf4258b05813b9 100644 (file)
--- a/matita/matita.glade
+++ b/matita/matita.glade
@@ -2589,450 +2589,6 @@
       </widget>
     </child>
   </widget>
-  <widget class="GtkWindow" id="NewRootWin">
-    <property name="title" translatable="yes">Create root file</property>
-    <property name="resizable">True</property>
-    <property name="modal">True</property>
-    <property name="window_position">GTK_WIN_POS_CENTER_ALWAYS</property>
-    <property name="type_hint">GDK_WINDOW_TYPE_HINT_UTILITY</property>
-    <child>
-      <widget class="GtkVBox" id="vbox10">
-        <property name="visible">True</property>
-        <child>
-          <widget class="GtkTable" id="table2">
-            <property name="visible">True</property>
-            <property name="border_width">3</property>
-            <property name="n_rows">2</property>
-            <property name="n_columns">3</property>
-            <property name="column_spacing">5</property>
-            <property name="row_spacing">5</property>
-            <child>
-              <placeholder/>
-            </child>
-            <child>
-              <widget class="GtkButton" id="chooseRootButton">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="label" translatable="yes">...</property>
-                <property name="use_underline">True</property>
-                <property name="response_id">0</property>
-              </widget>
-              <packing>
-                <property name="left_attach">2</property>
-                <property name="right_attach">3</property>
-                <property name="top_attach">1</property>
-                <property name="bottom_attach">2</property>
-                <property name="x_options">GTK_FILL</property>
-                <property name="y_options"></property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkEntry" id="rootEntry">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="invisible_char">*</property>
-              </widget>
-              <packing>
-                <property name="left_attach">1</property>
-                <property name="right_attach">2</property>
-                <property name="top_attach">1</property>
-                <property name="bottom_attach">2</property>
-                <property name="y_options"></property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkEntry" id="buriEntry">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="invisible_char">*</property>
-              </widget>
-              <packing>
-                <property name="left_attach">1</property>
-                <property name="right_attach">2</property>
-                <property name="y_options"></property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkLabel" id="label21">
-                <property name="visible">True</property>
-                <property name="xalign">0</property>
-                <property name="label" translatable="yes">Root directory</property>
-              </widget>
-              <packing>
-                <property name="top_attach">1</property>
-                <property name="bottom_attach">2</property>
-                <property name="x_options">GTK_FILL</property>
-                <property name="y_options"></property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkLabel" id="label20">
-                <property name="visible">True</property>
-                <property name="xalign">0</property>
-                <property name="label" translatable="yes">Base URI</property>
-              </widget>
-              <packing>
-                <property name="x_options">GTK_FILL</property>
-                <property name="y_options"></property>
-              </packing>
-            </child>
-          </widget>
-          <packing>
-            <property name="expand">False</property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkHSeparator" id="hseparator1">
-            <property name="visible">True</property>
-          </widget>
-          <packing>
-            <property name="expand">False</property>
-            <property name="padding">2</property>
-            <property name="position">1</property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkHBox" id="hbox21">
-            <property name="visible">True</property>
-            <property name="border_width">3</property>
-            <property name="spacing">5</property>
-            <child>
-              <widget class="GtkVBox" id="vbox11">
-                <property name="visible">True</property>
-                <child>
-                  <placeholder/>
-                </child>
-                <child>
-                  <placeholder/>
-                </child>
-              </widget>
-            </child>
-            <child>
-              <widget class="GtkButton" id="addButton">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="label">gtk-add</property>
-                <property name="use_stock">True</property>
-                <property name="response_id">0</property>
-              </widget>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">1</property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkButton" id="cancelButton">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="label">gtk-cancel</property>
-                <property name="use_stock">True</property>
-                <property name="response_id">0</property>
-              </widget>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">2</property>
-              </packing>
-            </child>
-          </widget>
-          <packing>
-            <property name="expand">False</property>
-            <property name="position">2</property>
-          </packing>
-        </child>
-      </widget>
-    </child>
-  </widget>
-  <!--
-  <widget class="GtkWindow" id="DevelListWin">
-    <property name="title" translatable="yes">Developments</property>
-    <property name="window_position">GTK_WIN_POS_CENTER</property>
-    <child>
-      <widget class="GtkVBox" id="vbox12">
-        <property name="visible">True</property>
-        <child>
-          <widget class="GtkScrolledWindow" id="scrolledwindow10">
-            <property name="visible">True</property>
-            <property name="can_focus">True</property>
-            <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-            <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
-            <property name="shadow_type">GTK_SHADOW_IN</property>
-            <child>
-              <widget class="GtkTreeView" id="developmentsTreeview">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="headers_visible">False</property>
-              </widget>
-            </child>
-          </widget>
-        </child>
-        <child>
-          <widget class="GtkHSeparator" id="hseparator2">
-            <property name="visible">True</property>
-          </widget>
-          <packing>
-            <property name="expand">False</property>
-            <property name="padding">2</property>
-            <property name="position">1</property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkHBox" id="buttonsHbox">
-            <property name="visible">True</property>
-            <property name="border_width">3</property>
-            <property name="spacing">4</property>
-            <child>
-              <widget class="GtkVBox" id="vbox13">
-                <property name="visible">True</property>
-                <child>
-                  <placeholder/>
-                </child>
-                <child>
-                  <placeholder/>
-                </child>
-              </widget>
-            </child>
-            <child>
-              <widget class="GtkButton" id="newButton">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="label">gtk-new</property>
-                <property name="use_stock">True</property>
-                <property name="response_id">0</property>
-              </widget>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">1</property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkButton" id="deleteButton">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="label">gtk-delete</property>
-                <property name="use_stock">True</property>
-                <property name="response_id">0</property>
-              </widget>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">2</property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkButton" id="buildButton">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="response_id">0</property>
-                <child>
-                  <widget class="GtkAlignment" id="alignment14">
-                    <property name="visible">True</property>
-                    <property name="xscale">0</property>
-                    <property name="yscale">0</property>
-                    <child>
-                      <widget class="GtkHBox" id="hbox23">
-                        <property name="visible">True</property>
-                        <property name="spacing">2</property>
-                        <child>
-                          <widget class="GtkImage" id="image358">
-                            <property name="visible">True</property>
-                            <property name="stock">gtk-execute</property>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="fill">False</property>
-                          </packing>
-                        </child>
-                        <child>
-                          <widget class="GtkLabel" id="label22">
-                            <property name="visible">True</property>
-                            <property name="label" translatable="yes">_Build</property>
-                            <property name="use_underline">True</property>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="fill">False</property>
-                            <property name="position">1</property>
-                          </packing>
-                        </child>
-                      </widget>
-                    </child>
-                  </widget>
-                </child>
-              </widget>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">3</property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkButton" id="cleanButton">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="response_id">0</property>
-                <child>
-                  <widget class="GtkAlignment" id="alignment15">
-                    <property name="visible">True</property>
-                    <property name="xscale">0</property>
-                    <property name="yscale">0</property>
-                    <child>
-                      <widget class="GtkHBox" id="hbox24">
-                        <property name="visible">True</property>
-                        <property name="spacing">2</property>
-                        <child>
-                          <widget class="GtkImage" id="image359">
-                            <property name="visible">True</property>
-                            <property name="stock">gtk-clear</property>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="fill">False</property>
-                          </packing>
-                        </child>
-                        <child>
-                          <widget class="GtkLabel" id="label23">
-                            <property name="visible">True</property>
-                            <property name="label" translatable="yes">C_lean</property>
-                            <property name="use_underline">True</property>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="fill">False</property>
-                            <property name="position">1</property>
-                          </packing>
-                        </child>
-                      </widget>
-                    </child>
-                  </widget>
-                </child>
-              </widget>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">4</property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkButton" id="publishButton">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="response_id">0</property>
-                <child>
-                  <widget class="GtkAlignment" id="alignment16">
-                    <property name="visible">True</property>
-                    <property name="xscale">0</property>
-                    <property name="yscale">0</property>
-                    <child>
-                      <widget class="GtkHBox" id="hbox25">
-                        <property name="visible">True</property>
-                        <property name="spacing">2</property>
-                        <child>
-                          <widget class="GtkImage" id="image907">
-                            <property name="visible">True</property>
-                            <property name="stock">gtk-convert</property>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="fill">False</property>
-                          </packing>
-                        </child>
-                        <child>
-                          <widget class="GtkLabel" id="label24">
-                            <property name="visible">True</property>
-                            <property name="label" translatable="yes">Publish</property>
-                            <property name="use_underline">True</property>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="fill">False</property>
-                            <property name="position">1</property>
-                          </packing>
-                        </child>
-                      </widget>
-                    </child>
-                  </widget>
-                </child>
-              </widget>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">5</property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkButton" id="graphButton">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="response_id">0</property>
-                <child>
-                  <widget class="GtkAlignment" id="alignment17">
-                    <property name="visible">True</property>
-                    <property name="xscale">0</property>
-                    <property name="yscale">0</property>
-                    <child>
-                      <widget class="GtkHBox" id="hbox26">
-                        <property name="visible">True</property>
-                        <property name="spacing">2</property>
-                        <child>
-                          <widget class="GtkImage" id="image908">
-                            <property name="visible">True</property>
-                            <property name="stock">gtk-zoom-fit</property>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="fill">False</property>
-                          </packing>
-                        </child>
-                        <child>
-                          <widget class="GtkLabel" id="label27">
-                            <property name="visible">True</property>
-                            <property name="label" translatable="yes">Graph</property>
-                            <property name="use_underline">True</property>
-                          </widget>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="fill">False</property>
-                            <property name="position">1</property>
-                          </packing>
-                        </child>
-                      </widget>
-                    </child>
-                  </widget>
-                </child>
-              </widget>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">6</property>
-              </packing>
-            </child>
-            <child>
-              <widget class="GtkButton" id="closeButton">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="label">gtk-close</property>
-                <property name="use_stock">True</property>
-                <property name="response_id">0</property>
-              </widget>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">7</property>
-              </packing>
-            </child>
-          </widget>
-          <packing>
-            <property name="expand">False</property>
-            <property name="position">2</property>
-          </packing>
-        </child>
-      </widget>
-    </child>
-  </widget>
-  -->
   <widget class="GtkDialog" id="DisambiguationErrors">
     <property name="width_request">450</property>
     <property name="height_request">400</property>

diff --git a/matita/matita.ml b/matita/matita.ml
index 198fad3c57fc54ab90d23ec58eee46e728fdfbe6..c559358c575934b67883baad1e9bd4286881fd32 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -65,7 +65,6 @@ let script =
         (fun ~title ~message -> 
             MatitaGtkMisc.ask_confirmation ~title ~message 
             ~parent:gui#main#toplevel ())
-      ~rootcreator:gui#createRoot
       ()
   in
   gui#sourceView#source_buffer#begin_not_undoable_action ();

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index b2f509b25ca036f2b16ab5003b1a10e6c721f867..aae91697a489cdf210649c75803b1b332b0bbbc5 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -363,7 +363,6 @@ class gui () =
   let main = new mainWin () in
   let fileSel = new fileSelectionWin () in
   let findRepl = new findReplWin () in
-  let newRoot = new newRootWin () in
   let keyBindingBoxes = (* event boxes which should receive global key events *)
     [ main#mainWinEventBox ]
   in
@@ -387,7 +386,6 @@ class gui () =
     val mutable _ok_not_exists = false
     val mutable _only_directory = false
     val mutable font_size = default_font_size
-    val mutable next_root_must_contain = None
     val mutable next_ligatures = []
     val clipboard = GData.clipboard Gdk.Atom.clipboard
     val primary = GData.clipboard Gdk.Atom.primary
@@ -721,26 +719,6 @@ class gui () =
           f (); source_view#misc#grab_focus ()
          with
           exc -> source_view#misc#grab_focus (); raise exc in
-      (* add root win *)
-      connect_button newRoot#addButton 
-       (fun () -> 
-          let name = newRoot#buriEntry#text in
-          let root = newRoot#rootEntry#text in
-          if next_root_must_contain = Some "xxx" then ();
-          HLog.error ("implement me: "^root^" "^name);
-          newRoot#buriEntry#set_text "";
-          newRoot#rootEntry#set_text "";
-          newRoot#toplevel#misc#hide());
-      connect_button newRoot#chooseRootButton 
-       (fun () ->
-         let path = self#chooseDir () in
-         match path with
-         | Some path -> newRoot#rootEntry#set_text path
-         | None -> ());
-      connect_button newRoot#cancelButton 
-       (fun () -> newRoot#toplevel#misc#hide ());
-      ignore(newRoot#toplevel#event#connect#delete 
-        (fun _ -> newRoot#toplevel#misc#hide();true));
       
         (* file selection win *)
       ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
@@ -1188,7 +1166,6 @@ class gui () =
     method fileSel = fileSel
     method findRepl = findRepl
     method main = main
-    method newRoot = newRoot
 
     method newBrowserWin () =
       object (self)
@@ -1242,10 +1219,6 @@ class gui () =
       (* we should check that this is a directory *)
       chosen_file
   
-    method createRoot ~containing =
-      next_root_must_contain <- containing;
-      newRoot#toplevel#misc#show()
-
     method askText ?(title = "") ?(msg = "") () =
       let dialog = new textDialog () in
       dialog#textDialog#set_title title;

diff --git a/matita/matitaGuiTypes.mli b/matita/matitaGuiTypes.mli
index 5a166fbd43c5b5988c85151da05181987eca861e..c9ef8612315169df35390dba041f1118da76566f 100644 (file)
--- a/matita/matitaGuiTypes.mli
+++ b/matita/matitaGuiTypes.mli
@@ -49,7 +49,6 @@ object
   method fileSel :      MatitaGeneratedGui.fileSelectionWin
   method main :         MatitaGeneratedGui.mainWin
   method findRepl :     MatitaGeneratedGui.findReplWin
-  method newRoot:      MatitaGeneratedGui.newRootWin
 (*   method toolbar :      MatitaGeneratedGui.toolBarWin *)
 
   method console:       console
@@ -86,7 +85,6 @@ object
     * @param ok_not_exists if set to true returns also non existent files
     * (useful for save). Defaults to false *)
   method chooseFile: ?ok_not_exists:bool -> unit -> string option
-  method createRoot: containing:string option -> unit
 
     (** prompt the user for a (multiline) text entry *)
   method askText: ?title:string -> ?msg:string -> unit -> string option

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index b0b020f0115bd8e7ffe3ff39dc798948a326fdf0..1a7c86bb858fa7800df793a888520583f598891b 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -691,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
@@ -733,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
@@ -1146,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

diff --git a/matita/matitaScript.mli b/matita/matitaScript.mli
index d4c82321e8e63b5382fb13ee129231ef7770011d..6b683799918e5a9c150f9342c1b954086874dc4d 100644 (file)
--- a/matita/matitaScript.mli
+++ b/matita/matitaScript.mli
@@ -93,7 +93,6 @@ val script:
   source_view:GSourceView.source_view -> 
   mathviewer: MatitaTypes.mathViewer-> 
   urichooser: (UriManager.uri list -> UriManager.uri list) -> 
-  rootcreator: (containing:string option -> unit) ->
   ask_confirmation: 
     (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> 
   set_star: (bool -> unit) ->