-matita.conf.xml
*.a
*.annot
autom4te.cache
config.status
configure
.depend
+dump_moo
+gtkmathview.matita.conf.xml
Makefile
matita
.matita
matitac
+matitaclean
+matitaclean.opt
+matita.conf.xml
+matita.conf.xml
+matita.conf.xml.sample
matitac.opt
+matitadep
+matitadep.opt
matitaGeneratedGui.ml
matitaGeneratedGui.mli
matita.glade.bak
matita.gladep
matita.gladep.bak
+matitamake
+matitamake.opt
matita.opt
matita.opt
matitatop
-matitadep
-matitadep.opt
-matitaclean
-matitaclean.opt
-matitamake
-matitamake.opt
-dump_moo
+*.moo
*.o
+*.static
*.swp
-matita.conf.xml
-*.moo
-matita.conf.xml.sample
-gtkmathview.matita.conf.xml
+*.upx
dump_moo.cmo: matitaMoo.cmi matitaLog.cmi buildTimeConf.cmo
dump_moo.cmx: matitaMoo.cmx matitaLog.cmx buildTimeConf.cmx
matitacleanLib.cmo: matitaSync.cmi matitaMoo.cmi matitaMisc.cmi matitaLog.cmi \
- matitaDb.cmi matitacleanLib.cmi
+ matitaExcPp.cmi matitaDb.cmi buildTimeConf.cmo matitacleanLib.cmi
matitacleanLib.cmx: matitaSync.cmx matitaMoo.cmx matitaMisc.cmx matitaLog.cmx \
- matitaDb.cmx matitacleanLib.cmi
+ matitaExcPp.cmx matitaDb.cmx buildTimeConf.cmx matitacleanLib.cmi
matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi \
- matitaInit.cmi matitaDb.cmi
+ matitaInit.cmi matitaDb.cmi matitaclean.cmi
matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx \
- matitaInit.cmx matitaDb.cmx
+ matitaInit.cmx matitaDb.cmx matitaclean.cmi
matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMoo.cmi \
- matitaMisc.cmi matitaLog.cmi matitaInit.cmi matitaExcPp.cmi \
- matitaEngine.cmi matitaDb.cmi buildTimeConf.cmo matitacLib.cmi
+ matitaLog.cmi matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
+ matitaDb.cmi buildTimeConf.cmo matitacLib.cmi
matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMoo.cmx \
- matitaMisc.cmx matitaLog.cmx matitaInit.cmx matitaExcPp.cmx \
- matitaEngine.cmx matitaDb.cmx buildTimeConf.cmx matitacLib.cmi
-matitac.cmo: matitacLib.cmi
-matitac.cmx: matitacLib.cmx
+ matitaLog.cmx matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
+ matitaDb.cmx buildTimeConf.cmx matitacLib.cmi
+matitac.cmo: matitamake.cmo matitadep.cmi matitaclean.cmi matitacLib.cmi
+matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx
matitaDb.cmo: matitaMisc.cmi matitaDb.cmi
matitaDb.cmx: matitaMisc.cmx matitaDb.cmi
-matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaInit.cmi
-matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaInit.cmx
+matitadep.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaInit.cmi \
+ matitadep.cmi
+matitadep.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaInit.cmx \
+ matitadep.cmi
matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi
matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi
matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \
matitaLog.cmx: matitaLog.cmi
matitamakeLib.cmo: matitaLog.cmi buildTimeConf.cmo matitamakeLib.cmi
matitamakeLib.cmx: matitaLog.cmx buildTimeConf.cmx matitamakeLib.cmi
-matitamake.cmo: matitamakeLib.cmi matitaInit.cmi
-matitamake.cmx: matitamakeLib.cmx matitaInit.cmx
+matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo
+matitamake.cmx: matitamakeLib.cmx buildTimeConf.cmx
matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
matitaLog.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \
buildTimeConf.cmo matitaMathView.cmi
matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
matitaLog.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \
buildTimeConf.cmx matitaMathView.cmi
-matitaMisc.cmo: matitaTypes.cmi matitaLog.cmi matitaExcPp.cmi \
- buildTimeConf.cmo matitaMisc.cmi
-matitaMisc.cmx: matitaTypes.cmx matitaLog.cmx matitaExcPp.cmx \
- buildTimeConf.cmx matitaMisc.cmi
-matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
- matitaMathView.cmi matitaLog.cmi matitaInit.cmi matitaGui.cmi \
- matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo
-matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
- matitaMathView.cmx matitaLog.cmx matitaInit.cmx matitaGui.cmx \
- matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx
+matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi
+matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi
+matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi matitaLog.cmi \
+ matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaEngine.cmi \
+ buildTimeConf.cmo
+matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx matitaLog.cmx \
+ matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx matitaEngine.cmx \
+ buildTimeConf.cmx
matitaMoo.cmo: matitaTypes.cmi matitaMoo.cmi
matitaMoo.cmx: matitaTypes.cmx matitaMoo.cmi
matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \
matitaGui.cmi: matitaGuiTypes.cmi matitaDisambiguator.cmi
matitaGuiTypes.cmi: matitaTypes.cmi matitaLog.cmi matitaGeneratedGui.cmi
matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
-matitaMisc.cmi: matitaTypes.cmi
matitaMoo.cmi: matitaTypes.cmi
matitaScript.cmi: matitaTypes.cmi
matitaSync.cmi: matitaTypes.cmi
CREQUIRES = @FINDLIB_CREQUIRES@
DEPREQUIRES = @FINDLIB_DEPREQUIRES@
CLEANREQUIRES = @FINDLIB_CLEANREQUIRES@
+MAKEREQUIRES = @FINDLIB_MAKEREQUIRES@
HAVE_OCAMLOPT = @HAVE_OCAMLOPT@
OCAML_FLAGS = -pp $(CAMLP4O)
CPKGS = -package "$(CREQUIRES)"
DEPPKGS = -package "$(DEPREQUIRES)"
CLEANPKGS = -package "$(CLEANREQUIRES)"
+MAKEPKGS = -package "$(MAKEREQUIRES)"
OCAML_THREADS_FLAGS = -thread
OCAML_DEBUG_FLAGS = -g
OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS)
OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
STATIC_LINK = dist/static_link/static_link
+# for matita
STATIC_LIBS = \
t1 t1x \
gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \
mysqlclient \
expat \
$(NULL)
-STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++ -cclib -lart_lgpl_2
+STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++
+# for matitac & co
+STATIC_CLIBS = \
+ gdome \
+ mysqlclient \
+ $(NULL)
+STATIC_EXTRA_CLIBS =
MATITA_FLAGS =
NODB=false
matitaEngine.cmo \
matitacLib.cmo \
$(NULL)
+MAINCMOS = \
+ matitadep.cmo \
+ matitaclean.cmo \
+ matitamake.cmo \
+ $(NULL)
+DEPCMOS = $(CCMOS)
CLEANCMOS = $(CCMOS)
-MAKECMOS = $(CCMOS)
+MAKECMOS = \
+ buildTimeConf.cmo \
+ matitaLog.cmo \
+ matitamakeLib.cmo \
+ $(NULL)
PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo
PROGRAMS = $(PROGRAMS_BYTE) matitatop
PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT))
+PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC))
all: matita.conf.xml $(PROGRAMS) coq.moo
ifeq ($(HAVE_OCAMLOPT),yes)
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
+MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
+DEPCMXS = $(patsubst %.cmo,%.cmx,$(DEPCMOS))
CLEANCMXS = $(patsubst %.cmo,%.cmx,$(CLEANCMOS))
MAKECMXS = $(patsubst %.cmo,%.cmx,$(MAKECMOS))
LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES))
MAKELIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MAKEREQUIRES))
opt: $(PROGRAMS_OPT) coq.moo.opt
static: $(PROGRAMS_STATIC) coq.moo.opt
- strip *.static
+upx: $(PROGRAMS_UPX) coq.moo.opt
else
+upx:
+ @echo "Native code compilation is disabled"
opt:
@echo "Native code compilation is disabled"
static:
$(STATIC_LINK) $(STATIC_LIBS) -- \
$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
$(STATIC_EXTRA_LIBS)
+ strip $@
dump_moo: buildTimeConf.cmo matitaLog.cmo matitaMoo.cmo dump_moo.ml
$(OCAMLC) $(PKGS) -linkpkg -o $@ $^
dump_moo.opt: buildTimeConf.cmx matitaLog.cmx matitaMoo.cmx dump_moo.ml
$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^
dump_moo.opt.static: buildTimeConf.cmx matitaLog.cmx matitaMoo.cmx dump_moo.ml
- $(STATIC_LINK) $(STATIC_LIBS) -- \
+ $(STATIC_LINK) $(STATIC_CLIBS) -- \
$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \
- $(STATIC_EXTRA_LIBS)
+ $(STATIC_EXTRA_CLIBS)
+ strip $@
-matitac: $(CLIB_DEPS) $(CCMOS) matitac.ml
- $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) matitac.ml
-matitac.opt: $(CLIBX_DEPS) $(CCMXS) matitac.ml
- $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml
-matitac.opt.static: $(CLIBX_DEPS) $(CCMXS) matitac.ml
- $(STATIC_LINK) $(STATIC_LIBS) -- \
- $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml \
- $(STATIC_EXTRA_LIBS)
+matitac: $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) matitac.ml
+ $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml
+matitac.opt: $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
+ $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
+matitac.opt.static: $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
+ $(STATIC_LINK) $(STATIC_CLIBS) -- \
+ $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
+ $(STATIC_EXTRA_CLIBS)
+ strip $@
matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS)
$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $<
-matitadep: matitadep.ml $(DEPLIB_DEPS) $(CCMOS)
- $(OCAMLC) $(DEPPKGS) -linkpkg -o $@ $(CCMOS) $<
-matitadep.opt: matitadep.ml $(DEPLIB_DEPS) $(CCMXS)
- $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(CCMXS) $<
-matitadep.opt.static: matitadep.ml $(DEPLIB_DEPS) $(CCMXS)
- $(STATIC_LINK) $(STATIC_LIBS) -- \
- $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(CCMXS) $< \
- $(STATIC_EXTRA_LIBS)
+# matitadep: matitadep.ml $(DEPLIB_DEPS) $(DEPCMOS)
+# $(OCAMLC) $(DEPPKGS) -linkpkg -o $@ $(DEPCMOS) $<
+# matitadep.opt: matitadep.ml $(DEPLIB_DEPS) $(DEPCMXS)
+# $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(DEPCMXS) $<
+# matitadep.opt.static: matitadep.ml $(DEPLIB_DEPS) $(DEPCMXS)
+# $(STATIC_LINK) $(STATIC_CLIBS) -- \
+# $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(DEPCMXS) $< \
+# $(STATIC_EXTRA_CLIBS)
+# strip $@
+matitadep: matitac
+ @test -f $@ || ln -s $< $@
+matitadep.opt: matitac.opt
+ @test -f $@ || ln -s $< $@
+matitadep.opt.static: matitac.opt.static
+ @test -f $@ || ln -s $< $@
-matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMOS)
- $(OCAMLC) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMOS) $<
-matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS)
- $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $<
-matitaclean.opt.static: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS)
- $(STATIC_LINK) $(STATIC_LIBS) -- \
- $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< \
- $(STATIC_EXTRA_LIBS)
+# matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMOS)
+# $(OCAMLC) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMOS) $<
+# matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS)
+# $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $<
+# matitaclean.opt.static: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS)
+# $(STATIC_LINK) $(STATIC_CLIBS) -- \
+# $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< \
+# $(STATIC_EXTRA_CLIBS)
+# strip $@
+matitaclean: matitac
+ @test -f $@ || ln -s $< $@
+matitaclean.opt: matitac.opt
+ @test -f $@ || ln -s $< $@
+matitaclean.opt.static: matitac.opt.static
+ @test -f $@ || ln -s $< $@
-matitamake: matitamake.ml $(MAKECMOS)
- $(OCAMLC) $(PKGS) -linkpkg -o $@ $(MAKECMOS) $<
-matitamake.opt: matitamake.ml $(MAKECMXS)
- $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(MAKECMXS) $<
-matitamake.opt.static: matitamake.ml $(MAKECMXS)
- $(STATIC_LINK) $(STATIC_LIBS) -- \
- $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(MAKECMXS) $< \
- $(STATIC_EXTRA_LIBS)
+# matitamake: matitamake.ml $(MAKECMOS)
+# $(OCAMLC) $(MAKEPKGS) -linkpkg -o $@ $(MAKECMOS) $<
+# matitamake.opt: matitamake.ml $(MAKECMXS)
+# $(OCAMLOPT) $(MAKEPKGS) -linkpkg -o $@ $(MAKECMXS) $<
+# matitamake.opt.static: matitamake.ml $(MAKECMXS)
+# $(STATIC_LINK) $(STATIC_CLIBS) -- \
+# $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(MAKECMXS) $< \
+# $(STATIC_EXTRA_CLIBS)
+# strip $@
+matitamake: matitac
+ @test -f $@ || ln -s $< $@
+matitamake.opt: matitac.opt
+ @test -f $@ || ln -s $< $@
+matitamake.opt.static: matitac.opt.static
+ @test -f $@ || ln -s $< $@
cicbrowser: matita
@test -f $@ || ln -s $< $@
@test -f $@ || ln -s $< $@
cicbrowser.opt.static: matita.opt.static
@test -f $@ || ln -s $< $@
+cicbrowser.opt.static.upx: matita.opt.static.upx
+ @test -f $@ || ln -s $< $@
matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade
$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml
%.annot: %.ml
$(OCAMLC) -dtypes $(PKGS) -c $<
+%.upx: %
+ cp $< $@
+ strip $@
+ upx $@
+
clean:
rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
$(PROGRAMS) \
$(PROGRAMS_OPT) \
$(PROGRAMS_STATIC) \
+ $(PROGRAMS_UPX) \
$(NULL)
distclean: clean
rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
else
AC_MSG_ERROR(could not find camlp4o)
fi
-FINDLIB_DEPREQUIRES="\
+FINDLIB_COMREQUIRES="\
pcre \
mysql \
helm-registry \
helm-extlib \
helm-hmysql \
+helm-cic_notation \
+helm-tactics \
helm-cic_disambiguation \
-helm-paramodulation \
"
-FINDLIB_CLEANREQUIRES="$FINDLIB_DEPREQUIRES"
-FINDLIB_CREQUIRES="\
-$FINDLIB_CLEANREQUIRES \
-unix \
-helm-cic_omdoc \
-helm-tactics \
-helm-xml \
+FINDLIB_CLEANREQUIRES="$FINDLIB_COMREQUIRES"
+FINDLIB_DEPREQUIRES="$FINDLIB_COMREQUIRES"
+FINDLIB_MAKEREQUIRES=" \
+helm-registry \
+helm-extlib \
+"
+FINDLIB_CREQUIRES=" \
+$FINDLIB_COMREQUIRES \
+helm-paramodulation \
"
FINDLIB_REQUIRES="\
$FINDLIB_CREQUIRES \
lablgtkmathview \
lablgtksourceview \
helm-xmldiff \
+helm-cic_transformations \
helm-tactics \
+helm-cic_disambiguation \
+helm-paramodulation \
"
for r in $FINDLIB_REQUIRES
do
AC_SUBST(FINDLIB_CREQUIRES)
AC_SUBST(FINDLIB_DEPREQUIRES)
AC_SUBST(FINDLIB_CLEANREQUIRES)
+AC_SUBST(FINDLIB_MAKEREQUIRES)
AC_SUBST(HAVE_OCAMLOPT)
AC_SUBST(LABLGLADECC)
AC_SUBST(OCAMLFIND)
</child>
</widget>
-<widget class="GtkDialog" id="InterpChoiceDialog">
+<widget class="GtkDialog" id="RecordChoiceDialog">
<property name="width_request">350</property>
<property name="height_request">250</property>
- <property name="title" translatable="yes">Interpretation choice</property>
+ <property name="title" translatable="yes">title</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
<property name="window_position">GTK_WIN_POS_NONE</property>
<property name="modal">True</property>
<property name="layout_style">GTK_BUTTONBOX_END</property>
<child>
- <widget class="GtkButton" id="InterpChoiceHelpButton">
+ <widget class="GtkButton" id="RecordChoiceHelpButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
<child>
- <widget class="GtkButton" id="InterpChoiceCancelButton">
+ <widget class="GtkButton" id="RecordChoiceCancelButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
<child>
- <widget class="GtkButton" id="InterpChoiceOkButton">
+ <widget class="GtkButton" id="RecordChoiceOkButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
<property name="spacing">0</property>
<child>
- <widget class="GtkLabel" id="InterpChoiceDialogLabel">
+ <widget class="GtkLabel" id="RecordChoiceDialogLabel">
<property name="visible">True</property>
<property name="label" translatable="yes">some informative message here ...</property>
<property name="use_underline">False</property>
<property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkTreeView" id="InterpChoiceTreeView">
+ <widget class="GtkTreeView" id="RecordChoiceTreeView">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="headers_visible">False</property>
(** {2 Initialization} *)
-let _ = MatitaInit.initialize_all ()
+let _ = MatitaInit.initialize_all ()
+let _ = Paramodulation.Saturation.init () (* ALB to link paramodulation *)
(** {2 GUI callbacks} *)
(List.map (fun (g, _, _) -> string_of_int g)
(MatitaScript.current ())#proofMetasenv));
prerr_endline ("stack: " ^ Continuationals.Stack.pp
- (MatitaMisc.get_stack (MatitaScript.current ())#status)));
+ (MatitaTypes.get_stack (MatitaScript.current ())#status)));
+(* addDebugItem "ask record choice"
+ (fun _ ->
+ MatitaLog.debug (string_of_int
+ (MatitaGtkMisc.ask_record_choice ~gui ~title:"title" ~message:"msg"
+ ~fields:["a"; "b"; "c"]
+ ~records:[
+ ["0"; "0"; "0"]; ["0"; "0"; "1"]; ["0"; "1"; "0"]; ["0"; "1"; "1"];
+ ["1"; "0"; "0"]; ["1"; "0"; "1"]; ["1"; "1"; "0"]; ["1"; "1"; "1"]]
+ ()))); *)
addDebugItem "rotate light bulbs"
(fun _ ->
let nb = gui#main#hintNotebook in
let context =
match context with
| Some c -> c
- | None -> MatitaMisc.get_proof_context status goal
+ | None -> MatitaTypes.get_proof_context status goal
in
let (diff, metasenv, cic, _) =
singleton
(MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
~aliases:status.aliases ~universe:(Some status.multi_aliases)
- ~context ~metasenv:(MatitaMisc.get_proof_metasenv status) term)
+ ~context ~metasenv:(MatitaTypes.get_proof_metasenv status) term)
in
let status = MatitaTypes.set_metasenv metasenv status in
let status = MatitaSync.set_proof_aliases status diff in
let apply_tactic tactic (status, goal) =
(* prerr_endline "apply_tactic"; *)
-(* prerr_endline (Continuationals.Stack.pp (MatitaMisc.get_stack status)); *)
- let starting_metasenv = MatitaMisc.get_proof_metasenv status in
+(* prerr_endline (Continuationals.Stack.pp (MatitaTypes.get_stack status)); *)
+ let starting_metasenv = MatitaTypes.get_proof_metasenv status in
let before = List.map (fun g, _, _ -> g) starting_metasenv in
(* prerr_endline "disambiguate"; *)
let status_ref, tactic = disambiguate_tactic status goal tactic in
- let metasenv_after_refinement = MatitaMisc.get_proof_metasenv !status_ref in
- let proof = MatitaMisc.get_current_proof !status_ref in
+ let metasenv_after_refinement = MatitaTypes.get_proof_metasenv !status_ref in
+ let proof = MatitaTypes.get_current_proof !status_ref in
let proof_status = proof, goal in
let needs_reordering, always_opens_a_goal = classify_tactic tactic in
let tactic = tactic_of_ast tactic in
let apply_tactic tac = tac
let goals (_, opened, closed) = opened, closed
let set_goals (opened, closed) (status, _, _) = (status, opened, closed)
- let get_stack (status, _) = MatitaMisc.get_stack status
+ let get_stack (status, _) = MatitaTypes.get_stack status
let set_stack stack (status, opened, closed) =
- MatitaMisc.set_stack stack status, opened, closed
+ MatitaTypes.set_stack stack status, opened, closed
let inject (status, _) = (status, [], [])
let focus goal (status, _, _) = (status, goal)
match obj with
GrafiteAst.Inductive (_,(name,_,_,_)::_)
| GrafiteAst.Record (_,name,_,_) ->
- Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
+ Some (UriManager.uri_of_string (MatitaTypes.qualify status name ^ ".ind"))
| GrafiteAst.Inductive _ -> assert false
| GrafiteAst.Theorem _ -> None in
let (diff, metasenv, cic, _) =
add_moo_content [cmd] status
| GrafiteAst.Include (loc, path) ->
let absolute_path = make_absolute opts.include_paths path in
- let moopath = MatitaMisc.obj_file_of_script absolute_path in
+ let moopath = MatitacleanLib.obj_file_of_script absolute_path in
let status = ref status in
if not (Sys.file_exists moopath) then
raise (IncludedFileNotCompiled moopath);
(match types with (name,_,_,_)::_ -> name | _ -> assert false)
| _ -> assert false in
let uri =
- UriManager.uri_of_string (MatitaMisc.qualify status name ^ ext)
+ UriManager.uri_of_string (MatitaTypes.qualify status name ^ ext)
in
- let metasenv = MatitaMisc.get_proof_metasenv status in
+ let metasenv = MatitaTypes.get_proof_metasenv status in
match obj with
| Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
let name = UriManager.name_of_uri uri in
List.map (function [x] -> x | _ -> assert false) m
end
-
class taggedStringListModel ~(tags:(string * GdkPixbuf.pixbuf) list)
(tree_view: GTree.view)
=
tree_view#selection#get_selected_rows
end
+class recordModel (tree_view:GTree.view) =
+ let cols_list = new GTree.column_list in
+ let text_col = cols_list#add Gobject.Data.string in
+(* let combo_col = cols_list#add (Gobject.Data.gobject_by_name "GtkListStore") in *)
+ let combo_col = cols_list#add Gobject.Data.int in
+ let toggle_col = cols_list#add Gobject.Data.boolean in
+ let list_store = GTree.list_store cols_list in
+ let text_rend = (GTree.cell_renderer_text [], ["text", text_col]) in
+ let combo_rend = GTree.cell_renderer_combo [] in
+(* let combo_rend = (GTree.cell_renderer_combo [], [|+"model", combo_col+|]) in *)
+ let toggle_rend =
+ (GTree.cell_renderer_toggle [`ACTIVATABLE true], ["active", toggle_col])
+ in
+ let text_vcol = GTree.view_column ~renderer:text_rend () in
+ let combo_vcol = GTree.view_column ~renderer:(combo_rend, []) () in
+ let _ =
+ combo_vcol#set_cell_data_func combo_rend
+ (fun _ _ ->
+ prerr_endline "qui";
+ let model, col =
+ GTree.store_of_list Gobject.Data.string ["a"; "b"; "c"]
+ in
+ combo_rend#set_properties [
+ `MODEL (Some (model :> GTree.model));
+ `TEXT_COLUMN col
+ ])
+ in
+ let toggle_vcol = GTree.view_column ~renderer:toggle_rend () in
+ object (self)
+ initializer
+ tree_view#set_model (Some (list_store :> GTree.model));
+ ignore (tree_view#append_column text_vcol);
+ ignore (tree_view#append_column combo_vcol);
+ ignore (tree_view#append_column toggle_vcol)
+
+ method list_store = list_store
+
+ method easy_append s (combo:int) (toggle:bool) =
+ let tree_iter = list_store#append () in
+ list_store#set ~row:tree_iter ~column:text_col s;
+ list_store#set ~row:tree_iter ~column:combo_col combo;
+ list_store#set ~row:tree_iter ~column:toggle_col toggle
+ end
+
class type gui =
object
method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
- method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
+ method newRecordDialog: unit -> MatitaGeneratedGui.recordChoiceDialog
method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
end
| PopupClosed -> ()
-let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false)
+let ask_text ~(gui:#gui) ?(title = "") ?(message = "") ?(multiline = false)
?default ()
=
let dialog = gui#newEmptyDialog () in
dialog#emptyDialog#set_title title;
- dialog#emptyDialogLabel#set_label msg;
+ dialog#emptyDialogLabel#set_label message;
let result = ref None in
let return r =
result := r;
GtkThread.main ();
(match !result with None -> raise Cancel | Some r -> r)
+type combo_status = Free of string | Locked of string
+
+let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "")
+ ~fields ~records ()
+=
+ let fields = Array.of_list fields in
+ let fields_no = Array.length fields in
+ assert (fields_no > 0);
+ let dialog = gui#newRecordDialog () in
+ dialog#recordChoiceDialog#set_title title;
+ dialog#recordChoiceDialogLabel#set_label message;
+ let model = new recordModel dialog#recordChoiceTreeView in
+ dialog#recordChoiceTreeView#set_headers_visible true;
+ let combos =
+ Array.init fields_no
+ (fun _ -> GTree.store_of_list Gobject.Data.string ["a"; "b"; "c"])
+ in
+ let (store, col) = combos.(0) in
+ store#set ~row:(store#append ()) ~column:col "uno";
+ store#set ~row:(store#append ()) ~column:col "due";
+ let toggles = Array.init fields_no (fun _ -> false) in
+ Array.iteri
+ (fun i f -> model#easy_append f i toggles.(i))
+ fields;
+ let status = Array.map (fun s -> Free s) fields in
+ let record_no = ref None in
+ let return _ =
+ dialog#recordChoiceDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ let fail _ = record_no := None; return () in
+ ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#recordChoiceOkButton (fun _ ->
+ match !record_no with None -> () | Some _ -> return ());
+ connect_button dialog#recordChoiceCancelButton fail;
+(* ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ ->
+ interp_no := Some (model#get_interp_no path);
+ return ()));
+ let selection = dialog#recordChoiceTreeView#selection in
+ ignore (selection#connect#changed (fun _ ->
+ match selection#get_selected_rows with
+ | [path] -> interp_no := Some (model#get_interp_no path)
+ | _ -> assert false)); *)
+ dialog#recordChoiceDialog#show ();
+ GtkThread.main ();
+ (match !record_no with Some n -> n | _ -> raise MatitaTypes.Cancel)
+
class type gui =
object (* minimal gui object requirements *)
method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
- method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
+ method newRecordDialog: unit -> MatitaGeneratedGui.recordChoiceDialog
method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
end
- (** {3 Dialogs} *)
+ (** {3 Dialogs}
+ * In functions below:
+ * @param title window title
+ * @param message content of the text label shown to the user *)
- (* @param parent to center the window on it *)
+ (** @param parent to center the window on it *)
val ask_confirmation:
- title:string ->
- message:string ->
+ title:string -> message:string ->
?parent:#GWindow.window_skel ->
- unit -> [`YES | `NO | `CANCEL]
-
-val report_error:
- title:string ->
- message:string ->
- ?parent:#GWindow.window_skel ->
- unit -> unit
+ unit ->
+ [`YES | `NO | `CANCEL]
(** @param multiline (default: false) if true a TextView widget will be used
* for prompting the user otherwise a TextEntry widget will be
* @return the string given by the user *)
val ask_text:
gui:#gui ->
- ?title:string -> ?msg:string -> ?multiline:bool -> ?default:string -> unit ->
+ ?title:string -> ?message:string ->
+ ?multiline:bool -> ?default:string -> unit ->
string
+ (** @param fields field names
+ * @param records list of records, each record is a list of [fields] strings
+ * @return number of the chosen record, 0 for the first one *)
+val ask_record_choice:
+ gui:#gui ->
+ ?title:string -> ?message:string ->
+ fields:string list -> records:string list list ->
+ unit ->
+ int
+
+val report_error:
+ title:string -> message:string ->
+ ?parent:#GWindow.window_skel ->
+ unit ->
+ unit
+
let ask_and_save_moo_if_needed parent fname status =
let save () =
- let moo_fname = MatitaMisc.obj_file_of_script fname in
+ let moo_fname = MatitacleanLib.obj_file_of_script fname in
MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
if (MatitaScript.current ())#eos &&
status.MatitaTypes.proof_status = MatitaTypes.No_proof
then
begin
let mooname =
- MatitaMisc.obj_file_of_script fname
+ MatitacleanLib.obj_file_of_script fname
in
let rc =
MatitaGtkMisc.ask_confirmation
dialog#check_widgets ();
dialog
- method newInterpDialog () =
- let dialog = new interpChoiceDialog () in
+ method newRecordDialog () =
+ let dialog = new recordChoiceDialog () in
dialog#check_widgets ();
dialog
let interactive_interp_choice () choices =
let gui = instance () in
assert (choices <> []);
- let dialog = gui#newInterpDialog () in
- let model = new interpModel dialog#interpChoiceTreeView choices in
+ let dialog = gui#newRecordDialog () in
+ let model = new interpModel dialog#recordChoiceTreeView choices in
let interp_len = List.length (List.hd choices) in
- dialog#interpChoiceDialog#set_title "Interpretation choice";
- dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
+ dialog#recordChoiceDialog#set_title "Interpretation choice";
+ dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:";
let interp_no = ref None in
let return _ =
- dialog#interpChoiceDialog#destroy ();
+ dialog#recordChoiceDialog#destroy ();
GMain.Main.quit ()
in
let fail _ = interp_no := None; return () in
- ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
- connect_button dialog#interpChoiceOkButton (fun _ ->
+ ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#recordChoiceOkButton (fun _ ->
match !interp_no with None -> () | Some _ -> return ());
- connect_button dialog#interpChoiceCancelButton fail;
- ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
+ connect_button dialog#recordChoiceCancelButton fail;
+ ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ ->
interp_no := Some (model#get_interp_no path);
return ()));
- let selection = dialog#interpChoiceTreeView#selection in
+ let selection = dialog#recordChoiceTreeView#selection in
ignore (selection#connect#changed (fun _ ->
match selection#get_selected_rows with
| [path] -> interp_no := Some (model#get_interp_no path)
| _ -> assert false));
- dialog#interpChoiceDialog#show ();
+ dialog#recordChoiceDialog#show ();
GtkThread.main ();
(match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
method newBrowserWin: unit -> browserWin
method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
- method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
+ method newRecordDialog: unit -> MatitaGeneratedGui.recordChoiceDialog
method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
open Printf
type thingsToInitilaize =
- ConfigurationFile | Db | Environment | Getter | Notation |
- Paramodulation | Makelib | CmdLine
+ ConfigurationFile | Db | Environment | Getter | Notation | Makelib | CmdLine
exception FailedToInitialize of thingsToInitilaize
else
init_status
-let initialize_paramodulation init_status =
- wants [] init_status;
- if not (already_configured [Paramodulation] init_status) then
- begin
- Paramodulation.Saturation.init ();
- Paramodulation::init_status
- end
- else
- init_status
-
let initialize_makelib init_status =
wants [ConfigurationFile] init_status;
if not (already_configured [Makelib] init_status) then
let initialize_all () =
status :=
- initialize_notation
+ List.fold_left (fun s f -> f s) !status
+ [ parse_cmdline; load_configuration; initialize_makelib;
+ initialize_db; initialize_environment; initialize_notation ]
+(* initialize_notation
(initialize_environment
(initialize_db
- (initialize_paramodulation
- (initialize_makelib
- (load_configuration
- (parse_cmdline !status))))))
+ (initialize_makelib
+ (load_configuration
+ (parse_cmdline !status))))) *)
let load_configuration_file () =
status := load_configuration !status
let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
(distance < 4.)
+let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink"
+let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm"
let href_ds = Gdome.domString "href"
let xref_ds = Gdome.domString "xref"
+let domImpl = Gdome.domImplementation ()
+
+ (** Gdome.element of a MathML document whose rendering should be blank. Used
+ * by cicBrowser to render "about:blank" document *)
+let empty_mathml = lazy (
+ domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
+ ~qualifiedName:(Gdome.domString "math") ~doctype:None)
+
+let empty_boxml = lazy (
+ domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns)
+ ~qualifiedName:(Gdome.domString "box") ~doctype:None)
+
+ (** shown for goals closed by side effects *)
+let closed_goal_mathml = lazy (
+ domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ())
+
(* ids_to_terms should not be passed here, is just for debugging *)
let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types =
let find_parent id ids =
(match self#get_element_at x y with
| None -> ()
| Some elt ->
- let namespaceURI = DomMisc.xlink_ns in
let localName = href_ds in
- if elt#hasAttributeNS ~namespaceURI ~localName then
+ if elt#hasAttributeNS ~namespaceURI:xlink_ns ~localName then
self#invoke_href_callback
- (elt#getAttributeNS ~namespaceURI ~localName)#to_string
+ (elt#getAttributeNS ~namespaceURI:xlink_ns
+ ~localName)#to_string
gdk_button
else
ignore (self#action_toggle elt));
ignore (self#coerce#misc#grab_selection Gdk.Atom.primary)
in
let rec aux elt =
- if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
+ if (elt#getAttributeNS ~namespaceURI:helm_ns
~localName:xref_ds)#to_string <> ""
then
set_selection elt
with GdomeInit.DOMCastException _ -> ()
in
(match gdome_elt with
- | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns
+ | Some elt when (elt#getAttributeNS ~namespaceURI:xlink_ns
~localName:href_ds)#to_string <> "" ->
set_selection elt
| Some elt -> aux elt
(try Hashtbl.find ids_to_terms id with Not_found -> assert false)
method private string_of_node node =
- if node#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
+ if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds
then self#string_of_id_node node
else string_of_dom_node node
method private string_of_id_node node =
let get_id (node: Gdome.element) =
let xref_attr =
- node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
+ node#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds
in
List.hd (HExtlib.split ~sep:' ' xref_attr#to_string)
in
Hashtbl.create 1, None));
let name = "sequent_viewer.xml" in
MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name);
- ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
+ ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
self#load_root ~root:mathml#get_documentElement
method load_object obj =
| _ ->
let name = "cic_browser.xml" in
MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name);
- ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
+ ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
self#load_root ~root:mathml#get_documentElement;
current_mathml <- Some mathml);
end
let markup =
match depth, pos with
| 0, _ -> `Current (render_switch sw)
- | 1, pos when Stack.head_tag stack = Stack.BranchTag ->
+ | 1, pos when Stack.head_tag stack = `BranchTag ->
`Shift (pos, render_switch sw)
| _ -> render_switch sw
in
(match goal_switch with
| Stack.Open goal -> cicMathView#load_sequent _metasenv goal
| Stack.Closed goal ->
- let doc = Lazy.force MatitaMisc.closed_goal_mathml in
+ let doc = Lazy.force closed_goal_mathml in
cicMathView#load_root ~root:doc#get_documentElement);
(try
cicMathView#set_selection None;
method private blank () =
self#_showMath;
- mathView#load_root
- (Lazy.force MatitaMisc.empty_mathml)#get_documentElement
+ mathView#load_root (Lazy.force empty_mathml)#get_documentElement
method private _loadCheck term =
failwith "not implemented _loadCheck";
Some buri
| _ -> None
-let baseuri_of_file file =
- let uri = ref None in
- let ic = open_in file in
- let istream = Ulexing.from_utf8_channel ic in
- (try
- while true do
- try
- let stm = GrafiteParser.parse_statement istream in
- match baseuri_of_baseuri_decl stm with
- | Some buri ->
- let u = strip_trailing_slash buri in
- if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
- MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
- (try
- ignore(Http_getter.resolve u)
- with
- | Http_getter_types.Unresolvable_URI _ ->
- MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
- | Http_getter_types.Key_not_found _ -> ());
- uri := Some u;
- raise End_of_file
- | None -> ()
- with
- CicNotationParser.Parse_error _ as exn ->
- prerr_endline ("Unable to parse: " ^ file);
- prerr_endline (MatitaExcPp.to_string exn);
- ()
- done
- with End_of_file -> close_in ic);
- match !uri with
- | Some uri -> uri
- | None -> failwith ("No baseuri defined in " ^ file)
-
let is_empty buri =
List.for_all
(function
else
s
-let empty_mathml = lazy (
- DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
- ~qualifiedName:(Gdome.domString "math") ~doctype:None)
-
-let empty_boxml = lazy (
- DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns)
- ~qualifiedName:(Gdome.domString "box") ~doctype:None)
-
-let closed_goal_mathml = lazy (
- DomMisc.domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ())
-
exception History_failure
type 'a memento = 'a array * int * int * int (* data, hd, tl, cur *)
let instance = lazy (f ()) in
fun () -> Lazy.force instance
-let get_current_proof status =
- match status.proof_status with
- | Incomplete_proof { proof = p } -> p
- | _ -> statement_error "no ongoing proof"
-
-let get_proof_metasenv status =
- match status.proof_status with
- | No_proof -> []
- | Proof (_, metasenv, _, _)
- | Incomplete_proof { proof = (_, metasenv, _, _) }
- | Intermediate metasenv ->
- metasenv
-
-let get_proof_context status goal =
- match status.proof_status with
- | Incomplete_proof { proof = (_, metasenv, _, _) } ->
- let (_, context, _) = CicUtil.lookup_meta goal metasenv in
- context
- | _ -> []
-
-let get_proof_conclusion status goal =
- match status.proof_status with
- | Incomplete_proof { proof = (_, metasenv, _, _) } ->
- let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
- conclusion
- | _ -> statement_error "no ongoing proof"
-
-let get_stack status =
- match status.proof_status with
- | Incomplete_proof p -> p.stack
- | Proof _ -> Continuationals.Stack.empty
- | _ -> assert false
-
-let set_stack stack status =
- match status.proof_status with
- | Incomplete_proof p ->
- { status with proof_status = Incomplete_proof { p with stack = stack } }
- | Proof _ ->
- assert (Continuationals.Stack.is_empty stack);
- status
- | _ -> assert false
-
-let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
-
let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
let end_ma_RE = Pcre.regexp "\\.ma$"
in
path ^ ".moo"
-let obj_file_of_script f =
- if f = "coq.ma" then BuildTimeConf.coq_notation_script else
- let baseuri = baseuri_of_file f in
- obj_file_of_baseuri baseuri
-
let list_tl_at ?(equality=(==)) e l =
let rec aux =
function
* http://helm.cs.unibo.it/
*)
-val baseuri_of_file : string -> string
-
val baseuri_of_baseuri_decl:
('a, 'b, 'c, 'd, 'e) GrafiteAst.statement -> string option
* @raise Not_found *)
val list_tl_at: ?equality:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
- (** Gdome.element of a MathML document whose rendering should be blank. Used
- * by cicBrowser to render "about:blank" document *)
-val empty_mathml: Gdome.document lazy_t
-val empty_boxml: Gdome.document lazy_t
-
- (** shown for goals closed by side effects *)
-val closed_goal_mathml: Gdome.document lazy_t
-
exception History_failure
type 'a memento
* first time it gets called. Next invocation will return first value *)
val singleton: (unit -> 'a) -> (unit -> 'a)
-val qualify: MatitaTypes.status -> string -> string
-
-val get_current_proof: MatitaTypes.status -> ProofEngineTypes.proof
-val get_stack: MatitaTypes.status -> Continuationals.Stack.t
-val set_stack: Continuationals.Stack.t ->MatitaTypes.status ->MatitaTypes.status
-val get_proof_metasenv: MatitaTypes.status -> Cic.metasenv
-
-val get_proof_context:
- MatitaTypes.status -> ProofEngineTypes.goal -> Cic.context
-
-val get_proof_conclusion:
- MatitaTypes.status -> ProofEngineTypes.goal -> Cic.term
-
(** given the base name of an image, returns its full path *)
val image_path: string -> string
val obj_file_of_baseuri: string -> string
-val obj_file_of_script: string -> string
let disambiguate_macro_term term status user_goal =
let module MD = MatitaDisambiguator in
let dbd = MatitaDb.instance () in
- let metasenv = MatitaMisc.get_proof_metasenv status in
- let context = MatitaMisc.get_proof_context status user_goal in
+ let metasenv = MatitaTypes.get_proof_metasenv status in
+ let context = MatitaTypes.get_proof_context status user_goal in
let interps =
MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases
~universe:(Some status.multi_aliases) term in
[], parsed_text_length
(* REAL macro *)
| TA.Hint loc ->
- let proof = MatitaMisc.get_current_proof status in
+ let proof = MatitaTypes.get_current_proof status in
let proof_status = proof, user_goal in
let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
let selected = guistuff.urichooser l in
) selected;
assert false)
| TA.Check (_,term) ->
- let metasenv = MatitaMisc.get_proof_metasenv status in
- let context = MatitaMisc.get_proof_context status user_goal in
+ let metasenv = MatitaTypes.get_proof_metasenv status in
+ let context = MatitaTypes.get_proof_context status user_goal in
let interps =
MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
~aliases:status.aliases ~universe:(Some status.multi_aliases) term
| Incomplete_proof _ -> true
| Intermediate _ -> assert false
-(* method proofStatus = MatitaMisc.get_proof_status self#status *)
- method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
- method proofContext = MatitaMisc.get_proof_context self#status userGoal
- method proofConclusion = MatitaMisc.get_proof_conclusion self#status userGoal
- method stack = MatitaMisc.get_stack self#status
+(* method proofStatus = MatitaTypes.get_proof_status self#status *)
+ method proofMetasenv = MatitaTypes.get_proof_metasenv self#status
+ method proofContext = MatitaTypes.get_proof_context self#status userGoal
+ method proofConclusion = MatitaTypes.get_proof_conclusion self#status userGoal
+ method stack = MatitaTypes.get_stack self#status
method setGoal n = userGoal <- n
method goal = userGoal
let dump_status status =
MatitaLog.message "status.aliases:\n";
- MatitaLog.message
- (DisambiguatePp.pp_environment status.aliases ^ "\n");
MatitaLog.message "status.proof_status:";
MatitaLog.message
(match status.proof_status with
?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
end
+let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
+
+let get_current_proof status =
+ match status.proof_status with
+ | Incomplete_proof { proof = p } -> p
+ | _ -> statement_error "no ongoing proof"
+
+let get_proof_metasenv status =
+ match status.proof_status with
+ | No_proof -> []
+ | Proof (_, metasenv, _, _)
+ | Incomplete_proof { proof = (_, metasenv, _, _) }
+ | Intermediate metasenv ->
+ metasenv
+
+let get_proof_context status goal =
+ match status.proof_status with
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+ let (_, context, _) = CicUtil.lookup_meta goal metasenv in
+ context
+ | _ -> []
+
+let get_proof_conclusion status goal =
+ match status.proof_status with
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+ let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
+ conclusion
+ | _ -> statement_error "no ongoing proof"
+
+let get_stack status =
+ match status.proof_status with
+ | Incomplete_proof p -> p.stack
+ | Proof _ -> Continuationals.Stack.empty
+ | _ -> assert false
+
+let set_stack stack status =
+ match status.proof_status with
+ | Incomplete_proof p ->
+ { status with proof_status = Incomplete_proof { p with stack = stack } }
+ | Proof _ ->
+ assert (Continuationals.Stack.is_empty stack);
+ status
+ | _ -> assert false
+
method show_uri_list :
?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
end
+
+val qualify: status -> string -> string
+
+val get_current_proof: status -> ProofEngineTypes.proof
+val get_proof_metasenv: status -> Cic.metasenv
+val get_proof_context: status -> ProofEngineTypes.goal -> Cic.context
+val get_proof_conclusion: status -> ProofEngineTypes.goal -> Cic.term
+val get_stack: status -> Continuationals.Stack.t
+
+val set_stack: Continuationals.Stack.t -> status -> status
+
* http://helm.cs.unibo.it/
*)
+let main () =
+ match Filename.basename Sys.argv.(0) with
+ | "matitadep" -> Matitadep.main ()
+ | "matitaclean" -> Matitaclean.main ()
+ | "matitamake" -> Matitamake.main ()
+ | _ ->
+ let _ = Paramodulation.Saturation.init () in (* ALB to link paramodulation *)
+ let _ = MatitacLib.main `COMPILER in
+ ()
-(* ALB to link paramodulation... *)
-let _ = Paramodulation.Saturation.init ()
-
-
-let _ = MatitacLib.main `COMPILER
+let _ = main ()
end
else
begin
- let moo_fname = MatitaMisc.obj_file_of_script fname in
+ let moo_fname = MatitacleanLib.obj_file_of_script fname in
MatitaMoo.save_moo moo_fname moo_content_rev;
MatitaLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
module UM = UriManager
module TA = GrafiteAst
-let _ = MatitaInit.initialize_all ()
-
-let main = MatitacleanLib.clean_baseuris
-
-let _ =
+let main () =
+ let _ = MatitaInit.initialize_all () in
let uris_to_remove = ref [] in
let files_to_remove = ref [] in
(match Helm_registry.get_list Helm_registry.string "matita.args" with
UM.buri_of_uri (UM.uri_of_string suri)
with UM.IllFormedUri _ ->
files_to_remove := suri :: !files_to_remove;
- let u = MatitaMisc.baseuri_of_file suri in
+ let u = MatitacleanLib.baseuri_of_file suri in
if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin
MatitaLog.error (sprintf "File %s defines a bad baseuri: %s"
suri u);
in
uris_to_remove := uri :: !uris_to_remove)
files);
- main !uris_to_remove;
- let moos = List.map MatitaMisc.obj_file_of_script !files_to_remove in
+ MatitacleanLib.clean_baseuris !uris_to_remove;
+ let moos = List.map MatitacleanLib.obj_file_of_script !files_to_remove in
List.iter MatitaMisc.safe_remove moos
MetadataTypes.count_tbl()]
end
+let baseuri_of_file file =
+ let uri = ref None in
+ let ic = open_in file in
+ let istream = Ulexing.from_utf8_channel ic in
+ (try
+ while true do
+ try
+ let stm = GrafiteParser.parse_statement istream in
+ match MatitaMisc.baseuri_of_baseuri_decl stm with
+ | Some buri ->
+ let u = MatitaMisc.strip_trailing_slash buri in
+ if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
+ MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
+ (try
+ ignore(Http_getter.resolve u)
+ with
+ | Http_getter_types.Unresolvable_URI _ ->
+ MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
+ | Http_getter_types.Key_not_found _ -> ());
+ uri := Some u;
+ raise End_of_file
+ | None -> ()
+ with
+ CicNotationParser.Parse_error _ as exn ->
+ prerr_endline ("Unable to parse: " ^ file);
+ prerr_endline (MatitaExcPp.to_string exn);
+ ()
+ done
+ with End_of_file -> close_in ic);
+ match !uri with
+ | Some uri -> uri
+ | None -> failwith ("No baseuri defined in " ^ file)
+
+let obj_file_of_script f =
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+ let baseuri = baseuri_of_file f in
+ MatitaMisc.obj_file_of_baseuri baseuri
+
val clean_baseuris : ?verbose:bool -> string list -> unit
+val baseuri_of_file: string -> string
+val obj_file_of_script : string -> string
+
module GA = GrafiteAst
module U = UriManager
-(* all are maps from "file" to "something" *)
-let include_deps = Hashtbl.create (Array.length Sys.argv)
-let baseuri_of = Hashtbl.create (Array.length Sys.argv)
-let uri_deps = Hashtbl.create (Array.length Sys.argv)
-
-let buri alias =
- U.buri_of_uri (U.uri_of_string alias)
-
-let resolve alias current_buri=
- let buri = buri alias in
- if buri <> current_buri then Some buri else None
-
-let find path =
- let rec aux = function
- | [] -> close_in (open_in path); path
- | p :: tl ->
- try
- close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path
- with Sys_error _ -> aux tl
- in
- let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in
- try
- aux paths
- with Sys_error _ as exc ->
- MatitaLog.error ("Unable to read " ^ path);
- MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
- raise exc
-;;
-
let main () =
+ (* all are maps from "file" to "something" *)
+ let include_deps = Hashtbl.create (Array.length Sys.argv) in
+ let baseuri_of = Hashtbl.create (Array.length Sys.argv) in
+ let uri_deps = Hashtbl.create (Array.length Sys.argv) in
+ let buri alias = U.buri_of_uri (U.uri_of_string alias) in
+ let resolve alias current_buri =
+ let buri = buri alias in
+ if buri <> current_buri then Some buri else None
+ in
+ let find path =
+ let rec aux = function
+ | [] -> close_in (open_in path); path
+ | p :: tl ->
+ try
+ close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path
+ with Sys_error _ -> aux tl
+ in
+ let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in
+ try
+ aux paths
+ with Sys_error _ as exc ->
+ MatitaLog.error ("Unable to read " ^ path);
+ MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
+ raise exc
+ in
MatitaInit.load_configuration_file ();
MatitaInit.parse_cmdline ();
List.iter
| GrafiteAst.IncludeDep path ->
try
let ma_file = if path <> "coq.ma" then find path else path in
- let moo_file = MatitaMisc.obj_file_of_script ma_file in
+ let moo_file = MatitacleanLib.obj_file_of_script ma_file in
Hashtbl.add include_deps file moo_file
with Sys_error _ ->
MatitaLog.warn
let deps = List.fast_sort Pervasives.compare deps in
let deps = HExtlib.list_uniq deps in
let deps = file :: deps in
- let moo = MatitaMisc.obj_file_of_script file in
+ let moo = MatitacleanLib.obj_file_of_script file in
Printf.printf "%s: %s\n" moo (String.concat " " deps);
Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo)
(Helm_registry.get_list Helm_registry.string "matita.args")
-;;
-
-let _ =
- main ()
+
module MK = MatitamakeLib ;;
-let _ =
- MatitaInit.load_configuration_file ();
- MK.initialize ()
-;;
-
-let usage = ref (fun () -> ())
-
-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
-;;
-
-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
-;;
-
-let init_dev_doc = "
+let main () =
+ Helm_registry.load_from BuildTimeConf.matita_conf;
+ 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_doc = "
\tParameters: name (the name of the development, required)
\tDescription: tells matitamake that a new development radicated
\t\tin the current working directory should be handled."
-;;
-
-let init_dev args =
- if List.length args <> 1 then !usage ();
- match MK.initialize_development (List.hd args) (Unix.getcwd ()) with
- | None -> exit 2
- | Some _ -> exit 0
-;;
-
-let list_dev_doc = "
+ in
+ let init_dev args =
+ if List.length args <> 1 then !usage ();
+ match MK.initialize_development (List.hd args) (Unix.getcwd ()) with
+ | None -> exit 2
+ | Some _ -> exit 0
+ in
+ let list_dev_doc = "
\tParameters:
\tDescription: lists the known developments and their roots."
-;;
-
-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
-;;
-
-let destroy_dev_doc = "
+ 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_doc = "
\tParameters: name (the name of the development to destroy, required)
\tDescription: deletes a development (only from matitamake metadat, no
\t\t.ma files will be deleted)."
-
-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
-;;
-
-let clean_dev_doc = "
+ 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_doc = "
\tParameters: name (the name of the development to destroy, optional)
\t\tIf omitted the development that holds the current working
\t\tdirectory is used (if any).
\tDescription: clean the develpoment."
-
-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
-;;
-
-let build_dev_doc = "
+ 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_doc = "
\tParameters: name (the name of the development to build, required)
\tDescription: completely builds the develpoment."
-
-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
-;;
-
-let nodb_doc = "
+ 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 nodb_doc = "
\tParameters:
\tDescription: avoid using external database connection."
-
-let nodb _ = Helm_registry.set_bool "db.nodb" true
-
-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
-;;
-
-let params = [
- "-init", init_dev, init_dev_doc;
- "-clean", clean_dev, clean_dev_doc;
- "-list", list_dev, list_dev_doc;
- "-destroy", destroy_dev, destroy_dev_doc;
- "-build", build_dev, build_dev_doc;
- "-nodb", nodb, nodb_doc;
- "-h", (fun _ -> !usage()), "print this help screen";
- "-help", (fun _ -> !usage()), "print this help screen";
-]
-;;
-
-usage := fun () ->
- let p = prerr_endline in
- p "\nusage:";
- p "\tmatitamake(.opt) [command [options]]\n";
- p "\tmatitamake(.opt) [target]\n";
- p "commands:";
- List.iter (fun (n,_,d) -> p (Printf.sprintf " %-10s%s" n d)) params;
- p "\nIf target is omitted a 'all' will be used as the default.";
- p "With -build you can build a development wherever it is.";
- p "If you specify a target it implicitly refers to the development that";
- p "holds the current working directory (if any).\n";
- exit 1
-;;
-
-let rec parse args =
- match args with
- | [] -> target ["all"]
- | s::tl ->
- try
- let _,f,_ = List.find (fun (n,_,_) -> n = s) params in
- f tl;
- parse tl
- with Not_found -> if s.[0] = '-' then !usage () else target args
-
-let _ =
+ in
+ let nodb _ = Helm_registry.set_bool "db.nodb" true 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, init_dev_doc;
+ "-clean", clean_dev, clean_dev_doc;
+ "-list", list_dev, list_dev_doc;
+ "-destroy", destroy_dev, destroy_dev_doc;
+ "-build", build_dev, build_dev_doc;
+ "-nodb", nodb, nodb_doc;
+ "-h", (fun _ -> !usage()), "print this help screen";
+ "-help", (fun _ -> !usage()), "print this help screen";
+ ]
+ in
+ usage := (fun () ->
+ let p = prerr_endline in
+ p "\nusage:";
+ p "\tmatitamake(.opt) [command [options]]\n";
+ p "\tmatitamake(.opt) [target]\n";
+ p "commands:";
+ List.iter (fun (n,_,d) -> p (Printf.sprintf " %-10s%s" n d)) params;
+ p "\nIf target is omitted a 'all' will be used as the default.";
+ p "With -build you can build a development wherever it is.";
+ p "If you specify a target it implicitly refers to the development that";
+ p "holds the current working directory (if any).\n";
+ exit 1);
+ let rec parse args =
+ match args with
+ | [] -> target ["all"]
+ | s::tl ->
+ try
+ let _,f,_ = List.find (fun (n,_,_) -> n = s) params in
+ f tl;
+ parse tl
+ with Not_found -> if s.[0] = '-' then !usage () else target args
+ in
parse (List.tl (Array.to_list Sys.argv))
-
+
projects / helm.git / commitdiff