+let new_proof () =
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
+ let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
+ let notebook = (rendering_window ())#notebook in
+
+ let chosen = ref false in
+ let get_metasenv_and_term = ref (function _ -> assert false) in
+ let get_uri = ref (function _ -> assert false) in
+ let non_empty_type = ref false in
+ let window =
+ GWindow.window
+ ~width:600 ~modal:true ~title:"New Proof or Definition"
+ ~border_width:2 () in
+ let vbox = GPack.vbox ~packing:window#add () in
+ let hbox =
+ GPack.hbox ~border_width:0
+ ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ =
+ GMisc.label ~text:"Enter the URI for the new theorem or definition:"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let uri_entry =
+ GEdit.entry ~editable:true
+ ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
+ uri_entry#set_text dummy_uri;
+ uri_entry#select_region ~start:1 ~stop:(String.length dummy_uri);
+ let hbox1 =
+ GPack.hbox ~border_width:0
+ ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ =
+ GMisc.label ~text:"Enter the theorem or definition type:"
+ ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:5
+ ~packing:(vbox#pack ~expand:true ~padding:0) () in
+ (* the content of the scrolled_window is moved below (see comment) *)
+ let hbox =
+ GPack.hbox ~border_width:0
+ ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let okb =
+ GButton.button ~label:"Ok"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ = okb#misc#set_sensitive false in
+ let cancelb =
+ GButton.button ~label:"Cancel"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ (* moved here to have visibility of the ok button *)
+ let newinputt =
+ TermEditor'.term_editor
+ mqi_handle
+ ~width:400 ~height:100 ~packing:scrolled_window#add
+ ~share_environment_with:inputt ()
+ ~isnotempty_callback:
+ (function b ->
+ non_empty_type := b ;
+ okb#misc#set_sensitive (b && uri_entry#text <> ""))
+ in
+ let _ =
+ newinputt#set_term inputt#get_as_string ;
+ inputt#reset in
+ let _ =
+ uri_entry#connect#changed
+ (function () ->
+ okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
+ in
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+ (okb#connect#clicked
+ (function () ->
+ chosen := true ;
+ try
+ let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
+ let uristr = "cic:" ^ uri_entry#text in
+ let uri = UriManager.uri_of_string uristr in
+ if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
+ raise NotAUriToAConstant
+ else
+ begin
+ try
+ ignore (Http_getter.resolve' uri) ;
+ raise UriAlreadyInUse
+ with Http_getter_types.Unresolvable_URI _ ->
+ get_metasenv_and_term := (function () -> metasenv,parsed) ;
+ get_uri := (function () -> uri) ;
+ window#destroy ()
+ end
+ with
+ e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+ )) ;
+ window#show () ;
+ GtkThread.main ();
+ if !chosen then
+ try
+ let metasenv,expr = !get_metasenv_and_term () in
+ let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
+ ProofEngine.set_proof
+ (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
+ set_proof_engine_goal (Some 1) ;
+ refresh_goals notebook ;
+ refresh_proof output ;
+ !save_set_sensitive true ;
+ inputt#reset ;
+ ProofEngine.intros ~mk_fresh_name_callback () ;
+ refresh_goals notebook ;
+ refresh_proof output
+ with
+ InvokeTactics.RefreshSequentException e ->
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
+ | InvokeTactics.RefreshProofException e ->
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
+ | e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+let check_term_in_scratch scratch_window metasenv context expr =
+ try
+ let ty = CicTypeChecker.type_of_aux' metasenv context expr in
+ let expr = Cic.Cast (expr,ty) in
+ scratch_window#show () ;
+ scratch_window#set_term expr ;
+ scratch_window#set_context context ;
+ scratch_window#set_metasenv metasenv ;
+ scratch_window#sequent_viewer#load_sequent metasenv (111,context,expr)
+ with
+ e ->
+ print_endline ("? " ^ CicPp.ppterm expr) ;
+ raise e
+;;
+
+let check scratch_window () =
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
+ let metasenv =
+ match ProofEngine.get_proof () with
+ None -> []
+ | Some (_,metasenv,_,_) -> metasenv
+ in
+ let context =
+ match !ProofEngine.goal with
+ None -> []
+ | Some metano ->
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ canonical_context
+ in
+ try
+ let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
+ check_term_in_scratch scratch_window metasenv' context expr
+ with
+ e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+let show () =
+ try
+ show_in_show_window_uri (input_or_locate_uri ~title:"Show")
+ with
+ e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+exception NotADefinition;;
+
+let open_ () =
+ let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
+ let notebook = (rendering_window ())#notebook in
+ try
+ let uri = input_or_locate_uri ~title:"Open" in
+ CicTypeChecker.typecheck uri ;
+ let metasenv,bo,ty =
+ match CicEnvironment.get_cooked_obj uri with
+ Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
+ | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
+ | Cic.Constant _
+ | Cic.Variable _
+ | Cic.InductiveDefinition _ -> raise NotADefinition
+ in
+ ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ set_proof_engine_goal None ;
+ refresh_goals notebook ;
+ refresh_proof output ;
+ !save_set_sensitive true
+ with
+ InvokeTactics.RefreshSequentException e ->
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
+ | InvokeTactics.RefreshProofException e ->
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
+ | e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+let show_query_results results =
+ let window =
+ GWindow.window
+ ~modal:false ~title:"Query results." ~border_width:2 () in
+ let vbox = GPack.vbox ~packing:window#add () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:"Click on a URI to show that object"
+ ~packing:hbox#add () in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
+ ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
+ ignore
+ (List.map
+ (function (uri,_) ->
+ let n =
+ clist#append [uri]
+ in
+ clist#set_row ~selectable:false n
+ ) results
+ ) ;
+ clist#columns_autosize () ;
+ ignore
+ (clist#connect#select_row
+ (fun ~row ~column ~event ->
+ let (uristr,_) = List.nth results row in
+ match
+ MQueryMisc.cic_textual_parser_uri_of_string
+ (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
+ uristr)
+ with
+ CicTextualParser0.ConUri uri
+ | CicTextualParser0.VarUri uri
+ | CicTextualParser0.IndTyUri (uri,_)
+ | CicTextualParser0.IndConUri (uri,_,_) ->
+ show_in_show_window_uri uri
+ )
+ ) ;
+ window#show ()
+;;
+
+let refine_constraints (must_obj,must_rel,must_sort) =
+ let chosen = ref false in
+ let use_only = ref false in
+ let window =
+ GWindow.window
+ ~modal:true ~title:"Constraints refinement."
+ ~width:800 ~border_width:2 () in
+ let vbox = GPack.vbox ~packing:window#add () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text: "\"Only\" constraints can be enforced or not."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let onlyb =
+ GButton.toggle_button ~label:"Enforce \"only\" constraints"
+ ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
+ in
+ ignore
+ (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
+ (* Notebook for the constraints choice *)
+ let notebook =
+ GPack.notebook ~scrollable:true
+ ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ (* Rel constraints *)
+ let label =
+ GMisc.label
+ ~text: "Constraints on Rels" () in
+ let vbox' =
+ GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
+ () in
+ let hbox =
+ GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text: "You can now specify the constraints on Rels."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let expected_height = 25 * (List.length must_rel + 2) in
+ let height = if expected_height > 400 then 400 else expected_height in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10 ~height ~width:600
+ ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
+ let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
+ let mk_depth_button (hbox:GPack.box) d =
+ let mutable_ref = ref (Some d) in
+ let depthb =
+ GButton.toggle_button
+ ~label:("depth = " ^ string_of_int d)
+ ~active:true
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
+ in
+ ignore
+ (depthb#connect#toggled
+ (function () ->
+ let sel_depth = if depthb#active then Some d else None in
+ mutable_ref := sel_depth
+ )) ; mutable_ref
+ in
+ let rel_constraints =
+ List.map
+ (function p ->
+ let hbox =
+ GPack.hbox
+ ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:(MQGU.text_of_position (p:>MQGT.full_position))
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ match p with
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth'
+ ) must_rel in
+ (* Sort constraints *)
+ let label =
+ GMisc.label
+ ~text: "Constraints on Sorts" () in
+ let vbox' =
+ GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
+ () in
+ let hbox =
+ GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text: "You can now specify the constraints on Sorts."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let expected_height = 25 * (List.length must_sort + 2) in
+ let height = if expected_height > 400 then 400 else expected_height in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10 ~height ~width:600
+ ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
+ let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
+ let sort_constraints =
+ List.map
+ (function (p, sort) ->
+ let hbox =
+ GPack.hbox
+ ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:(MQGU.text_of_sort sort ^ " " ^ MQGU.text_of_position (p:>MQGT.full_position))
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ match p with
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None, sort
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', sort
+ ) must_sort in
+ (* Obj constraints *)
+ let label =
+ GMisc.label
+ ~text: "Constraints on constants" () in
+ let vbox' =
+ GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
+ () in
+ let hbox =
+ GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text: "You can now specify the constraints on constants."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let expected_height = 25 * (List.length must_obj + 2) in
+ let height = if expected_height > 400 then 400 else expected_height in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10 ~height ~width:600
+ ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
+ let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
+ let obj_constraints =
+ List.map
+ (function (p, uri) ->
+ let hbox =
+ GPack.hbox
+ ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:(uri ^ " " ^ (MQGU.text_of_position p))
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ match p with
+ | `InBody
+ | `InHypothesis
+ | `InConclusion
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None, uri
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', uri
+ ) must_obj in
+ (* Confirm/abort buttons *)
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let okb =
+ GButton.button ~label:"Ok"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let cancelb =
+ GButton.button ~label:"Abort"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
+ in
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+ (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
+ window#set_position `CENTER ;
+ window#show () ;
+ GtkThread.main ();
+ if !chosen then
+ let chosen_must_rel =
+ List.map
+ (function (position, ref_depth) -> MQGU.set_main_position position !ref_depth)
+ rel_constraints
+ in
+ let chosen_must_sort =
+ List.map
+ (function (position, ref_depth, sort) ->
+ MQGU.set_main_position position !ref_depth,sort)
+ sort_constraints
+ in
+ let chosen_must_obj =
+ List.map
+ (function (position, ref_depth, uri) -> MQGU.set_full_position position !ref_depth, uri)
+ obj_constraints
+ in
+ (chosen_must_obj,chosen_must_rel,chosen_must_sort),
+ (if !use_only then
+(*CSC: ???????????????????????? I assume that must and only are the same... *)
+ Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
+ else
+ None,None,None
+ )
+ else
+ raise NoChoice
+;;
+
+let completeSearchPattern () =
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
+ try
+ let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
+ let must = CGSearchPattern.get_constraints expr in
+ let must',only = refine_constraints must in
+ let query =
+ MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
+ in
+ let results = MQI.execute mqi_handle query in
+ show_query_results results
+ with
+ e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+let insertQuery () =
+ try
+ let chosen = ref None in
+ let window =
+ GWindow.window
+ ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
+ let vbox = GPack.vbox ~packing:window#add () in
+ let label =
+ GMisc.label ~text:"Insert Query. For Experts Only."
+ ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
+ ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let input = GText.view ~editable:true
+ ~packing:scrolled_window#add () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let okb =
+ GButton.button ~label:"Ok"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let loadb =
+ GButton.button ~label:"Load from file..."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let cancelb =
+ GButton.button ~label:"Abort"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+ (okb#connect#clicked
+ (function () ->
+ chosen := Some (input#buffer#get_text ()) ; window#destroy ())) ;
+ ignore
+ (loadb#connect#clicked
+ (function () ->
+ match
+ GToolbox.select_file ~title:"Select Query File" ()
+ with
+ None -> ()
+ | Some filename ->
+ let inch = open_in filename in
+ let rec read_file () =
+ try
+ let line = input_line inch in
+ line ^ "\n" ^ read_file ()
+ with
+ End_of_file -> ""
+ in
+ let text = read_file () in
+ input#buffer#delete input#buffer#start_iter input#buffer#end_iter ;
+ ignore (input#buffer#insert text))) ;
+ window#set_position `CENTER ;
+ window#show () ;
+ GtkThread.main ();
+ match !chosen with
+ None -> ()
+ | Some q ->
+ let results =
+ MQI.execute mqi_handle (MQueryUtil.query_of_text (Lexing.from_string q))
+ in
+ show_query_results results
+ with
+ e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+let choose_must list_of_must only =
+ let chosen = ref None in
+ let user_constraints = ref [] in
+ let window =
+ GWindow.window
+ ~modal:true ~title:"Query refinement." ~border_width:2 () in
+ let vbox = GPack.vbox ~packing:window#add () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:
+ ("You can now specify the genericity of the query. " ^
+ "The more generic the slower.")
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:
+ "Suggestion: start with faster queries before moving to more generic ones."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let notebook =
+ GPack.notebook ~scrollable:true
+ ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let _ =
+ let page = ref 0 in
+ let last = List.length list_of_must in
+ List.map
+ (function must ->
+ incr page ;
+ let label =
+ GMisc.label ~text:
+ (if !page = 1 then "More generic" else
+ if !page = last then "More precise" else " ") () in
+ let expected_height = 25 * (List.length must + 2) in
+ let height = if expected_height > 400 then 400 else expected_height in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10 ~height ~width:600
+ ~packing:(notebook#append_page ~tab_label:label#coerce) () in
+ let clist =
+ GList.clist ~columns:2 ~packing:scrolled_window#add
+ ~titles:["URI" ; "Position"] ()
+ in
+ ignore
+ (List.map
+ (function (position, uri) ->
+ let n =
+ clist#append
+ [uri; MQGUtil.text_of_position position]
+ in
+ clist#set_row ~selectable:false n
+ ) must
+ ) ;
+ clist#columns_autosize ()
+ ) list_of_must in
+ let _ =
+ let label = GMisc.label ~text:"User provided" () in
+ let vbox =
+ GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:"Select the constraints that must be satisfied and press OK."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let expected_height = 25 * (List.length only + 2) in
+ let height = if expected_height > 400 then 400 else expected_height in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10 ~height ~width:600
+ ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let clist =
+ GList.clist ~columns:2 ~packing:scrolled_window#add
+ ~selection_mode:`MULTIPLE
+ ~titles:["URI" ; "Position"] ()
+ in
+ ignore
+ (List.map
+ (function (position, uri) ->
+ let n =
+ clist#append
+ [uri; MQGUtil.text_of_position position]
+ in
+ clist#set_row ~selectable:true n
+ ) only
+ ) ;
+ clist#columns_autosize () ;
+ ignore
+ (clist#connect#select_row
+ (fun ~row ~column ~event ->
+ user_constraints := (List.nth only row)::!user_constraints)) ;
+ ignore
+ (clist#connect#unselect_row
+ (fun ~row ~column ~event ->
+ user_constraints :=
+ List.filter
+ (function uri -> uri != (List.nth only row)) !user_constraints)) ;
+ in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let okb =
+ GButton.button ~label:"Ok"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let cancelb =
+ GButton.button ~label:"Abort"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ (* actions *)
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+ (okb#connect#clicked
+ (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
+ window#set_position `CENTER ;
+ window#show () ;
+ GtkThread.main ();
+ match !chosen with
+ None -> raise NoChoice
+ | Some n ->
+ if n = List.length list_of_must then
+ (* user provided constraints *)
+ !user_constraints
+ else
+ List.nth list_of_must n
+;;
+
+let searchPattern () =
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
+ try
+ let proof =
+ match ProofEngine.get_proof () with
+ None -> assert false
+ | Some proof -> proof
+ in
+ match !ProofEngine.goal with
+ | None -> ()
+ | Some metano ->
+ let uris' =
+ TacticChaser.matchConclusion mqi_handle
+ ~choose_must () (proof, metano)
+ in
+ let uri' =
+ user_uri_choice ~title:"Ambiguous input."
+ ~msg: "Many lemmas can be successfully applied. Please, choose one:"
+ uris'
+ in
+ inputt#set_term uri' ;
+ InvokeTactics'.apply ()
+ with
+ e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+let choose_selection mmlwidget (element : Gdome.element option) =