match !ProofEngine.proof with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
+ ProofEngine.proof := Some(uri,metasenv,bo,ty);
if List.length metasenv = 0 then
begin
!qed_set_sensitive true ;
let uri_entry =
GEdit.entry ~editable:true
~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let hint_uri = "/foo.con" in
+ uri_entry#set_text hint_uri;
+ uri_entry#select_region ~start:1 ~stop:(String.length hint_uri);
let hbox1 =
GPack.hbox ~border_width:0
~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
- let must = MQueryLevels2.get_constraints expr in
+ let must = CGSearchPattern.get_constraints expr in
let must',only = refine_constraints must in
let query =
- MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
+ MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
in
let results = MQI.execute mqi_handle query in
show_query_results results
in
ignore
(List.map
- (function (uri,position) ->
+ (function (position, uri) ->
let n =
clist#append
- [uri; if position then "MainConclusion" else "Conclusion"]
+ [uri; MQGUtil.text_of_position position]
in
clist#set_row ~selectable:false n
) must
in
ignore
(List.map
- (function (uri,position) ->
+ (function (position, uri) ->
let n =
clist#append
- [uri; if position then "MainConclusion" else "Conclusion"]
+ [uri; MQGUtil.text_of_position position]
in
clist#set_row ~selectable:true n
) only
(* hbugs menu *)
let hbugs_menu = factory0#add_submenu "HBugs" in
let factory6 = new GMenu.factory hbugs_menu ~accel_group in
- let toggle_hbugs_menu_item =
+ let _ =
factory6#add_check_item
~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
in
+ let _ = factory6#add_item ~callback:Hbugs.notify "(Re)Submit status!" in
+ let _ = factory6#add_separator () in
+ let _ =
+ factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services"
+ in
+ let _ =
+ factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services"
+ in
(* settings menu *)
let settings_menu = factory0#add_submenu "Settings" in
let factory3 = new GMenu.factory settings_menu ~accel_group in