From 3c7cfd710f472bd56ba430cac8d2fa794eaecfe3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 5 Jan 2008 15:43:47 +0000 Subject: [PATCH] get rid of gragrep, matitamake(Lib) and development windows, added a tutor to create a root file --- components/library/librarian.ml | 25 +- components/library/librarian.mli | 4 +- matita/.depend | 68 +++--- matita/Makefile | 35 +-- matita/gragrep.ml | 67 ------ matita/gragrep.mli | 27 --- matita/matita.glade | 14 +- matita/matita.ml | 26 +- matita/matitaGui.ml | 148 ++---------- matita/matitaGuiTypes.mli | 5 +- matita/matitaInit.ml | 20 +- matita/matitaMathView.ml | 15 -- matita/matitaScript.ml | 82 ++----- matita/matitaScript.mli | 2 +- matita/matitaTypes.ml | 2 - matita/matitaTypes.mli | 1 - matita/matitac.ml | 5 +- matita/matitadep.ml | 1 - matita/matitamake.ml | 135 ----------- matita/matitamake.mli | 27 --- matita/matitamakeLib.ml | 394 ------------------------------- matita/matitamakeLib.mli | 62 ----- 22 files changed, 105 insertions(+), 1060 deletions(-) delete mode 100644 matita/gragrep.ml delete mode 100644 matita/gragrep.mli delete mode 100644 matita/matitamake.ml delete mode 100644 matita/matitamake.mli delete mode 100644 matita/matitamakeLib.ml delete mode 100644 matita/matitamakeLib.mli diff --git a/components/library/librarian.ml b/components/library/librarian.ml index e8d0e7da1..417035a81 100644 --- a/components/library/librarian.ml +++ b/components/library/librarian.ml @@ -22,6 +22,18 @@ let remove_trailing_slash s = if s.[len-1] = '/' then String.sub s 0 (len-1) else s ;; +let parse_root rootpath = + let data = HExtlib.input_file rootpath in + let lines = Str.split (Str.regexp "\n") data in + List.map + (fun l -> + match Str.split (Str.regexp "=") l with + | [k;v] -> Pcre.replace ~pat:" " k, Pcre.replace ~pat:" " v + | _ -> raise (Failure ("Malformed root file: " ^ rootpath))) + lines +;; + + let find_root_for ~include_paths file = let include_paths = "" :: Sys.getcwd () :: include_paths in let path = HExtlib.find_in include_paths file in @@ -35,18 +47,7 @@ let find_root_for ~include_paths file = | _ -> raise (Helm_registry.Key_not_found "matita.baseuri") with Helm_registry.Key_not_found "matita.baseuri" -> let rootpath = find_root path in - let data = HExtlib.input_file rootpath in - let buri = - let lines = Str.split (Str.regexp "\n") data in - let lines = - List.map (fun l -> - match Str.split (Str.regexp "=") l with - | [k;v] -> Pcre.replace ~pat:" " k, Pcre.replace ~pat:" " v - | _ -> raise (Failure ("Malformed root file: " ^ rootpath))) - lines - in - List.assoc "baseuri" lines - in + let buri = List.assoc "baseuri" (parse_root rootpath) in rootpath, Filename.dirname rootpath, buri in (* HLog.debug ("file "^file^" rooted by "^rootpath^""); *) diff --git a/components/library/librarian.mli b/components/library/librarian.mli index a6b3c6849..5280dbbf8 100644 --- a/components/library/librarian.mli +++ b/components/library/librarian.mli @@ -1,6 +1,8 @@ exception NoRootFor of string -val find_root : string -> string +val find_root: string -> string + +val parse_root: string -> (string*string) list (* baseuri_of_script ?(inc:REG[matita.includes]) fname -> root, buri, fullpath * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a, diff --git a/matita/.depend b/matita/.depend index 9b802e20b..1530bae72 100644 --- a/matita/.depend +++ b/matita/.depend @@ -2,8 +2,6 @@ applyTransformation.cmo: applyTransformation.cmi applyTransformation.cmx: applyTransformation.cmi dump_moo.cmo: buildTimeConf.cmo dump_moo.cmx: buildTimeConf.cmx -gragrep.cmo: matitaInit.cmi buildTimeConf.cmo gragrep.cmi -gragrep.cmx: matitaInit.cmx buildTimeConf.cmx gragrep.cmi lablGraphviz.cmo: lablGraphviz.cmi lablGraphviz.cmx: lablGraphviz.cmi make.cmo: make.cmi @@ -14,18 +12,16 @@ matitaAutoGui.cmx: matitaGeneratedGui.cmx applyTransformation.cmx \ matitaAutoGui.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi -matitacLib.cmo: matitamakeLib.cmi matitaExcPp.cmi matitaEngine.cmi \ - buildTimeConf.cmo applyTransformation.cmi matitacLib.cmi -matitacLib.cmx: matitamakeLib.cmx matitaExcPp.cmx matitaEngine.cmx \ - buildTimeConf.cmx applyTransformation.cmx matitacLib.cmi -matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \ - matitacLib.cmi matitaWiki.cmo matitaMisc.cmi matitaInit.cmi \ - matitaEngine.cmi make.cmi gragrep.cmi -matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ - matitacLib.cmx matitaWiki.cmx matitaMisc.cmx matitaInit.cmx \ - matitaEngine.cmx make.cmx gragrep.cmx -matitadep.cmo: matitamakeLib.cmi matitaInit.cmi matitadep.cmi -matitadep.cmx: matitamakeLib.cmx matitaInit.cmx matitadep.cmi +matitacLib.cmo: matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmo \ + applyTransformation.cmi matitacLib.cmi +matitacLib.cmx: matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitacLib.cmi +matitac.cmo: matitaprover.cmi matitadep.cmi matitaclean.cmi matitacLib.cmi \ + matitaWiki.cmo matitaMisc.cmi matitaInit.cmi matitaEngine.cmi make.cmi +matitac.cmx: matitaprover.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx \ + matitaWiki.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx make.cmx +matitadep.cmo: matitaInit.cmi matitadep.cmi +matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi matitaEngine.cmx: matitaEngine.cmi matitaExcPp.cmo: matitaExcPp.cmi @@ -34,30 +30,22 @@ matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \ matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi -matitaGui.cmo: matitaprover.cmi matitamakeLib.cmi matitaTypes.cmi \ - matitaScript.cmi matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \ +matitaGui.cmo: matitaprover.cmi matitaTypes.cmi matitaScript.cmi \ + matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \ matitaGeneratedGui.cmo matitaExcPp.cmi matitaAutoGui.cmi \ buildTimeConf.cmo matitaGui.cmi -matitaGui.cmx: matitaprover.cmx matitamakeLib.cmx matitaTypes.cmx \ - matitaScript.cmx matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \ +matitaGui.cmx: matitaprover.cmx matitaTypes.cmx matitaScript.cmx \ + matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \ matitaGeneratedGui.cmx matitaExcPp.cmx matitaAutoGui.cmx \ buildTimeConf.cmx matitaGui.cmi -matitaInit.cmo: matitamakeLib.cmi matitaExcPp.cmi buildTimeConf.cmo \ - matitaInit.cmi -matitaInit.cmx: matitamakeLib.cmx matitaExcPp.cmx buildTimeConf.cmx \ - matitaInit.cmi -matitamakeLib.cmo: buildTimeConf.cmo matitamakeLib.cmi -matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi -matitamake.cmo: matitamakeLib.cmi matitaInit.cmi matitamake.cmi -matitamake.cmx: matitamakeLib.cmx matitaInit.cmx matitamake.cmi -matitaMathView.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi \ - matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \ - lablGraphviz.cmi buildTimeConf.cmo applyTransformation.cmi \ - matitaMathView.cmi -matitaMathView.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \ - matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \ - lablGraphviz.cmx buildTimeConf.cmx applyTransformation.cmx \ - matitaMathView.cmi +matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi +matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi +matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ + matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \ + buildTimeConf.cmo applyTransformation.cmi matitaMathView.cmi +matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ + matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \ + buildTimeConf.cmx applyTransformation.cmx matitaMathView.cmi matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ @@ -70,12 +58,12 @@ matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmo matitaprover.cmi matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ buildTimeConf.cmx matitaprover.cmi -matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo \ - applyTransformation.cmi matitaScript.cmi -matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \ - applyTransformation.cmx matitaScript.cmi +matitaScript.cmo: matitaTypes.cmi matitaMisc.cmi matitaGtkMisc.cmi \ + matitaEngine.cmi buildTimeConf.cmo applyTransformation.cmi \ + matitaScript.cmi +matitaScript.cmx: matitaTypes.cmx matitaMisc.cmx matitaGtkMisc.cmx \ + matitaEngine.cmx buildTimeConf.cmx applyTransformation.cmx \ + matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ diff --git a/matita/Makefile b/matita/Makefile index 2aef5b8fa..6d1135a23 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -18,8 +18,8 @@ OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLDEP_FLAGS) INSTALL_PROGRAMS= matita matitac -INSTALL_PROGRAMS_LINKS_MATITA= cicbrowser -INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean matitaprover matitawiki +INSTALL_PROGRAMS_LINKS_MATITA= +INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitaclean matitaprover matitawiki MATITA_FLAGS = -noprofile NODB=false @@ -32,7 +32,6 @@ MLI = \ lablGraphviz.mli \ matitaTypes.mli \ matitaMisc.mli \ - matitamakeLib.mli \ matitaExcPp.mli \ matitaInit.mli \ matitaEngine.mli \ @@ -49,7 +48,6 @@ CMLI = \ make.mli \ matitaTypes.mli \ matitaMisc.mli \ - matitamakeLib.mli \ matitaExcPp.mli \ matitaInit.mli \ matitaEngine.mli \ @@ -61,8 +59,6 @@ CMLI = \ MAINCMLI = \ matitadep.mli \ matitaclean.mli \ - matitamake.mli \ - gragrep.mli \ $(NULL) # objects for matita (GTK GUI) ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml) @@ -71,11 +67,11 @@ CML = buildTimeConf.ml $(CMLI:%.mli=%.ml) MAINCML = $(MAINCMLI:%.mli=%.ml) PROGRAMS_BYTE = \ - matita matitac cicbrowser matitadep matitaclean \ - matitamake matitaprover matitawiki + matita matitac matitadep matitaclean \ + matitaprover matitawiki PROGRAMS = $(PROGRAMS_BYTE) PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) -NOINST_PROGRAMS = dump_moo gragrep +NOINST_PROGRAMS = dump_moo NOINST_PROGRAMS_OPT = $(patsubst %,%.opt,$(EXTRA_PROGRAMS)) .PHONY: all @@ -169,21 +165,6 @@ matitaclean: matitac matitaclean.opt: matitac.opt $(H)test -f $@ || ln -s $< $@ -matitamake: matitac - $(H)test -f $@ || ln -s $< $@ -matitamake.opt: matitac.opt - $(H)test -f $@ || ln -s $< $@ - -gragrep: matitac - $(H)test -f $@ || ln -s $< $@ -gragrep.opt: matitac.opt - $(H)test -f $@ || ln -s $< $@ - -cicbrowser: matita - $(H)test -f $@ || ln -s $< $@ -cicbrowser.opt: matita.opt - $(H)test -f $@ || ln -s $< $@ - matitaGeneratedGui.ml: matita.glade $(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml @@ -378,12 +359,6 @@ matitaclean.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ matitawiki.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ -matitamake.opt.static: matitac.opt.static - $(H)test -f $@ || ln -s $< $@ -cicbrowser.opt.static: matita.opt.static - $(H)test -f $@ || ln -s $< $@ -cicbrowser.opt.static.upx: matita.opt.static.upx - $(H)test -f $@ || ln -s $< $@ %.upx: % cp $< $@ diff --git a/matita/gragrep.ml b/matita/gragrep.ml deleted file mode 100644 index d44c08d27..000000000 --- a/matita/gragrep.ml +++ /dev/null @@ -1,67 +0,0 @@ -(* Copyright (C) 2006, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -open Printf - -let is_notation = function GrafiteParser.LNone _ -> true | _ -> false - -let grep () = - let recursive = ref false in - let spec = [ - "-r", Arg.Set recursive, "enable directory recursion"; - ] in - MatitaInit.add_cmdline_spec spec; - MatitaInit.initialize_all (); - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in - let status = - CicNotation2.load_notation ~include_paths - BuildTimeConf.core_notation_script in - let path = - match Helm_registry.get_list Helm_registry.string "matita.args" with - | [ path ] -> path - | _ -> MatitaInit.die_usage () in - let grep_fun = - if !recursive then - (fun dirname -> - ignore (GrafiteWalker.rgrep_statement ~status - ~callback:(fun (fname, s) -> printf "%s: %s\n%!" fname s) - ~dirname is_notation)) - else - (fun fname -> - ignore (GrafiteWalker.grep_statement ~status - ~callback:(fun s -> printf "%s\n%!" s) - ~fname is_notation)) in - grep_fun path - -let handle_localized_exns f arg = - try - f arg - with HExtlib.Localized (loc, exn) -> - let loc_begin, loc_end = HExtlib.loc_of_floc loc in - eprintf "Error at %d-%d: %s\n%!" loc_begin loc_end (Printexc.to_string exn) - -let main () = handle_localized_exns grep () - diff --git a/matita/gragrep.mli b/matita/gragrep.mli deleted file mode 100644 index f762adb22..000000000 --- a/matita/gragrep.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* Copyright (C) 2006, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -val main: unit -> unit - diff --git a/matita/matita.glade b/matita/matita.glade index 72ba3db8c..462d0c64c 100644 --- a/matita/matita.glade +++ b/matita/matita.glade @@ -770,6 +770,7 @@ + True @@ -2587,9 +2589,9 @@ - - Create development - False + + Create root file + True True GTK_WIN_POS_CENTER_ALWAYS GDK_WINDOW_TYPE_HINT_UTILITY @@ -2639,7 +2641,7 @@ - + True True * @@ -2667,7 +2669,7 @@ True 0 - Name + Base URI GTK_FILL @@ -2742,6 +2744,7 @@ + 450 400 diff --git a/matita/matita.ml b/matita/matita.ml index b3c0373eb..198fad3c5 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -65,7 +65,7 @@ let script = (fun ~title ~message -> MatitaGtkMisc.ask_confirmation ~title ~message ~parent:gui#main#toplevel ()) - ~develcreator:gui#createDevelopment + ~rootcreator:gui#createRoot () in gui#sourceView#source_buffer#begin_not_undoable_action (); @@ -274,34 +274,16 @@ let _ = end (** Debugging }}} *) - (** {2 Command line parsing} *) - -let set_matita_mode () = - let matita_mode = - if Filename.basename Sys.argv.(0) = "cicbrowser" || - Filename.basename Sys.argv.(0) = "cicbrowser.opt" - then "cicbrowser" - else "matita" - in - Helm_registry.set "matita.mode" matita_mode - (** {2 Main} *) let _ = - set_matita_mode (); at_exit (fun () -> print_endline "\nThanks for using Matita!\n"); Sys.catch_break true; let args = Helm_registry.get_list Helm_registry.string "matita.args" in - if Helm_registry.get "matita.mode" = "cicbrowser" then (* cicbrowser *) - let browser = MatitaMathView.cicBrowser () in - let uri = match args with [] -> "cic:/" | _ -> String.concat " " args in - browser#loadInput uri - else begin (* matita *) - (try gui#loadScript (List.hd args) with Failure _ -> ()); - gui#main#mainWin#show (); - end; + (try gui#loadScript (List.hd args) with Failure _ -> ()); + gui#main#mainWin#show (); try - GtkThread.main () + GtkThread.main () with Sys.Break -> Sys.set_signal Sys.sigint (Sys.Signal_handle diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index ff1281fde..7fe9cdedb 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -362,8 +362,7 @@ class gui () = let main = new mainWin () in let fileSel = new fileSelectionWin () in let findRepl = new findReplWin () in - let develList = new develListWin () in - let newDevel = new newDevelWin () in + let newRoot = new newRootWin () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ main#mainWinEventBox ] in @@ -387,7 +386,7 @@ class gui () = val mutable _ok_not_exists = false val mutable _only_directory = false val mutable font_size = default_font_size - val mutable next_devel_must_contain = None + 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 @@ -632,13 +631,11 @@ class gui () = (* interface lockers *) let lock_world _ = main#buttonsToolbar#misc#set_sensitive false; - develList#buttonsHbox#misc#set_sensitive false; main#scriptMenu#misc#set_sensitive false; source_view#set_editable false in let unlock_world _ = main#buttonsToolbar#misc#set_sensitive true; - develList#buttonsHbox#misc#set_sensitive true; main#scriptMenu#misc#set_sensitive true; source_view#set_editable true; (*The next line seems sufficient to avoid some unknown race condition *) @@ -723,128 +720,26 @@ class gui () = f (); source_view#misc#grab_focus () with exc -> source_view#misc#grab_focus (); raise exc in - (* developments win *) - let model = - new MatitaGtkMisc.multiStringListModel - ~cols:2 develList#developmentsTreeview - in - let refresh_devels_win () = - model#list_store#clear (); - List.iter - (fun (name, root) -> model#easy_mappend [name;root]) - (MatitamakeLib.list_known_developments ()) - in - let get_devel_selected () = - match model#easy_mselection () with - | [[name;_]] -> MatitamakeLib.development_for_name name - | _ -> None - in - let refresh () = - while Glib.Main.pending () do - ignore(Glib.Main.iteration false); - done - in - connect_button develList#newButton - (fun () -> - next_devel_must_contain <- None; - newDevel#toplevel#misc#show()); - connect_button develList#deleteButton - (locker (fun () -> - (match get_devel_selected () with - | None -> () - | Some d -> MatitamakeLib.destroy_development_in_bg refresh d); - refresh_devels_win ())); - connect_button develList#buildButton - (locker (fun () -> - match get_devel_selected () with - | None -> () - | Some d -> - let build = locker - (fun () -> MatitamakeLib.build_development_in_bg refresh d) - in - ignore(build ()))); - connect_button develList#cleanButton - (locker (fun () -> - match get_devel_selected () with - | None -> () - | Some d -> - let clean = locker - (fun () -> MatitamakeLib.clean_development_in_bg refresh d) - in - ignore(clean ()))); - (* publish button hidden, use command line - connect_button develList#publishButton - (locker (fun () -> - match get_devel_selected () with - | None -> () - | Some d -> - let publish = locker (fun () -> - MatitamakeLib.publish_development_in_bg refresh d) in - ignore(publish ()))); - *) - develList#publishButton#misc#hide (); - connect_button develList#graphButton (fun () -> - match get_devel_selected () with - | None -> () - | Some d -> - (match MatitamakeLib.dot_for_development d with - | None -> () - | Some _ -> - let browser = MatitaMathView.cicBrowser () in - browser#load (`Development - (MatitamakeLib.name_for_development d)))); - connect_button develList#closeButton - (fun () -> develList#toplevel#misc#hide()); - ignore(develList#toplevel#event#connect#delete - (fun _ -> develList#toplevel#misc#hide();true)); - connect_menu_item main#developmentsMenuItem - (fun () -> refresh_devels_win ();develList#toplevel#misc#show ()); - - (* add development win *) - let check_if_root_contains root = - match next_devel_must_contain with - | None -> true - | Some path -> - let is_prefix_of d1 d2 = - let d1 = MatitamakeLib.normalize_path d1 in - let d2 = MatitamakeLib.normalize_path d2 in - let len1 = String.length d1 in - let len2 = String.length d2 in - if len2 < len1 then - false - else - let pref = String.sub d2 0 len1 in - pref = d1 - in - is_prefix_of root path - in - connect_button newDevel#addButton + (* add root win *) + connect_button newRoot#addButton (fun () -> - let name = newDevel#nameEntry#text in - let root = newDevel#rootEntry#text in - if check_if_root_contains root then - begin - ignore (MatitamakeLib.initialize_development name root); - refresh_devels_win (); - newDevel#nameEntry#set_text ""; - newDevel#rootEntry#set_text ""; - newDevel#toplevel#misc#hide() - end - else - HLog.error ("The selected root does not contain " ^ - match next_devel_must_contain with - | Some x -> x - | _ -> assert false)); - connect_button newDevel#chooseRootButton + 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 -> newDevel#rootEntry#set_text path + | Some path -> newRoot#rootEntry#set_text path | None -> ()); - connect_button newDevel#cancelButton - (fun () -> newDevel#toplevel#misc#hide ()); - ignore(newDevel#toplevel#event#connect#delete - (fun _ -> newDevel#toplevel#misc#hide();true)); + 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)); @@ -1291,8 +1186,7 @@ class gui () = method fileSel = fileSel method findRepl = findRepl method main = main - method develList = develList - method newDevel = newDevel + method newRoot = newRoot method newBrowserWin () = object (self) @@ -1346,9 +1240,9 @@ class gui () = (* we should check that this is a directory *) chosen_file - method createDevelopment ~containing = - next_devel_must_contain <- containing; - newDevel#toplevel#misc#show() + method createRoot ~containing = + next_root_must_contain <- containing; + newRoot#toplevel#misc#show() method askText ?(title = "") ?(msg = "") () = let dialog = new textDialog () in diff --git a/matita/matitaGuiTypes.mli b/matita/matitaGuiTypes.mli index 71cda4ac9..5a166fbd4 100644 --- a/matita/matitaGuiTypes.mli +++ b/matita/matitaGuiTypes.mli @@ -49,8 +49,7 @@ object method fileSel : MatitaGeneratedGui.fileSelectionWin method main : MatitaGeneratedGui.mainWin method findRepl : MatitaGeneratedGui.findReplWin - method develList: MatitaGeneratedGui.develListWin - method newDevel: MatitaGeneratedGui.newDevelWin + method newRoot: MatitaGeneratedGui.newRootWin (* method toolbar : MatitaGeneratedGui.toolBarWin *) method console: console @@ -87,7 +86,7 @@ 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 createDevelopment: containing:string option -> unit + 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/matitaInit.ml b/matita/matitaInit.ml index 58aadf76f..7bdf36a1a 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -26,7 +26,7 @@ (* $Id$ *) type thingsToInitilaize = - ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry + ConfigurationFile | Db | Environment | Getter | CmdLine | Registry exception FailedToInitialize of thingsToInitilaize @@ -102,16 +102,6 @@ let initialize_db init_status = else init_status -let initialize_makelib init_status = - wants [ConfigurationFile] init_status; - if not (already_configured [Makelib] init_status) then - begin - MatitamakeLib.initialize (); - Makelib::init_status - end - else - init_status - let initialize_environment init_status = wants [CmdLine] init_status; if not (already_configured [Getter;Environment] init_status) then @@ -324,18 +314,12 @@ let conf_components = [ load_configuration; fill_registry; parse_cmdline] let other_components = - [ initialize_makelib; initialize_db; initialize_environment ] + [ initialize_db; initialize_environment ] let initialize_all () = status := List.fold_left (fun s f -> f s) !status (conf_components @ other_components) -(* initialize_notation - (initialize_environment - (initialize_db - (initialize_makelib - (load_configuration - (parse_cmdline !status))))) *) let parse_cmdline_and_configuration_file () = status := List.fold_left (fun s f -> f s) !status conf_components diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml index 23f57820d..ff79f54ed 100644 --- a/matita/matitaMathView.ml +++ b/matita/matitaMathView.ml @@ -904,10 +904,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ignore (win#toplevel#event#connect#delete (fun _ -> let my_id = Oo.id self in cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers; - if !cicBrowsers = [] && - Helm_registry.get "matita.mode" = "cicbrowser" - then - GMain.quit (); false)); ignore(win#whelpResultTreeview#connect#row_activated ~callback:(fun _ _ -> @@ -1045,7 +1041,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `About `Coercions -> self#coerchgraph true () | `Check term -> self#_loadCheck term | `Cic (term, metasenv) -> self#_loadTermCic term metasenv - | `Development d -> self#_showDevelDeps d | `Dir dir -> self#_loadDir dir | `HBugs `Tutors -> self#_loadHBugsTutors | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) -> @@ -1136,16 +1131,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry); current_entry <- entry - method private _showDevelDeps d = - match MatitamakeLib.development_for_name d with - | None -> () - | Some devel -> - (match MatitamakeLib.dot_for_development devel with - | None -> () - | Some fname -> - gviz#load_graph_from_file ~gviz_cmd:"tred | dot" fname; - self#_showGviz) - method private _loadObj obj = (* showMath must be done _before_ loading the document, since if the * widget is not mapped (hidden by the notebook) the document is not diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index c4cb286b3..255a0dde1 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -69,7 +69,6 @@ type guistuff = { mathviewer:MatitaTypes.mathViewer; urichooser: UriManager.uri list -> UriManager.uri list; ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; - develcreator: containing:string option -> unit; } let eval_with_engine guistuff lexicon_status grafite_status user_goal @@ -101,80 +100,32 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal ([],skipped_txt) enriched_history_fragment in res,"",parsed_text_length +;; -let wrap_with_developments guistuff f arg = - let compile_needed_and_go_on lexiconfile d exc = - let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" lexiconfile in - let target = Pcre.replace ~pat:"metadata$" ~templ:"moo" target in - let refresh_cb () = - while Glib.Main.pending () do ignore(Glib.Main.iteration false); done - in - if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then - raise exc - else - f arg - in - let do_nothing () = raise (ActionCancelled "Inclusion not performed") in - let check_if_file_is_exists f = - assert(Pcre.pmatch ~pat:"ma$" f); - let pwd = Sys.getcwd () in - let f_pwd = pwd ^ "/" ^ f in - if not (HExtlib.is_regular f_pwd) then - raise (ActionCancelled ("File "^f_pwd^" does not exists!")) - else - raise - (ActionCancelled - ("Internal error: "^f_pwd^" exists but I'm unable to include it!")) - in - let handle_with_devel d lexiconfile mafile exc = - let name = MatitamakeLib.name_for_development d in - let title = "Unable to include " ^ lexiconfile in - let message = - mafile ^ " is handled by development " ^ name ^ ".\n\n" ^ - "Should I compile it and Its dependencies?" - in - (match guistuff.ask_confirmation ~title ~message with - | `YES -> compile_needed_and_go_on lexiconfile d exc - | `NO -> raise exc - | `CANCEL -> do_nothing ()) - in - let handle_without_devel mafilename exc = - let title = "Unable to include " ^ mafilename in - let message = - mafilename ^ " is not handled by a development.\n" ^ - "All dependencies are automatically solved for a development.\n\n" ^ - "Do you want to set up a development?" - in - (match guistuff.ask_confirmation ~title ~message with - | `YES -> - guistuff.develcreator ~containing:(Some (Filename.dirname mafilename)); - do_nothing () - | `NO -> raise exc - | `CANCEL -> do_nothing()) - in - try - f arg +let wrap_with_make g f x = + try + f x with - | DependenciesParser.UnableToInclude mafilename -> +(* + | DependenciesParser.UnableToInclude mafilename -> assert (Pcre.pmatch ~pat:"ma$" mafilename); check_if_file_is_exists mafilename - | LexiconEngine.IncludedFileNotCompiled (xfilename,mafilename) +*) + | LexiconEngine.IncludedFileNotCompiled (xfilename,mafilename) | GrafiteEngine.IncludedFileNotCompiled (xfilename,mafilename) as exn -> assert (Pcre.pmatch ~pat:"ma$" mafilename); - assert (Pcre.pmatch ~pat:"lexicon$" xfilename || + assert (Pcre.pmatch ~pat:"lexicon$" xfilename || Pcre.pmatch ~pat:"mo$" xfilename ); (* we know that someone was able to include the .ma, get the baseuri * but was unable to get the compilation output 'xfilename' *) - match MatitamakeLib.development_for_dir (Filename.dirname mafilename) with - | None -> handle_without_devel mafilename exn - | Some d -> handle_with_devel d xfilename mafilename exn + raise exn ;; - + let eval_with_engine guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt st = - wrap_with_developments guistuff + wrap_with_make guistuff (eval_with_engine guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt) st @@ -680,7 +631,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; let ast = - wrap_with_developments guistuff + wrap_with_make guistuff (GrafiteParser.parse_statement (Ulexing.from_utf8_string text) ~include_paths) lexicon_status in @@ -739,7 +690,7 @@ class script ~(source_view: GSourceView.source_view) ~set_star ~ask_confirmation ~urichooser - ~develcreator + ~rootcreator () = let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in @@ -765,7 +716,6 @@ object (self) mathviewer = mathviewer; urichooser = urichooser; ask_confirmation = ask_confirmation; - develcreator=develcreator; } val mutable filename_ = (None : string option) @@ -1162,10 +1112,10 @@ end let _script = ref None -let script ~source_view ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star () +let script ~source_view ~mathviewer ~urichooser ~rootcreator ~ask_confirmation ~set_star () = let s = new script - ~source_view ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () + ~source_view ~mathviewer ~ask_confirmation ~urichooser ~rootcreator ~set_star () in _script := Some s; s diff --git a/matita/matitaScript.mli b/matita/matitaScript.mli index 8f120b296..89986ead7 100644 --- a/matita/matitaScript.mli +++ b/matita/matitaScript.mli @@ -92,7 +92,7 @@ val script: source_view:GSourceView.source_view -> mathviewer: MatitaTypes.mathViewer-> urichooser: (UriManager.uri list -> UriManager.uri list) -> - develcreator: (containing:string option -> unit) -> + rootcreator: (containing:string option -> unit) -> ask_confirmation: (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> set_star: (bool -> unit) -> diff --git a/matita/matitaTypes.ml b/matita/matitaTypes.ml index 23d0d832f..0c8952e89 100644 --- a/matita/matitaTypes.ml +++ b/matita/matitaTypes.ml @@ -43,7 +43,6 @@ type mathViewer_entry = [ `About of abouts (* current proof *) | `Check of string (* term *) | `Cic of Cic.term * Cic.metasenv - | `Development of string | `Dir of string (* "directory" in cic uris namespace *) | `HBugs of [ `Tutors ] (* list of available HBugs tutors *) | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] @@ -59,7 +58,6 @@ let string_of_entry = function | `About `CoercionsFull -> "about:coercions" | `Check _ -> "check:" | `Cic (_, _) -> "term:" - | `Development d -> "devel:/" ^ d | `Dir uri -> uri | `HBugs `Tutors -> "hbugs:/tutors/" | `Metadata meta -> diff --git a/matita/matitaTypes.mli b/matita/matitaTypes.mli index c71c99dcc..67655c921 100644 --- a/matita/matitaTypes.mli +++ b/matita/matitaTypes.mli @@ -31,7 +31,6 @@ type mathViewer_entry = [ `About of abouts | `Check of string | `Cic of Cic.term * Cic.metasenv - | `Development of string | `Dir of string | `HBugs of [ `Tutors ] | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] diff --git a/matita/matitac.ml b/matita/matitac.ml index 8645d2175..8f8a19b2d 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -145,12 +145,9 @@ let main_compiler () = let main () = Helm_registry.set_bool "matita.moo" true; match Filename.basename Sys.argv.(0) with - |"gragrep" |"gragrep.opt" |"gragrep.opt.static" ->Gragrep.main() |"matitadep" |"matitadep.opt" |"matitadep.opt.static" ->Matitadep.main() |"matitaclean"|"matitaclean.opt"|"matitaclean.opt.static"->Matitaclean.main() - |"matitamake" |"matitamake.opt" |"matitamake.opt.static" ->Matitamake.main() - |"matitaprover"|"matitaprover.opt" - |"matitaprover.opt.static" ->Matitaprover.main() + |"matitaprover"|"matitaprover.opt"|"matitaprover.opt.static"->Matitaprover.main() |"matitawiki"|"matitawiki.opt" ->MatitaWiki.main() | _ -> let dump_msg = " Dump with expanded macros to " in diff --git a/matita/matitadep.ml b/matita/matitadep.ml index 4e309ae75..995230c45 100644 --- a/matita/matitadep.ml +++ b/matita/matitadep.ml @@ -66,7 +66,6 @@ let main () = " Save dependency graph in dot format to the given file";]; MatitaInit.parse_cmdline_and_configuration_file (); MatitaInit.initialize_environment (); - MatitamakeLib.initialize (); let args = Helm_registry.get_list Helm_registry.string "matita.args" in let args = if args = [] then diff --git a/matita/matitamake.ml b/matita/matitamake.ml deleted file mode 100644 index ad4368738..000000000 --- a/matita/matitamake.ml +++ /dev/null @@ -1,135 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -module MK = MatitamakeLib ;; - -let main () = - MatitaInit.parse_cmdline_and_configuration_file (); - MK.initialize (); - let usage = ref (fun () -> ()) in - let dev_of_name name = - match MK.development_for_name name with - | None -> - prerr_endline ("Unable to find a development called " ^ name); - exit 1 - | Some d -> d - in - let dev_for_dir dir = - match MK.development_for_dir dir with - | None -> - prerr_endline ("Unable to find a development holding directory: "^ dir); - exit 1 - | Some d -> d - in - let init_dev args = - let name, path = - match args with - | [ name; path ] when path.[0] = '/' -> name, path - | [ name; path ] -> name, Unix.getcwd () ^ "/" ^ path - | [ name ] -> name, Unix.getcwd () - | _ -> !usage (); (* should not be reached *) assert false - in - match MK.initialize_development name path with - | None -> exit 2 - | Some _ -> exit 0 - in - let list_dev args = - if List.length args <> 0 then !usage (); - match MK.list_known_developments () with - | [] -> print_string "No developments found.\n"; exit 0 - | l -> - List.iter - (fun (name, root) -> - print_string (Printf.sprintf "%-10s\trooted in %s\n" name root)) - l; - exit 0 - in - let destroy_dev args = - if List.length args <> 1 then !usage (); - let name = (List.hd args) in - let dev = dev_of_name name in - MK.destroy_development dev; - exit 0 - in - let clean_dev args = - let dev = - match args with - | [] -> dev_for_dir (Unix.getcwd ()) - | [name] -> dev_of_name name - | _ -> !usage (); exit 1 - in - match MK.clean_development dev with - | true -> exit 0 - | false -> exit 1 - in - let build_dev args = - if List.length args <> 1 then !usage (); - let name = (List.hd args) in - let dev = dev_of_name name in - match MK.build_development dev with - | true -> exit 0 - | false -> exit 1 - in - let publish_dev args = - if List.length args <> 1 then !usage (); - let name = (List.hd args) in - let dev = dev_of_name name in - match MK.publish_development dev with - | true -> exit 0 - | false -> exit 1 - in - let target args = - if List.length args < 1 then !usage (); - let dev = dev_for_dir (Unix.getcwd ()) in - List.iter - (fun t -> - ignore(MK.build_development ~target:t dev)) - args - in - let params = [ - "init", init_dev; - "clean", clean_dev; - "list", list_dev; - "destroy", destroy_dev; - "build", build_dev; - "publish", publish_dev; - ] - in - usage := MatitaInit.die_usage; - let parse args = - match args with - | [] -> target [ "all" ] - | s :: tl -> - let f, args = - try - (List.assoc s params), tl - with Not_found -> - if s.[0] = '-' then (!usage ();assert false) else target, args - in - f args - in - parse (Helm_registry.get_list Helm_registry.string "matita.args") diff --git a/matita/matitamake.mli b/matita/matitamake.mli deleted file mode 100644 index 47ea2fe34..000000000 --- a/matita/matitamake.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* Copyright (C) 2006, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -val main : unit -> unit - diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml deleted file mode 100644 index 499d0eaf3..000000000 --- a/matita/matitamakeLib.ml +++ /dev/null @@ -1,394 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -open Printf - -let logger = fun mark -> - match mark with - | `Error -> HLog.error - | `Warning -> HLog.warn - | `Debug -> HLog.debug - | `Message -> HLog.message - -type development = - { root: string ; name: string } - -let developments = ref [] - -let pool () = Helm_registry.get "matita.basedir" ^ "/matitamake/" ;; -let rootfile = "/root" ;; - -(* /foo/./bar/..//baz -> /foo/baz *) -let normalize_path s = - let s = Str.global_replace (Str.regexp "//") "/" s in - let l = Str.split (Str.regexp "/") s in - let rec aux = function - | [] -> [] - | he::".."::tl -> aux tl - | he::"."::tl -> aux (he::tl) - | he::tl -> he :: aux tl - in - (if Str.string_match (Str.regexp "^/") s 0 then "/" else "") ^ - String.concat "/" (aux l) - ^ (if Str.string_match (Str.regexp "/$") s 0 then "/" else "") -;; - -let ls_dir dir = - try - let d = Unix.opendir dir in - let content = ref [] in - try - while true do - let name = Unix.readdir d in - if name <> "." && name <> ".." then - content := name :: !content - done; - Some [] - with End_of_file -> Unix.closedir d; Some !content - with Unix.Unix_error _ -> None - -let initialize () = - (* create a base env if none *) - HExtlib.mkdir (pool ()); - (* load developments *) - match ls_dir (pool ()) with - | None -> logger `Error ("Unable to list directory " ^ pool ()) - | Some l -> - let paths = - List.fold_left - (fun acc name -> - let root = - try - Some (HExtlib.input_file (pool () ^ name ^ rootfile)) - with Unix.Unix_error _ -> - logger `Warning ("Malformed development " ^ name); - None - in - match root with - | None -> acc - | Some root -> - developments := {root = root ; name = name} :: !developments; - root::acc) - [] l - in - let inc = Helm_registry.get_list Helm_registry.string "matita.includes" in - Helm_registry.set_list Helm_registry.of_string - ~key:"matita.includes" ~value:(inc @ paths) - -(* finds the makefile path for development devel *) -let makefile_for_development devel = - let develdir = pool () ^ devel.name in - develdir ^ "/makefile" - -let dot_for_development devel = - let dot_fname = pool () ^ devel.name ^ "/depend.dot" in - if Sys.file_exists dot_fname then Some dot_fname else None - -(* given a dir finds a development that is radicated in it or below *) -let development_for_dir dir = - let dir = normalize_path dir in - let is_prefix_of d1 d2 = - let len1 = String.length d1 in - let len2 = String.length d2 in - if len2 < len1 then - false - else - let pref = String.sub d2 0 len1 in - pref = d1 && (len1 = len2 || d2.[len1] = '/') - in - try - Some (List.find (fun d -> is_prefix_of d.root dir) !developments) - with Not_found | Failure _ -> None - -let development_for_name name = - try - Some (List.find (fun d -> d.name = name) !developments) - with Not_found -> None - -(* dumps the deveopment to disk *) -let dump_development devel = - let devel_dir = pool () ^ devel.name in - HExtlib.mkdir devel_dir; - HExtlib.output_file ~filename:(devel_dir ^ rootfile) ~text:devel.root - -let list_known_developments () = - List.map (fun r -> r.name,r.root) !developments - -let am_i_opt = lazy ( - if Pcre.pmatch ~pat:"\\.opt$" Sys.argv.(0) then ".opt" else "") - -let rebuild_makefile development = - let makefilepath = makefile_for_development development in - let template = - HExtlib.input_file BuildTimeConf.matitamake_makefile_template - in - let ext = Lazy.force am_i_opt in - let binpath = - if HExtlib.is_executable - (BuildTimeConf.runtime_base_dir ^ "/matitac" ^ ext) - then BuildTimeConf.runtime_base_dir ^ "/" else "" - in - let cc = binpath ^ "matitac" ^ ext in - let rm = binpath ^ "matitaclean" ^ ext in - let mm = binpath ^ "matitadep" ^ ext in - let df = pool () ^ development.name ^ "/depend" in - let template = Pcre.replace ~pat:"@ROOT@" ~templ:development.root template in - let template = Pcre.replace ~pat:"@CC@" ~templ:cc template in - let template = Pcre.replace ~pat:"@DEP@" ~templ:mm template in - let template = Pcre.replace ~pat:"@DEPFILE@" ~templ:df template in - let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in - HExtlib.output_file ~filename:makefilepath ~text:template - -let rebuild_makefile_devel development = - let path = development.root ^ "/makefile" in - if not (Sys.file_exists path) then - begin - let template = - HExtlib.input_file BuildTimeConf.matitamake_makefile_template_devel - in - let template = - Pcre.replace ~pat:"@MATITA_RT_BASE_DIR@" - ~templ:BuildTimeConf.runtime_base_dir template - in - HExtlib.output_file ~filename:path ~text:template - end - -(* creates a new development if possible *) -let initialize_development name dir = - let dir = normalize_path dir in - let name = Pcre.replace ~pat:" " ~templ:"_" name in - let dev = {name = name ; root = dir} in - dump_development dev; - rebuild_makefile dev; - rebuild_makefile_devel dev; - developments := dev :: !developments; - Some dev - -let make chdir args = - let old = Unix.getcwd () in - try - Unix.chdir chdir; - let cmd = String.concat " " ("make" :: List.map Filename.quote args) in - let rc = Unix.system cmd in - Unix.chdir old; - match rc with - | Unix.WEXITED 0 -> true - | Unix.WEXITED i -> logger `Error ("make returned " ^ string_of_int i);false - | _ -> logger `Error "make STOPPED or SIGNALED!";false - with Unix.Unix_error (_,cmd,err) -> - logger `Warning ("Unix Error: " ^ cmd ^ ": " ^ err); - false - -let call_make ?matita_flags development target make = - let matita_flags = - let already_defined = - match matita_flags with - | None -> (try Sys.getenv "MATITA_FLAGS" with Not_found -> "") - | Some s -> s - in - let bench = - if Helm_registry.get_bool "matita.bench" then " -bench" else "" - in - let system = - if Helm_registry.get_bool "matita.system" then " -system" else "" - in - let noinnertypes = - if Helm_registry.get_bool "matita.noinnertypes" then " -noinnertypes" else "" - in - already_defined ^ bench ^ system ^ noinnertypes - in - let csc = try ["SRC=" ^ Sys.getenv "SRC"] with Not_found -> [] in - rebuild_makefile development; - let makefile = makefile_for_development development in - let flags = [] in - let flags = - try - flags @ [ sprintf "MATITA_FLAGS=%s" matita_flags ] - with Not_found -> flags in - let flags = flags @ csc in - let args = - ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] @ flags - in - (* prerr_endline (String.concat " " args); *) - make development.root args - -let build_development ?matita_flags ?(target="all") development = - call_make ?matita_flags development target make - -(* not really good vt100 *) -let vt100 s = - let rex = Pcre.regexp "\\[[0-9;]+m" in - let rex_i = Pcre.regexp "^Info" in - let rex_w = Pcre.regexp "^Warning" in - let rex_e = Pcre.regexp "^Error" in - let rex_d = Pcre.regexp "^Debug" in - let rex_noendline = Pcre.regexp "\\n" in - let s = Pcre.replace ~rex:rex_noendline s in - let tokens = Pcre.split ~rex s in - let logger = ref HLog.message in - let rec aux = - function - | [] -> () - | s::tl -> - (if Pcre.pmatch ~rex:rex_i s then - logger := HLog.message - else if Pcre.pmatch ~rex:rex_w s then - logger := HLog.warn - else if Pcre.pmatch ~rex:rex_e s then - logger := HLog.error - else if Pcre.pmatch ~rex:rex_d s then - logger := HLog.debug - else - !logger s); - aux tl - in - aux tokens - - -let mk_maker refresh_cb = - (fun chdir args -> - let out_r,out_w = Unix.pipe () in - let err_r,err_w = Unix.pipe () in - let pid = ref ~-1 in - let oldhandler = Sys.signal Sys.sigchld (Sys.Signal_ignore) in - try -(* prerr_endline (String.concat " " args); *) - let argv = Array.of_list ("make"::args) in - pid := Unix.create_process "make" argv Unix.stdin out_w err_w; - Unix.close out_w; - Unix.close err_w; - let buf = String.create 1024 in - let rec aux = function - | f::tl -> - let len = Unix.read f buf 0 1024 in - if len = 0 then - raise - (Unix.Unix_error - (Unix.EPIPE,"read","len = 0 (matita internal)")); - vt100 (String.sub buf 0 len); - aux tl - | _ -> () - in - while true do - let r,_,_ = Unix.select [out_r; err_r] [] [] (-. 1.) in - aux r; - refresh_cb () - done; - ignore(Sys.signal Sys.sigchld oldhandler); - true - with - | Unix.Unix_error (_,"read",_) - | Unix.Unix_error (_,"select",_) -> - ignore(Sys.signal Sys.sigchld oldhandler); - true) - -let build_development_in_bg ?matita_flags ?(target="all") refresh_cb development = - call_make ?matita_flags development target (mk_maker refresh_cb) - -let clean_development ?matita_flags development = - call_make ?matita_flags development "clean" make - -let clean_development_in_bg ?matita_flags refresh_cb development = - call_make development ?matita_flags "clean" (mk_maker refresh_cb) - -let destroy_development_aux development clean_development = - let delete_development development = - let unlink = HExtlib.safe_remove in - let rmdir dir = - try - Unix.rmdir dir - with Unix.Unix_error _ -> - logger `Warning ("Unable to remove dir " ^ dir); - match ls_dir dir with - | None -> logger `Error ("Unable to list directory " ^ dir) - | Some [] -> () - | Some l -> logger `Error ("The directory is not empty") - in - unlink (makefile_for_development development); - unlink (pool () ^ development.name ^ rootfile); - unlink (pool () ^ development.name ^ "/depend"); - unlink (pool () ^ development.name ^ "/depend.errors"); - unlink (pool () ^ development.name ^ "/depend.dot"); - rmdir (pool () ^ development.name); - developments := - List.filter (fun d -> d.name <> development.name) !developments - in - if not(clean_development development) then - begin - logger `Warning "Unable to clean the development problerly."; - logger `Warning "This may cause garbage." - end; - delete_development development - -let destroy_development ?matita_flags development = - destroy_development_aux development (clean_development ?matita_flags) - -let destroy_development_in_bg ?matita_flags refresh development = - destroy_development_aux development - (clean_development_in_bg refresh ?matita_flags ) - -let root_for_development development = development.root -let name_for_development development = development.name - -let publish_development_bstract build clean devel = - let matita_flags, matita_flags_system = - let orig_matita_flags = - try Sys.getenv "MATITA_FLAGS" with Not_found -> "" - in - orig_matita_flags, orig_matita_flags ^ " -system" - in - HLog.message "cleaning the development before publishing"; - if clean ~matita_flags devel then - begin - HLog.message "rebuilding the development in 'system' space"; - (* here we should use pristine metadata if we use sqlite *) - if build ~matita_flags:matita_flags_system devel then - begin - HLog.message "publishing succeded"; - true - end - else - begin - HLog.error "building process failed, reverting"; - if not (clean ~matita_flags devel) then - HLog.error "cleaning failed, end of the world (2)"; - false - end - end - else - (HLog.error "unable to clean the development, publishing failed"; false) - -let publish_development devel = - publish_development_bstract - (fun ~matita_flags devel -> build_development ~matita_flags devel) - (fun ~matita_flags devel -> clean_development ~matita_flags devel) devel -let publish_development_in_bg cb devel = - publish_development_bstract - (fun ~matita_flags devel -> build_development_in_bg cb ~matita_flags devel) - (fun ~matita_flags devel -> clean_development_in_bg cb ~matita_flags devel) - devel - diff --git a/matita/matitamakeLib.mli b/matita/matitamakeLib.mli deleted file mode 100644 index 8f6fda2e4..000000000 --- a/matita/matitamakeLib.mli +++ /dev/null @@ -1,62 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -type development - -(* initialize_development [name] [dir] - * ask matitamake to recorder [dir] as the root for thedevelopment [name] *) -val initialize_development: string -> string -> development option -(* make target [default all] *) -val build_development: ?matita_flags:string -> ?target:string -> development -> bool -(* make target [default all], the refresh cb is called after every output *) -val build_development_in_bg: - ?matita_flags:string -> ?target:string -> (unit -> unit) -> development -> bool -(* make clean *) -val clean_development: ?matita_flags:string -> development -> bool -val clean_development_in_bg: ?matita_flags:string -> (unit -> unit) -> development -> bool - -val publish_development_in_bg: (unit -> unit) -> development -> bool -val publish_development: development -> bool - -(* return the development that handles dir *) -val development_for_dir: string -> development option -(* return the development *) -val development_for_name: string -> development option -(* return the known list of name, development_root *) -val list_known_developments: unit -> (string * string ) list -(* cleans the development, forgetting about it *) -val destroy_development: ?matita_flags:string -> development -> unit -val destroy_development_in_bg: ?matita_flags:string -> (unit -> unit) -> development -> unit -(* initiale internal data structures *) -val initialize : unit -> unit -(* gives back the root *) -val root_for_development : development -> string -(* gives back the name *) -val name_for_development : development -> string - -(** @return dot file for a given development, if it exists *) -val dot_for_development : development -> string option - -val normalize_path: string -> string -- 2.39.2