- (** quit program, possibly asking for confirmation *)
-let quit () = GMain.Main.quit ()
-let _ = gui#setQuitCallback quit
-let _ = gui#main#debugMenu#misc#hide ()
+let quit () = (* quit program, asking for confirmation if needed *)
+ if not (has_proof ()) ||
+ (ask_confirmation ~gui
+ ~msg:("Proof in progress, are you sure you want to quit?") ())
+ then
+ GMain.Main.quit ()
+
+let proof_handler =
+ { MatitaTypes.get_proof = get_proof;
+ MatitaTypes.set_proof = set_proof;
+ MatitaTypes.has_proof = has_proof;
+ MatitaTypes.new_proof = new_proof;
+ MatitaTypes.quit = quit;
+ }
+
+let interpreter =
+ let console = gui#console in
+ new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
+
+let _ =
+ gui#setQuitCallback quit;
+ gui#setPhraseCallback interpreter#evalPhrase;
+ gui#main#debugMenu#misc#hide ();
+ ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
+ if has_proof () &&
+ not (ask_confirmation ~gui
+ ~msg:("Proof in progress, are you sure you want to start a new one?")
+ ())
+ then
+ () (* abort new proof process *)
+ else
+ let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in
+ let (env, metasenv, term) =
+ disambiguator#disambiguateTerm (Stream.of_string input)
+ in
+ let proof = MatitaProof.proof ~typ:term ~metasenv () in
+ new_proof proof))