From 2d03016df7f68c81dd0f25bf18a792a80b412702 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 27 Jul 2005 13:11:45 +0000 Subject: [PATCH] fixed matitamake to handle development with names with spaces the engine now has 2 different exception to report 2 diffrent problems: - UnableToInclude - IncluedFileNotCompiled --- helm/matita/matitaEngine.ml | 9 +++++---- helm/matita/matitaEngine.mli | 1 + helm/matita/matitaScript.ml | 3 ++- helm/matita/matitamakeLib.ml | 6 +++++- helm/matita/template_makefile.in | 2 +- 5 files changed, 14 insertions(+), 7 deletions(-) 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 -- 2.39.2