(* DEBUGGING *)
-let debug_print =
- let debug = true in
- fun s -> prerr_endline (sprintf "DEBUG: %s" s)
-;;
+module MQI = MQueryInterpreter
+module MQIC = MQIConn
+module MQG = MQueryGenerator
(* GLOBAL CONSTANTS *)
+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 htmlheader =
Not_found -> "/public/currentprooftype"
;;
-let postgresqlconnectionstring =
- try
- Sys.getenv "POSTGRESQL_CONNECTION_STRING"
- with
- Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
-;;
-
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
let htmlheader_and_content = ref htmlheader;;
(* MISC FUNCTIONS *)
-(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
-(* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE *)
-let get_last_query =
- let query = ref "" in
- let out s = query := ! query ^ s in
- MQueryGenerator.set_confirm_query
- (function q ->
- query := ""; MQueryUtil.text_of_query out q ""; true);
- function result ->
- out (!query ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
- !query
-;;
-
let
save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
=
match !ProofEngine.proof with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- !qed_set_sensitive (List.length metasenv = 0) ;
+ if List.length metasenv = 0 then
+ begin
+ !qed_set_sensitive true ;
+prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.clear ()" ;
+ Hbugs.clear ()
+ end
+ else
+begin
+prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ;
+ Hbugs.notify () ;
+end ;
(*CSC: Wrong: [] is just plainly wrong *)
uri,
(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
raise (InvokeTactics.RefreshSequentException e)
with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
-let __notify_hbugs = ref None;;
module InvokeTacticsCallbacks =
struct
let sequent_viewer () = (rendering_window ())#notebook#proofw
let decompose_uris_choice_callback = decompose_uris_choice_callback
let mk_fresh_name_callback = mk_fresh_name_callback
let output_html msg = output_html (outputhtml ()) msg
- let notify_hbugs () =
- match !__notify_hbugs with
- | Some f -> f ()
- | None -> assert false
end
;;
module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
-module Hbugs' = Hbugs.Make (InvokeTactics');;
-__notify_hbugs := Some Hbugs'.notify;;
+(* Just to initialize the Hbugs module *)
+module Ignore = Hbugs.Initialize (InvokeTactics');;
(** load an unfinished proof from filesystem *)
let load_unfinished_proof () =
("<h1 color=\"Green\">Current proof body loaded from " ^
prooffile ^ "</h1>") ;
!save_set_sensitive true;
- Hbugs'.notify ()
| _ -> assert false
with
InvokeTactics.RefreshSequentException e ->
let locate_callback id =
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let result = MQueryGenerator.locate id in
+ let out = output_html outputhtml in
+ let query = MQG.locate id in
+ let result = MQI.execute mqi_handle query in
let uris =
List.map
(function uri,_ ->
MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
result in
- let html =
- (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
- in
- output_html outputhtml html ;
+ out "<h1>Locate Query: </h1><pre>";
+ MQueryUtil.text_of_query out query "";
+ out "<h1>Result:</h1>";
+ MQueryUtil.text_of_result out result "<br>";
user_uri_choice ~title:"Ambiguous input."
~msg:
("Ambiguous input \"" ^ id ^
~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 ->
okb#misc#set_sensitive (b && uri_entry#text <> ""))
in
let _ =
+let xxx = inputt#get_as_string in
+prerr_endline ("######################## " ^ xxx) ;
+ newinputt#set_term xxx ;
+(*
newinputt#set_term inputt#get_as_string ;
+*)
inputt#reset in
let _ =
uri_entry#connect#changed
!save_set_sensitive true ;
inputt#reset ;
ProofEngine.intros ~mk_fresh_name_callback () ;
- Hbugs'.notify ();
refresh_goals notebook ;
refresh_proof output
with
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 query = MQG.query_of_constraints None must' only in
+ let results = MQI.execute mqi_handle query in
show_query_results results
with
e ->
None -> ()
| Some q ->
let results =
- Mqint.execute (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
let factory6 = new GMenu.factory hbugs_menu ~accel_group in
let toggle_hbugs_menu_item =
factory6#add_check_item
- ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs'.toggle "HBugs enabled"
+ ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
in
(* settings menu *)
let settings_menu = factory0#add_submenu "Settings" in
~packing:frame#add () in
let inputt =
TexTermEditor'.term_editor
+ mqi_handle
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
Gdome_xslt.setDebugCallback
(Some (print_error_as_html "XSLT Debug Message: "));
rendering_window'#show () ;
-(* Hbugs'.toggle true; *)
+(* Hbugs.toggle true; *)
GtkThread.main ()
;;
let main () =
- if !usedb then
- begin
- Mqint.set_database Mqint.postgres_db ;
- Mqint.init postgresqlconnectionstring ;
- end ;
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
- if !usedb then Mqint.close ();
- prerr_endline "FOO";
- Hbugs'.quit ()
+ MQIC.close mqi_handle;
+ Hbugs.quit ()
;;
try
projects / helm.git / blobdiff