(* DEBUGGING *)
-module MQICallbacks =
- struct
- let log s = prerr_string s
- end
-
-module MQI = MQueryInterpreter.Make(MQICallbacks)
+module MQI = MQueryInterpreter
+module MQIC = MQIConn
(* GLOBAL CONSTANTS *)
-let mqi_options = "" (* default MathQL interpreter options *)
+let mqi_flags = [] (* default MathQL interpreter options *)
+let mqi_handle = MQIC.init mqi_flags prerr_string
let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
let locate_callback id =
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let result = MQueryGenerator.locate id in
+ let result = MQueryGenerator.locate mqi_handle id in
let uris =
List.map
(function uri,_ ->
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
TexTermEditor'.term_editor
+ mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
TexTermEditor'.term_editor
+ mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
(* moved here to have visibility of the ok button *)
let newinputt =
- TexTermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
+ TexTermEditor'.term_editor
+ mqi_handle
+ ~width:400 ~height:100 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
(function b ->
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
let must = MQueryLevels2.get_constraints expr in
let must',only = refine_constraints must in
- let results = MQueryGenerator.searchPattern must' only in
+ let results = MQueryGenerator.searchPattern mqi_handle must' only in
show_query_results results
with
e ->
None -> ()
| Some q ->
let results =
- MQI.execute mqi_options (MQueryUtil.query_of_text (Lexing.from_string q))
+ MQI.execute mqi_handle (MQueryUtil.query_of_text (Lexing.from_string q))
in
show_query_results results
with
| Some metano ->
let uris' =
TacticChaser.searchPattern
+ mqi_handle
~output_html:(output_html outputhtml) ~choose_must ()
~status:(proof, metano)
in
~packing:frame#add () in
let inputt =
TexTermEditor'.term_editor
+ mqi_handle
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
;;
let main () =
- if !usedb then ignore (MQI.init mqi_options) ;
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
- if !usedb then MQI.close mqi_options;
+ MQIC.close mqi_handle;
Hbugs.quit ()
;;