+ if success then begin
+ let new_offset = interpreter#endOffset + offset in
+ gui#lockScript (new_offset + locked_iter#offset);
+ parse new_offset
+ end else
+ raise Exit
+ end
+ in
+ try
+ parse 0
+ with Exit -> ()
+
+let script_back _ = not_implemented "script_back"
+
+let load_script fname =
+ gui#script#scriptTextView#buffer#set_text (input_file fname);
+ gui#script#scriptWin#show ();
+ gui#main#showScriptMenuItem#set_active true
+
+(** {2 GUI callbacks} *)
+
+let _ =
+ gui#setQuitCallback currentProof#quit;
+ gui#setPhraseCallback interpreter#evalPhrase;
+ gui#main#debugMenu#misc#hide ();
+ ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
+ gui#console#clear ();
+ gui#console#show ~msg:"theorem " ()));
+ ignore (gui#main#openMenuItem#connect#activate (fun _ ->
+ match gui#chooseFile () with
+ | None -> ()
+ | Some f when is_proof_script f -> load_script f
+ | Some f ->
+ gui#console#echo_error (sprintf
+ "Don't know what to do with file: %s\nUnrecognized file format."
+ f)));
+ connect_button gui#script#scriptWinForwardButton script_forward;
+ connect_button gui#script#scriptWinBackButton script_back;
+ connect_button gui#script#scriptWinJumpButton script_jump;
+ let module A = TacticAst in
+ let hole = CicAst.UserInput in
+ let tac ast _ = ignore (interpreter#evalAst (A.Tactic ast)) in
+ let tac_w_term ast _ =
+ gui#console#clear ();
+ gui#console#show ~msg:(TacticAstPp.pp_tactic ast) ();
+ gui#main#mainWin#present ()
+ in
+ let tbar = gui#toolbar in
+ connect_button tbar#introsButton (tac (A.Intros (None, [])));
+ connect_button tbar#applyButton (tac_w_term (A.Apply hole));
+ connect_button tbar#exactButton (tac_w_term (A.Exact hole));
+ connect_button tbar#elimButton (tac_w_term (A.Elim (hole, None)));
+ connect_button tbar#elimTypeButton (tac_w_term (A.ElimType hole));
+ connect_button tbar#splitButton (tac A.Split);
+ connect_button tbar#leftButton (tac A.Left);
+ connect_button tbar#rightButton (tac A.Right);
+ connect_button tbar#existsButton (tac A.Exists);
+ connect_button tbar#reflexivityButton (tac A.Reflexivity);
+ connect_button tbar#symmetryButton (tac A.Symmetry);
+ connect_button tbar#transitivityButton (tac_w_term (A.Transitivity hole));
+ connect_button tbar#assumptionButton (tac A.Assumption);
+ connect_button tbar#cutButton (tac_w_term (A.Cut hole));
+ connect_button tbar#autoButton (tac A.Auto)
+
+ (** <DEBUGGING> *)
+
+let _ =
+ if BuildTimeConf.debug then begin
+ gui#main#debugMenu#misc#show ();
+ let addDebugItem ~label callback =
+ let item =
+ GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
+ in
+ ignore (item#connect#activate callback)
+ in
+ addDebugItem "toggle auto disambiguation" (fun _ ->
+ Helm_registry.set_bool "matita.auto_disambiguation"
+ (not (Helm_registry.get_bool "matita.auto_disambiguation")));
+ addDebugItem "dump proof status to stdout" (fun _ ->
+ print_endline (currentProof#proof#toString));
+ addDebugItem "dump environment to \"env.dump\"" (fun _ ->
+ let oc = open_out "env.dump" in
+ CicEnvironment.dump_to_channel oc;
+ close_out oc);
+ addDebugItem "print selected terms" (fun () ->
+ let i = ref 0 in
+ List.iter
+ (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t)))
+ sequent_viewer#get_selected_terms);
+ addDebugItem "show cic browser" (fun () -> gui#browser#browserWin#show ());
+ end
+