snapshot

[helm.git] / helm / matita / matitaInterpreter.ml

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 8ec043a1b9eb270978076e3e6024ee9b02fb850b..4b87ec8f808012fcac907889e7484b4089dd18d5 100644 (file)
--- 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