From 3e86f296f53e98401b281ce96fc7ba545dbd05b4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 Jul 2005 13:20:45 +0000 Subject: [PATCH] matitac now automatically cleans a non empty baseuri --- helm/matita/.depend | 8 +++---- helm/matita/Makefile.in | 2 +- helm/matita/matitaEngine.ml | 41 ++++++++++++++++++++++++-------- helm/matita/matitaEngine.mli | 4 ++++ helm/matita/matitaScript.ml | 2 +- helm/matita/matitacLib.ml | 9 +++++-- helm/matita/matitamakeLib.ml | 9 ++++--- helm/matita/template_makefile.in | 2 +- 8 files changed, 53 insertions(+), 24 deletions(-) diff --git a/helm/matita/.depend b/helm/matita/.depend index d057b7b4f..95ab00934 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -60,10 +60,10 @@ matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ buildTimeConf.cmo matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ buildTimeConf.cmx -matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ - matitacleanLib.cmi -matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ - matitacleanLib.cmi +matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ + matitaExcPp.cmi matitaDb.cmi matitacleanLib.cmi +matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx \ + matitaExcPp.cmx matitaDb.cmx matitacleanLib.cmi matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi buildTimeConf.cmo matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx buildTimeConf.cmx matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 7a553445d..44df23874 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -49,8 +49,8 @@ CCMOS = \ matitaDb.cmo \ matitaSync.cmo \ matitaDisambiguator.cmo \ - matitaEngine.cmo \ matitacleanLib.cmo \ + matitaEngine.cmo \ matitacLib.cmo CLEANCMOS = $(CCMOS) MAKECMOS = $(CCMOS) matitamakeLib.cmo diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 9fc24acf1..3d738e1b9 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -32,7 +32,11 @@ exception UnableToInclude of string;; let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; -type options = { do_heavy_checks: bool ; include_paths: string list } +type options = { + do_heavy_checks: bool ; + include_paths: string list ; + clean_baseuri: bool +} type statement = (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement @@ -546,6 +550,15 @@ let eval_command opts status cmd = else value in + if not (MatitacleanLib.is_empty value) then + begin + MatitaLog.warn ("baseuri " ^ value ^ " is not empty"); + if opts.clean_baseuri then + begin + MatitaLog.message ("cleaning baseuri " ^ value); + MatitacleanLib.clean_baseuris [value] + end + end; set_option status name value | GrafiteAst.Drop loc -> raise Drop | GrafiteAst.Qed loc -> @@ -671,39 +684,47 @@ let eval_executable opts status ex = let eval_comment status c = status -let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st = - let opts = - {do_heavy_checks = do_heavy_checks ; include_paths = include_paths} +let eval_ast + ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st += + let opts = { + do_heavy_checks = do_heavy_checks ; + include_paths = include_paths; + clean_baseuri = clean_baseuri } in match st with | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex | GrafiteAst.Comment (_,c) -> eval_comment status c -let eval_from_stream ?do_heavy_checks ?include_paths status str cb = +let eval_from_stream + ?do_heavy_checks ?include_paths ?clean_baseuri status str cb += try while true do let ast = GrafiteParser.parse_statement str in cb !status ast; - status := eval_ast ?do_heavy_checks ?include_paths !status ast + status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast done with End_of_file -> () (* to avoid a long list of recursive functions *) let _ = eval_from_stream_ref := eval_from_stream -let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb = +let eval_from_stream_greedy + ?do_heavy_checks ?include_paths ?clean_baseuri status str cb += while true do print_string "matita> "; flush stdout; let ast = GrafiteParser.parse_statement str in cb !status ast; - status := eval_ast ?do_heavy_checks ?include_paths !status ast + status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast done ;; -let eval_string ?do_heavy_checks ?include_paths status str = +let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str = eval_from_stream - ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->()) + ?do_heavy_checks ?include_paths ?clean_baseuri status (Stream.of_string str) (fun _ _ ->()) let default_options () = (* diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 6b9f235cd..a06c51170 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -34,11 +34,13 @@ type statement = val eval_string: ?do_heavy_checks:bool -> ?include_paths:string list -> + ?clean_baseuri:bool -> MatitaTypes.status ref -> string -> unit val eval_from_stream: ?do_heavy_checks:bool -> ?include_paths:string list -> + ?clean_baseuri:bool -> MatitaTypes.status ref -> char Stream.t -> (MatitaTypes.status -> statement -> unit) -> unit @@ -46,6 +48,7 @@ val eval_from_stream: val eval_from_stream_greedy: ?do_heavy_checks:bool -> ?include_paths:string list -> + ?clean_baseuri:bool -> MatitaTypes.status ref-> char Stream.t -> (MatitaTypes.status -> statement -> unit) -> unit @@ -53,6 +56,7 @@ val eval_from_stream_greedy: val eval_ast: ?do_heavy_checks:bool -> ?include_paths:string list -> + ?clean_baseuri:bool -> MatitaTypes.status -> statement -> MatitaTypes.status diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index c2b9a7e93..821602dce 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -337,7 +337,7 @@ let eval_executable guistuff status user_goal parsed_text script ex = (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with | None -> () | Some u -> - if not (MatitacleanLib.is_empty u) then + if not (ML.is_empty u) then match guistuff.ask_confirmation ~title:"Baseuri redefinition" diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index c77bb76bd..ebf1e455b 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -31,6 +31,7 @@ open MatitaTypes let paths_to_search_in = ref [];; let quiet_compilation = ref false;; +let dont_delete_baseuri = ref false;; let add_l l = fun s -> l := s :: !l ;; let set_b b = fun () -> b := true;; @@ -38,7 +39,9 @@ let set_b b = fun () -> b := true;; let arg_spec = [ "-I", Arg.String (add_l paths_to_search_in), " Adds path to the list of searched paths for the include command"; - "-q", Arg.Unit (set_b quiet_compilation), "Turn off verbose compilation" + "-q", Arg.Unit (set_b quiet_compilation), "Turn off verbose compilation"; + "-preserve", Arg.Unit (set_b dont_delete_baseuri), + "Turns off automatic baseuri cleaning" ] let usage = sprintf "MatitaC v%s\nUsage: matitac [option ...] file\nOptions:" @@ -174,7 +177,9 @@ let main ~mode = | fname -> open_in fname) in run_script is - (MatitaEngine.eval_from_stream ~include_paths:!paths_to_search_in); + (MatitaEngine.eval_from_stream + ~include_paths:!paths_to_search_in + ~clean_baseuri:(not !dont_delete_baseuri)); let elapsed = Unix.time () -. time in let tm = Unix.gmtime elapsed in let sec = diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index 2b3a4b394..534f2dc73 100644 --- a/helm/matita/matitamakeLib.ml +++ b/helm/matita/matitamakeLib.ml @@ -225,6 +225,8 @@ let mk_maker refresh_cb = let rec aux = function | f::tl -> let len = Unix.read f buf 0 1024 in + if len = 0 then + raise CHILD_DEAD; vt100 (String.sub buf 0 len); aux tl | _ -> () @@ -236,12 +238,9 @@ let mk_maker refresh_cb = done; true with CHILD_DEAD -> + ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore)); let _, status = Unix.waitpid [] !pid in - match status with - | Unix.WEXITED 0 -> - ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore)); - true - | _ -> false) + match status with | Unix.WEXITED 0 -> true | _ -> false) let build_development_in_bg ?(target="all") refresh_cb development = diff --git a/helm/matita/template_makefile.in b/helm/matita/template_makefile.in index 83fc7a3c7..1413aedd9 100644 --- a/helm/matita/template_makefile.in +++ b/helm/matita/template_makefile.in @@ -13,7 +13,7 @@ clean: %.moo:%.ma [ ! -e $@ ] || ($(MATITACLEAN) $< 1>/dev/null 2>/dev/null ; rm -f $@) - ($(MATITAC) -q -I @ROOT@ $< | (grep -v "^make" || true)) || \ + ($(MATITAC) -preserve -q -I @ROOT@ $< | (grep -v "^make" || true)) || \ ($(MATITACLEAN) $< ; exit 1) @DEPFILE@ @DEPFILESHORT@: $(SRC) -- 2.39.2