From: Stefano Zacchiroli Date: Wed, 3 Nov 2004 16:39:22 +0000 (+0000) Subject: snapshot (notably: ported to mysql instead of dbi) X-Git-Tag: v_0_6_4_1~30 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=afd3b379d4959e4a18c1f26f25e4a9c14997866f;p=helm.git snapshot (notably: ported to mysql instead of dbi) --- diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 7b3805751..e7f4f677b 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -25,21 +25,24 @@ CMOS = \ matitaDisambiguator.cmo \ matitaMathView.cmo \ matitaInterpreter.cmo -CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) + +LIB_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES)) all: matita ifeq ($(HAVE_OCAMLOPT),yes) +CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) +LIBX_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES)) opt: matita.opt else opt: @echo "Native code compilation is disabled" endif -matita: $(CMOS) matita.ml - $(OCAMLC) -linkpkg -o $@ $^ -matita.opt: $(CMXS) matita.ml - $(OCAMLOPT) -linkpkg -o $@ $^ +matita: $(LIB_DEPS) $(CMOS) matita.ml + $(OCAMLC) -linkpkg -o $@ $(CMOS) matita.ml +matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml + $(OCAMLOPT) -linkpkg -o $@ $(CMXS) matita.ml matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade $(LABLGLADECC) $< > matitaGeneratedGui.ml diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index bb3391317..249058f8b 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -29,5 +29,4 @@ let undo_history_size = 10;; let console_history_size = 100;; let gtkrc = "@MATITA_GTKRC@";; let base_uri = "cic:/matita";; -module DB = @DBI_MODULE@;; diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 2cf2e52b8..d04ac1867 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -27,13 +27,11 @@ else AC_MSG_ERROR(could not find camlp4o) fi -DBI_DRIVER="mysql" - FINDLIB_REQUIRES="\ lablgtk2.glade \ lablgtkmathview \ pcre \ -dbi.$DBI_DRIVER \ +mysql \ unix \ helm-cic_omdoc \ helm-cic_transformations \ @@ -87,7 +85,6 @@ if test "$DEBUG" = "true"; then fi MATITA_GTKRC="matita.gtkrc" -DBI_MODULE="Dbi_$DBI_DRIVER" AC_SUBST(CAMLP4O) AC_SUBST(DEBUG) @@ -97,7 +94,6 @@ AC_SUBST(HAVE_OCAMLOPT) AC_SUBST(LABLGLADECC) AC_SUBST(OCAMLFIND) AC_SUBST(MATITA_GTKRC) -AC_SUBST(DBI_MODULE) AC_OUTPUT([ buildTimeConf.ml diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index 389a14e8d..1ca17a9ed 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -5,14 +5,14 @@ true
- - localhost + mowgli.cs.unibo.it + helm mowgli
remote - - http://localhost:58081/ + http://mowgli.cs.unibo.it:58081/ +
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index e7dc8ded4..7c272a828 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -1281,7 +1281,7 @@ Copyright (C) 2004, GTK_WINDOW_TOPLEVEL GTK_WIN_POS_NONE False - 300 + 450 800 True False diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index b946ec69b..2619b9bb9 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -29,8 +29,6 @@ open MatitaGtkMisc open MatitaTypes open MatitaMisc -module DB = BuildTimeConf.DB - (** {2 Internal status} *) let (get_proof, set_proof, has_proof) = @@ -51,12 +49,15 @@ let _ = GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; GMain.Main.init () let parserr = new MatitaDisambiguator.parserr () -let dbh = - new DB.connection ~host:(Helm_registry.get "db.host") - ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database") +let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () let gui = MatitaGui.instance () let disambiguator = - new MatitaDisambiguator.disambiguator ~parserr ~dbh + new MatitaDisambiguator.disambiguator ~parserr ~dbd ~chooseUris:(interactive_user_uri_choice ~gui) ~chooseInterp:(interactive_interp_choice ~gui) () @@ -148,10 +149,13 @@ let _ = match gui#chooseFile () with | None -> () | Some f when is_proof_script f -> - gui#script#scriptTextView#buffer#set_text (input_file f) + gui#script#scriptTextView#buffer#set_text (input_file f); + gui#script#scriptWin#show (); + gui#main#showScriptMenuItem#set_active true | Some f -> gui#console#echo_error (sprintf - "Don't know what to do with file: %s\nUnrecognized file format." f))) + "Don't know what to do with file: %s\nUnrecognized file format." + f))) (** *) diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index 23de092bd..01e85e0c4 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -30,7 +30,7 @@ class parserr () = end class disambiguator - ~parserr ~dbh ~(chooseUris: MatitaTypes.choose_uris_callback) + ~parserr ~dbd ~(chooseUris: MatitaTypes.choose_uris_callback) ~(chooseInterp: MatitaTypes.choose_interp_callback) () = let disambiguate_term = @@ -70,7 +70,7 @@ class disambiguator | Some env -> (false, env) | None -> (true, _env) in - match disambiguate_term ~dbh context metasenv termAst ~aliases:env with + match disambiguate_term ~dbd context metasenv termAst ~aliases:env with | [ (env, metasenv, term) as x ] -> if save_state then self#setEnv env; x diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli index 9b432f845..5b7bbc880 100644 --- a/helm/matita/matitaDisambiguator.mli +++ b/helm/matita/matitaDisambiguator.mli @@ -27,7 +27,7 @@ class parserr: unit -> MatitaTypes.parserr class disambiguator: parserr:MatitaTypes.parserr -> (** parser *) - dbh:Dbi.connection -> + dbd:Mysql.dbd -> chooseUris:MatitaTypes.choose_uris_callback -> chooseInterp:MatitaTypes.choose_interp_callback -> unit -> diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index 9c8ae97f3..8c45d4d59 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -31,7 +31,7 @@ val toggle_visibility: win:GWindow.window -> check:GMenu.check_menu_item -> unit val toggle_win: - ?check:GMenu.check_menu_item -> GWindow.window -> (unit -> unit) + ?check:GMenu.check_menu_item -> GWindow.window -> unit -> unit val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit