module Make(C:Callbacks) =
struct
- let locate_one_id id =
- let result = MQueryGenerator.locate id in
+ let locate_one_id mqi_handle id =
+ let result = MQueryGenerator.locate mqi_handle id in
let uris =
List.map
(function uri,_ ->
Uris of CicTextualParser0.uri list
| Symbols of (CicTextualParser0.interpretation -> Cic.term) list
- let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris=
+ let disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris=
let known_ids,resolve_id = id_to_uris in
let dom' =
let rec filter =
let list_of_uris =
List.map
(function
- CicTextualParser0.Id id -> Uris (locate_one_id id)
+ CicTextualParser0.Id id -> Uris (locate_one_id mqi_handle id)
| CicTextualParser0.Symbol (descr,choices) ->
(* CSC: Implementare la funzione di filtraggio manuale *)
(* CSC: corrispondente alla locate_one_id *)
sig
exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
val disambiguate_input :
+ MQIConn.handle ->
Cic.context ->
Cic.metasenv ->
CicTextualParser0.interpretation_domain_item list ->
(* 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 ()
;;
module Disambiguate' = Disambiguate.Make(C);;
- class term_editor_impl ?packing ?width ?height ?isnotempty_callback
+ class term_editor_impl mqi_handle ?packing ?width ?height ?isnotempty_callback
?share_id_to_uris_with () : term_editor
=
let id_to_uris =
~context:name_context ~metasenv CicTextualLexer.token lexbuf
in
let id_to_uris',metasenv,expr =
- Disambiguate'.disambiguate_input
+ Disambiguate'.disambiguate_input mqi_handle
context metasenv dom mk_metasenv_and_expr ~id_to_uris:!id_to_uris
in
id_to_uris := id_to_uris' ;
module Make (C : Disambiguate.Callbacks) :
sig
val term_editor :
+ MQIConn.handle ->
?packing:(GObj.widget -> unit) ->
?width:int ->
?height:int ->
module Disambiguate' = Disambiguate.Make(C);;
class term_editor_impl
+ mqi_handle
?packing ?width ?height
?isnotempty_callback ?share_id_to_uris_with () : term_editor
=
~context:name_context ~metasenv TexCicTextualLexer.token lexbuf
in
let id_to_uris',metasenv,expr =
- Disambiguate'.disambiguate_input
+ Disambiguate'.disambiguate_input mqi_handle
context metasenv dom mk_metasenv_and_expr ~id_to_uris:!id_to_uris
in
id_to_uris := id_to_uris' ;
module Make (C : Disambiguate.Callbacks) :
sig
val term_editor :
+ MQIConn.handle ->
?packing:(GObj.widget -> unit) ->
?width:int ->
?height:int ->
* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
-(* 30/04/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-module MQICallbacks =
- struct
- let log s = prerr_string s
- end
-
-module MQI = MQueryInterpreter.Make(MQICallbacks)
+module MQI = MQueryInterpreter
(* Query issuing functions **************************************************)
let get_query_info () = ! info
-let execute_query query =
+let execute_query handle query =
let module Util = MQueryUtil in
let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
let perm = 64 * 6 + 8 * 6 + 4 in
flush och
in
let execute q =
- let r = MQI.execute "" q in
+ let r = MQI.execute handle q in
if ! log_file <> "" then log q r;
info := string_of_int ! query_num :: ! info;
incr query_num;
(* Query building functions ************************************************)
-let locate s =
+let locate handle s =
let module M = MathQL in
let q =
M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
in
- execute_query q
+ execute_query handle q
-let searchPattern must_use can_use =
+let searchPattern handle must_use can_use =
let module M = MathQL in
let in_path s = (s, []) in
let assign v p = (in_path v, in_path p) in
(*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*)
print_endline "### "; MQueryUtil.text_of_query print_string (q_let_po opos 1) "\n"; flush stdout;
- execute_query (q_let_po opos 1)
+ execute_query handle (q_let_po opos 1)
(* the callback function must return false iff the query must be skipped *)
val set_confirm_query : (MathQL.query -> bool) -> unit
-val execute_query : MathQL.query -> MathQL.result
+val execute_query : MQIConn.handle -> MathQL.query -> MathQL.result
-val locate : string -> MathQL.result
+val locate : MQIConn.handle -> string -> MathQL.result
-val searchPattern : must_restrictions -> only_restrictions -> MathQL.result
+val searchPattern : MQIConn.handle -> must_restrictions -> only_restrictions -> MathQL.result
val get_query_info : unit -> string list
(******************************************************************************)
(* search arguments on which Apply tactic doesn't fail *)
-let searchPattern ?(output_html = (fun _ -> ())) ~choose_must () ~status =
+let searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
let ((_, metasenv, _, _), metano) = status in
let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
let rigth_must = List.map torigth_restriction must in
let rigth_only = Some (List.map torigth_restriction only) in
let result =
- MQueryGenerator.searchPattern
+ MQueryGenerator.searchPattern mqi_handle
(rigth_must,[],[]) (rigth_only,None,None) in
let uris =
List.map
* http://cs.unibo.it/helm/.
*)
-val searchPattern :
+val searchPattern : MQIConn.handle ->
?output_html:(string -> unit) ->
(* boolean value: true = in main position *)
choose_must:((MQueryGenerator.uri * bool) list list ->
(** accepted HTTP servers for ask_uwobo method forwarding *)
let valid_servers = [ "mowgli.cs.unibo.it:58080" ; "mowgli.cs.unibo.it" ; "localhost:58080" ] ;;
-module MQICallbacks =
- struct
- let log s = debug_print s
- end
-
-module MQI = MQueryInterpreter.Make(MQICallbacks)
-
-let mqi_options = "" (* default MathQL interpreter options *)
+let mqi_flags = [] (* default MathQL interpreter options *)
open Printf;;
let callback (req: Http_types.request) outchan =
try
debug_print (sprintf "Received request: %s" req#path);
- if req#path <> "/getpage" then
- ignore (MQI.init mqi_options);
(match req#path with
| "/execute" ->
+ let mqi_handle = MQIConn.init mqi_flags debug_print in
let query_string = req#param "query" in
let lexbuf = Lexing.from_string query_string in
let query = MQueryUtil.query_of_text lexbuf in
- let result = MQueryGenerator.execute_query query in
+ let result = MQueryGenerator.execute_query mqi_handle query in
let result_string = pp_result result in
+ MQIConn.close mqi_handle;
Http_daemon.respond ~body:result_string ~headers:[contype] outchan
| "/locate" ->
+ let mqi_handle = MQIConn.init mqi_flags debug_print in
let id = req#param "id" in
- let result = MQueryGenerator.locate id in
+ let result = MQueryGenerator.locate mqi_handle id in
+ MQIConn.close mqi_handle;
Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
| "/getpage" ->
(* TODO implement "is_permitted" *)
| "/searchPattern"
| "/matchConclusion"
| "/locateInductivePrinciple" ->
+ let mqi_handle = MQIConn.init mqi_flags debug_print in
let term_string = req#param "term" in
let lexbuf = Lexing.from_string term_string in
let (context, metasenv) = ([], []) in
in
let module Disambiguate' = Disambiguate.Make (Chat) in
let (id_to_uris', metasenv', term') =
- Disambiguate'.disambiguate_input
+ Disambiguate'.disambiguate_input mqi_handle
context metasenv dom mk_metasenv_and_expr id_to_uris
in
(match metasenv' with
| [] ->
let must',only = get_constraints term' req#path in
- let results = MQueryGenerator.searchPattern must' only in
+ let results = MQueryGenerator.searchPattern mqi_handle must' only in
Http_daemon.send_basic_headers ~code:200 outchan ;
Http_daemon.send_CRLF outchan ;
iter_file
Http_daemon.respond
~headers:[contype]
~body:"some implicit variables are still unistantiated :-("
- outchan)
-
+ outchan);
+ MQIConn.close mqi_handle
| invalid_request ->
Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
- if req#path <> "/getpage" then
- MQI.close mqi_options;
debug_print (sprintf "%s done!" req#path)
with
| Chat_unfinished -> prerr_endline "Chat unfinished, Try again!"
projects / helm.git / commitdiff