From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 27 Jul 2005 13:11:45 +0000 (+0000)
Subject: fixed matitamake to handle development with names with spaces
X-Git-Tag: V_0_7_2~34
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d03016df7f68c81dd0f25bf18a792a80b412702;p=helm.git

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 fe9ea94d6..1d23ac063 100644
--- 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 a06c51170..6c8b86605 100644
--- 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 f8a9c9bb1..f7094ab95 100644
--- 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 55029914e..6e0d5660c 100644
--- 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 9af4cb0b6..073efb8f4 100644
--- 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