(** {2 Internal status} *)
- (* TODO Zack: may be current_proofs if we want an MDI interface *)
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 -> assert false),
- (fun proof -> current_proof := Some proof),
+ | None -> failwith "No current proof"),
+ (fun proof -> current_proof := proof),
(fun () -> !current_proof <> None))
(** {2 Settings} *)
~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 ()
+ 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 ()
- (** quit program, possibly asking for confirmation *)
-let quit () = 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;
ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
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
disambiguator#disambiguateTerm (Stream.of_string input)
in
let proof = MatitaProof.proof ~typ:term ~metasenv () in
- new_proof proof;
- debug_print ("new proof, goal is: " ^ CicPp.ppterm term)))
+ new_proof proof))
(** <DEBUGGING> *)
let _ =
class commandState
~(disambiguator: MatitaTypes.disambiguator)
+ ~(proof_handler: MatitaTypes.proof_handler)
~(console: MatitaConsole.console)
- ~new_proof ()
+ ()
=
object
method evalPhrase s: state_tag =
let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
let proof = MatitaProof.proof ~typ:expr ~metasenv () in
- new_proof proof;
+ proof_handler.MatitaTypes.new_proof proof;
`Proof
+ | CommandAst.Quit _ ->
+ proof_handler.MatitaTypes.quit ();
+ `Command (* dummy answer *)
| _ ->
MatitaTypes.not_implemented (* TODO Zack *)
"MatitaInterpreter.commandState#evalPhrase: commands other than full theorem ones";
`Proof
end
+ (* TODO Zack FINQUI
+ * bisogna rivedere la grammatica di tatticali/comandi
+ * molti comandi (o addirittura tutti tranne Theorem) hanno senso anche nello
+ * stato proof, e' quindi un casino parsare la phrase. Un'idea potrebbe essere
+ * quella di tentare di parsare una tattica e se il parsing fallisce provare a
+ * parsare un comando (BLEAARGH). Oppure si puo' aggiungere una possibile entry
+ * nella grammatica delle tattiche che punti ad un comando (RI-BLEAARGH).
+ * Oppure boh ...
+ *)
class proofState
~(disambiguator: MatitaTypes.disambiguator)
+ ~(proof_handler: MatitaTypes.proof_handler)
~(console: MatitaConsole.console)
- ~get_proof ()
+ ()
=
object
method evalPhrase (s: string): state_tag =
class interpreter
~(disambiguator: MatitaTypes.disambiguator)
+ ~(proof_handler: MatitaTypes.proof_handler)
~(console: MatitaConsole.console)
- ~(get_proof: unit -> MatitaTypes.proof)
- ~(new_proof: MatitaTypes.proof -> unit)
()
=
let commandState =
- lazy (new commandState ~disambiguator ~console ~new_proof ())
+ lazy (new commandState ~disambiguator ~proof_handler ~console ())
in
let proofState =
- lazy (new proofState ~disambiguator ~console ~get_proof ())
+ lazy (new proofState ~disambiguator ~proof_handler ~console ())
in
object
val mutable state = Lazy.force commandState