~chooseUris:(interactive_user_uri_choice ~gui)
~chooseInterp:(interactive_interp_choice ~gui)
()
+let new_proof proof =
+ (* TODO Zack: high level function which create a new proof object and register
+ * to it the widgets which must be refreshed upon status changes *)
+(* proof#status#attach ... *)
+ proof#status#notify ();
+ set_proof proof
+let interpreter =
+ new MatitaInterpreter.interpreter
+ ~disambiguator ~console:gui#console ~get_proof ~new_proof ()
(** quit program, possibly asking for confirmation *)
let quit () = GMain.Main.quit ()
let _ =
gui#setQuitCallback quit;
+ gui#setPhraseCallback interpreter#evalPhrase;
gui#main#debugMenu#misc#hide ();
ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
if has_proof () &&
disambiguator#disambiguateTerm (Stream.of_string input)
in
let proof = MatitaProof.proof ~typ:term ~metasenv () in
-(* proof#status#attach ... FINQUI *)
- proof#status#notify ();
- set_proof proof;
+ new_proof proof;
debug_print ("new proof, goal is: " ^ CicPp.ppterm term)))
(** <DEBUGGING> *)