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
| _ -> 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^""); *)
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,
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
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
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 \
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 \
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
lablGraphviz.mli \
matitaTypes.mli \
matitaMisc.mli \
- matitamakeLib.mli \
matitaExcPp.mli \
matitaInit.mli \
matitaEngine.mli \
make.mli \
matitaTypes.mli \
matitaMisc.mli \
- matitamakeLib.mli \
matitaExcPp.mli \
matitaInit.mli \
matitaEngine.mli \
MAINCMLI = \
matitadep.mli \
matitaclean.mli \
- matitamake.mli \
- gragrep.mli \
$(NULL)
# objects for matita (GTK GUI)
ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.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
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
$(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 $< $@
+++ /dev/null
-(* 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 ()
-
+++ /dev/null
-(* 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
-
</child>
</widget>
</child>
+ <!--
<child>
<widget class="GtkImageMenuItem" id="developmentsMenuItem">
<property name="visible">True</property>
</child>
</widget>
</child>
+ -->
<child>
<widget class="GtkSeparatorMenuItem" id="separator2">
<property name="visible">True</property>
</widget>
</child>
</widget>
- <widget class="GtkWindow" id="NewDevelWin">
- <property name="title" translatable="yes">Create development</property>
- <property name="resizable">False</property>
+ <widget class="GtkWindow" id="NewRootWin">
+ <property name="title" translatable="yes">Create root file</property>
+ <property name="resizable">True</property>
<property name="modal">True</property>
<property name="window_position">GTK_WIN_POS_CENTER_ALWAYS</property>
<property name="type_hint">GDK_WINDOW_TYPE_HINT_UTILITY</property>
</packing>
</child>
<child>
- <widget class="GtkEntry" id="nameEntry">
+ <widget class="GtkEntry" id="buriEntry">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="invisible_char">*</property>
<widget class="GtkLabel" id="label20">
<property name="visible">True</property>
<property name="xalign">0</property>
- <property name="label" translatable="yes">Name</property>
+ <property name="label" translatable="yes">Base URI</property>
</widget>
<packing>
<property name="x_options">GTK_FILL</property>
</widget>
</child>
</widget>
+ <!--
<widget class="GtkWindow" id="DevelListWin">
<property name="title" translatable="yes">Developments</property>
<property name="window_position">GTK_WIN_POS_CENTER</property>
</widget>
</child>
</widget>
+ -->
<widget class="GtkDialog" id="DisambiguationErrors">
<property name="width_request">450</property>
<property name="height_request">400</property>
(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 ();
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
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
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
(* 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 *)
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));
method fileSel = fileSel
method findRepl = findRepl
method main = main
- method develList = develList
- method newDevel = newDevel
+ method newRoot = newRoot
method newBrowserWin () =
object (self)
(* 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
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
* @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
(* $Id$ *)
type thingsToInitilaize =
- ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry
+ ConfigurationFile | Db | Environment | Getter | CmdLine | Registry
exception FailedToInitialize of thingsToInitilaize
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
[ 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
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 _ _ ->
| `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)) ->
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
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
([],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 <b>" ^ name ^ "</b>.\n\n" ^
- "<i>Should I compile it and Its dependencies?</i>"
- 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 <b>not</b> handled by a development.\n" ^
- "All dependencies are automatically solved for a development.\n\n" ^
- "<i>Do you want to set up a development?</i>"
- 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
| `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
~set_star
~ask_confirmation
~urichooser
- ~develcreator
+ ~rootcreator
() =
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
mathviewer = mathviewer;
urichooser = urichooser;
ask_confirmation = ask_confirmation;
- develcreator=develcreator;
}
val mutable filename_ = (None : string option)
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
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) ->
[ `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 ]
| `About `CoercionsFull -> "about:coercions"
| `Check _ -> "check:"
| `Cic (_, _) -> "term:"
- | `Development d -> "devel:/" ^ d
| `Dir uri -> uri
| `HBugs `Tutors -> "hbugs:/tutors/"
| `Metadata meta ->
[ `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 ]
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 = "<filename> Dump with expanded macros to <filename>" in
"<file> 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
+++ /dev/null
-(* 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")
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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 "\e\\[[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
-
+++ /dev/null
-(* 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
projects / helm.git / commitdiff