]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/hbugs/tutors/search_pattern_apply_tutor.ml
When the stylesheet from TML to MathML generated a document without a root
[helm.git] / helm / hbugs / tutors / search_pattern_apply_tutor.ml
index 0893c195f0843492b277f217cd8da3ed03a31432..4790ab88ab7620c1d89045a8873f1ced8e838c85 100644 (file)
@@ -4,6 +4,13 @@ open Printf;;
 
 exception Empty_must;;
 
+module MQICallbacks =
+   struct
+      let log s = prerr_string s
+   end
+
+module MQI = MQueryInterpreter.Make(MQICallbacks)
+
 let broker_id = ref None
 let my_own_id = Hbugs_tutors_common.init_tutor ()
 let my_own_addr, my_own_port = "127.0.0.1", 50011
@@ -103,25 +110,18 @@ let callback (req: Http_types.request) outchan =
         (Exception ("parse_error", reason)))
       outchan
 
-let postgresqlconnectionstring =
- try
-  Sys.getenv "POSTGRESQL_CONNECTION_STRING"
- with
-  Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
-;;
-
 let main () =
+  let mqi_options = "" in (* default MathQL interpreter options *)
   try
     Sys.catch_break true;
     at_exit (fun () -> Hbugs_tutors_common.unregister_from_broker my_own_id);
     broker_id :=
       Some (Hbugs_tutors_common.register_to_broker
         my_own_id my_own_url "FOO" "Search_pattern_apply tutor");
-    Mqint.set_database Mqint.postgres_db ;
-    Mqint.init postgresqlconnectionstring ;
+    ignore (MQI.init mqi_options) ;
     Http_daemon.start'
       ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback;
-    Mqint.close ()
+    MQI.close mqi_options
   with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
 ;;