(** {2 Internal status} *)
- (* TODO Zack: may be current_proofs if we want an MDI interface *)
-let (current_proof: MatitaProof.proof option ref) = ref None
+let (get_proof, set_proof, has_proof) =
+ let (current_proof: MatitaTypes.proof option ref) = ref None in
+ ((fun () ->
+ match !current_proof with
+ | Some proof -> proof
+ | None -> failwith "No current proof"),
+ (fun proof -> (* TODO Zack: this function should probably be smarter taking
+ care also of unregistering notifications subscriber and so on *)
+ current_proof := proof),
+ (fun () -> !current_proof <> None))
(** {2 Settings} *)
-let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
-let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.def"
+let debug_print = MatitaTypes.debug_print
(** {2 Initialization} *)
~chooseInterp:(interactive_interp_choice ~gui)
()
- (** quit program, possibly asking for confirmation *)
-let quit () = GMain.Main.quit ()
+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 (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 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 (!current_proof <> None) &&
+ if has_proof () &&
not (ask_confirmation ~gui
- ~msg:("Starting a new proof will abort current one,\n" ^
- "are you sure you want to continue?")
- ())
+ ~msg:("Proof in progress, are you sure you want to start a new one?")
+ ())
then
() (* abort new proof process *)
else
let (env, metasenv, term) =
disambiguator#disambiguateTerm (Stream.of_string input)
in
- prerr_endline ("nuova prova: " ^ CicPp.ppterm term)
- (* TODO Zack: FINQUI *)
- ))
+ let proof = MatitaProof.proof ~typ:term ~metasenv () in
+ new_proof proof))
(** <DEBUGGING> *)
let _ =
addDebugItem "multi line text input" (fun _ ->
prerr_endline
(ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ()));
+ addDebugItem "dump proof status to stdout" (fun _ ->
+ print_endline ((get_proof ())#status#toString));
end
(** </DEBUGGING> *)