- ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- sequents_observer);
- ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- proof_observer);
- ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- xmldump_observer);
- proof#notify;
- set_proof (Some proof)
-
-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 abort_proof () =
- if has_proof () then begin
- set_proof None;
- sequents_viewer#reset
- end
-
-let proof_handler =
- { MatitaTypes.get_proof = get_proof;
- MatitaTypes.abort_proof = abort_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, expr) =
- disambiguator#disambiguateTerm (Stream.of_string input)
- in
- let proof = MatitaProof.proof ~typ:expr ~metasenv () in
- new_proof proof));
- ignore (gui#main#openMenuItem#connect#activate (fun _ ->
- match gui#chooseFile () with
- | None -> ()
- | Some f when is_proof_script f ->
- gui#script#scriptTextView#buffer#set_text (input_file f);
- gui#script#scriptWin#show ();
- gui#main#showScriptMenuItem#set_active true
- | Some f ->
- gui#console#echo_error (sprintf
- "Don't know what to do with file: %s\nUnrecognized file format."
- f)))