From e89486cad653803954662a5e543537acd49a866f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 30 Apr 2004 08:23:12 +0000 Subject: [PATCH] snapshot --- helm/matita/matita.ml | 39 ++++++++++++++++++++----------- helm/matita/matitaInterpreter.ml | 27 +++++++++++++++------ helm/matita/matitaInterpreter.mli | 3 +-- helm/matita/matitaTypes.ml | 9 +++++++ 4 files changed, 55 insertions(+), 23 deletions(-) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index dd813debe..8f34f5bf7 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -27,14 +27,13 @@ open MatitaGtkMisc (** {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} *) @@ -53,18 +52,32 @@ let disambiguator = ~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; @@ -73,9 +86,8 @@ let _ = 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 @@ -84,8 +96,7 @@ let _ = 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)) (** *) let _ = diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 8ec043a1b..4b87ec8f8 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -34,8 +34,9 @@ class type interpreterState = class commandState ~(disambiguator: MatitaTypes.disambiguator) + ~(proof_handler: MatitaTypes.proof_handler) ~(console: MatitaConsole.console) - ~new_proof () + () = object method evalPhrase s: state_tag = @@ -45,18 +46,31 @@ class commandState 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 = @@ -67,16 +81,15 @@ class proofState 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 diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli index fc529c3c0..1407f9c0e 100644 --- a/helm/matita/matitaInterpreter.mli +++ b/helm/matita/matitaInterpreter.mli @@ -25,9 +25,8 @@ class interpreter: disambiguator:MatitaTypes.disambiguator -> + proof_handler:MatitaTypes.proof_handler -> console:MatitaConsole.console -> - get_proof:(unit -> MatitaTypes.proof) -> - new_proof:(MatitaTypes.proof -> unit) -> unit -> MatitaTypes.interpreter diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 27783ec67..92fc79b7c 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -129,6 +129,15 @@ class type proof = method setStatus: proofStatus -> unit end +type proof_handler = + { get_proof: unit -> proof; (* return current proof or fail *) + set_proof: proof option -> unit; (* set a proof option as current proof *) + has_proof: unit -> bool; (* check if a current proof is available or not *) + new_proof: proof -> unit; (* as a set_proof but takes care also to register + observers *) + quit: unit -> unit + } + (** interpreter for toplevel phrases given via console *) class type interpreter = object -- 2.39.2