+ currentProof#addObserver sequents_observer;
+ currentProof#addObserver browser_observer;
+ currentProof#connect `Quit (fun () ->
+ (* quit program, asking for confirmation if needed *)
+ if not (currentProof#onGoing ()) ||
+ (ask_confirmation ~gui
+ ~msg:("Proof in progress, are you sure you want to quit?") ())
+ then
+ GMain.Main.quit ();
+ false);
+ currentProof#connect `Abort (fun () -> sequents_viewer#reset; false)
+
+let interpreter =
+ let mathViewer = MatitaMathView.mathViewer () in
+ MatitaInterpreter.interpreter ~console:gui#console ~mathViewer ()
+let script = MatitaScript.script ~interpreter
+let _ =
+ let href_callback uri =
+ let term = CicAst.Uri (uri, None) in
+ ignore (interpreter#evalAst (TacticAst.Command (TacticAst.Check term)))
+ in
+ sequent_viewer#set_href_callback (Some href_callback)
+
+let console_callback s =
+ let module A = TacticAst in
+ let rec strip_locations = function
+ | A.LocatedTactical (loc, tac) -> strip_locations tac
+ | tac -> tac
+ in
+ let needed_by_script ast =
+ match strip_locations ast with
+ | A.Tactic _
+ | A.Command
+ (A.Inductive _ | A.Theorem _ | A.Coercion _ | A.Qed _ | A.Proof) ->
+ true
+ | _ -> false
+ in
+ let ast = disambiguator#parserr#parseTactical (Stream.of_string s) in
+ debug_print (sprintf "evaluating '%s'" s);
+ if needed_by_script ast then
+ script#advance s
+ else
+ interpreter#evalAst ast
+
+let console_callback s =
+ match gui#console#wrap_exn (fun () -> console_callback s) with
+ | None -> (false, false)
+ | Some outcome -> outcome
+
+(** {2 GUI callbacks} *)
+
+let _ =
+ gui#setQuitCallback currentProof#quit;
+ gui#setPhraseCallback console_callback;
+ 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 ->
+ ignore (gui#console#wrap_exn (fun () -> script#loadFrom f))
+ | Some f ->
+ gui#console#echo_error (sprintf
+ "Don't know what to do with file: %s\nUnrecognized file format."
+ f)));
+ ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ ->
+ ignore (MatitaMathView.cicBrowser ())));
+ let module A = TacticAst in
+ let hole = CicAst.UserInput in
+ let tac ast _ =
+ let ast = A.Tactic ast in
+ ignore (script#advance (TacticAstPp.pp_tactical 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 ()