snapshot (notably: ported to mysql instead of dbi)

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index 7b38057517908102ef3728462240cf90fb764e5f..e7f4f677b5dc06f8ef56de8ccbd3bf8d0e9ae5b5 100644 (file)
--- 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 bb3391317dd26c268403a8fc6e9a32d4c0f2b783..249058f8b9d795ebcce09200faa1695def43501c 100644 (file)
--- 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 2cf2e52b845f38edc0923d5d117eba3225bad873..d04ac1867bd05b12ec41aa55f3724b355a71389e 100644 (file)
--- 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 389a14e8d2c78c8e9e5be3ad4dd62cd66ec60f18..1ca17a9edeeca546c8527864ae1ed09b1bee4d86 100644 (file)
--- 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 e7dc8ded4036b80d16c1137c4f826c1b410bc39a..7c272a828deac347d774ce49b915faa8d33af56d 100644 (file)
--- 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 b946ec69bf353f8028f8022f771b5c47130186ea..2619b9bb9968e5c20631bbe64523f7fd7feb6a9c 100644 (file)
--- 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 23de092bd14013c089907259bdfbb77ef5d372ff..01e85e0c45c0f4ba42bffa85c6d29902c955a275 100644 (file)
--- 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 9b432f845270d88febf2ded021965419e19274cc..5b7bbc8808ff05ffe739b2f8bc48c9996f8a2940 100644 (file)
--- 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 9c8ae97f34f974249dcf45d094b4440bb4c35689..8c45d4d59372e8a04ea8583207f921a2f6892bee 100644 (file)
--- 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