From: Stefano Zacchiroli <zack@upsilon.cc>
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 @@
     <key name="auto_disambiguation">true</key>
   </section>
   <section name="db">
-<!--     <key name="host">mowgli.cs.unibo.it</key> -->
-    <key name="host">localhost</key>
+    <key name="host">mowgli.cs.unibo.it</key>
+<!--     <key name="host">localhost</key> -->
     <key name="user">helm</key>
     <key name="database">mowgli</key>
   </section>
   <section name="getter">
     <key name="mode">remote</key>
-<!--     <key name="url">http://mowgli.cs.unibo.it:58081/</key> -->
-    <key name="url">http://localhost:58081/</key>
+    <key name="url">http://mowgli.cs.unibo.it:58081/</key>
+<!--     <key name="url">http://localhost:58081/</key> -->
   </section>
 </helm_registry>
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,
   <property name="type">GTK_WINDOW_TOPLEVEL</property>
   <property name="window_position">GTK_WIN_POS_NONE</property>
   <property name="modal">False</property>
-  <property name="default_width">300</property>
+  <property name="default_width">450</property>
   <property name="default_height">800</property>
   <property name="resizable">True</property>
   <property name="destroy_with_parent">False</property>
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)))
 
   (** <DEBUGGING> *)
 
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