fixed matitamake to handle development with names with spaces

the engine now has 2 different exception to report 2 diffrent problems:
- UnableToInclude
- IncluedFileNotCompiled

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index fe9ea94d66b3ba1dafab5310c035217dcb5f164a..1d23ac063709e3fe57265c86f57a95ae56bcb1e4 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -27,7 +27,8 @@ open Printf
 open MatitaTypes
 
 exception Drop;;
-exception UnableToInclude of string;;
+exception UnableToInclude of string
+exception IncludedFileNotCompiled of string
 
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
@@ -513,8 +514,7 @@ let make_absolute paths path =
   in
   try
     aux paths
-  with Unix.Unix_error _ as exc ->
-    command_error ("File " ^ path ^ " not found")
+  with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
 ;;
        
 let eval_command opts status cmd =
@@ -532,7 +532,8 @@ let eval_command opts status cmd =
      let absolute_path = make_absolute opts.include_paths path in
      let moopath = MatitaMisc.obj_file_of_script absolute_path in
      let ic =
-      try open_in moopath with Sys_error _ -> raise (UnableToInclude moopath) in
+      try open_in moopath with Sys_error _ -> 
+        raise (IncludedFileNotCompiled moopath) in
      let stream = Stream.of_channel ic in
      let status = ref status in
       !eval_from_stream_ref status stream (fun _ _ -> ());

diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli
index a06c5117005489ee02c7fc0ff2404501081c8146..6c8b8660518eb70cf07d5ae20e6a0c3f839cb5cf 100644 (file)
--- a/helm/matita/matitaEngine.mli
+++ b/helm/matita/matitaEngine.mli
@@ -25,6 +25,7 @@
 
 exception Drop
 exception UnableToInclude of string
+exception IncludedFileNotCompiled of string
 
 type statement =
   (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index f8a9c9bb132a3b23c0596d4b1778a701f06836d0..f7094ab95d282763733ab987af03bd7ec28d94f5 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -147,7 +147,8 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   try
     eval_with_engine guistuff status user_goal parsed_text st
   with
-    MatitaEngine.UnableToInclude what as exc ->
+  | MatitaEngine.UnableToInclude what 
+  | MatitaEngine.IncludedFileNotCompiled what as exc ->
       let compile_needed_and_go_on d =
         let target = what in
         let refresh_cb () = 

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 55029914ec12e1089f11c7af245b5fe0277ff29c..6e0d5660cd62148b2cade6a99410495da25fad48 100644 (file)
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -134,6 +134,7 @@ let rebuild_makefile development =
   
 (* creates a new development if possible *)
 let initialize_development name dir =
+  let name = Pcre.replace ~pat:" " ~templ:"_" name in 
   let dev = {name = name ; root = dir} in
   match development_for_dir dir with
   | Some d ->
@@ -154,7 +155,10 @@ let make chdir args =
   let old = Unix.getcwd () in
   try
     Unix.chdir chdir;
-    let rc = Unix.system (String.concat " " ("make"::args)) in
+    let rc = 
+      Unix.system 
+        (String.concat " " ("make"::(List.map Filename.quote args)))
+    in
     Unix.chdir old;
     match rc with
     | Unix.WEXITED 0 -> true

diff --git a/helm/matita/template_makefile.in b/helm/matita/template_makefile.in
index 9af4cb0b60b8f725093433c0562923d0f5b41804..073efb8f45856bc87798d9a2785f3b203f23875b 100644 (file)
--- a/helm/matita/template_makefile.in
+++ b/helm/matita/template_makefile.in
@@ -15,7 +15,7 @@ clean:
        ($(MATITAC) -q -I @ROOT@ $< | (grep -v "^make" || true))
 
 @DEPFILE@ : $(SRC)
-       @DEP@ -I @ROOT@ $^ > @DEPFILE@
+       @DEP@ -I '@ROOT@' $^ > @DEPFILE@
 
 # this is the depend for full targets like:
 # dir/dir/name.moo: dir/dir/name.ma dir/dep.moo