snapshot

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 8954ec704af26b49dde3d8adcad6116fcee144ad..5fb0cb9061a7a8dfb6da9b9d39c3639be2dbef97 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -54,12 +54,45 @@ let disambiguator =
     ~chooseUris:(interactive_user_uri_choice ~gui)
     ~chooseInterp:(interactive_interp_choice ~gui)
     ()
+let proof_viewer =
+  let mml_of_cic_object = BuildTimeConf.Transformer.mml_of_cic_object in
+  MatitaMathView.proof_viewer ~mml_of_cic_object ~show:true
+    ~packing:(gui#proof#scrolledProof#add) ()
+(*
+let sequent_viewer =
+  let mml_of_cic_sequent = BuildTimeConf.Transformer.mml_of_cic_sequent in
+  MatitaMathView.sequent_viewer ~mml_of_cic_sequent ~show:true
+    ~packing:(gui#main#scrolledSequents#add) ()
+*)
 
-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 ();
+let new_proof (proof: MatitaTypes.proof) =
+  (* TODO Zack a lot:
+  * - ids_to_inner_types, ids_to_inner_sorts handling
+  * - sequent viewer notification
+  *)
+  let xmldump_observer _ (status, _) =  print_endline proof#toString in
+  ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
+    xmldump_observer);
+(*
+  let proof_observer _ (status, ()) =
+prerr_endline "proof_observer";
+    let ((uri_opt, metasenv, bo, ty), _) = status in
+    let uri = MatitaTypes.unopt_uri uri_opt in
+    (* TODO CSC [] is wrong *)
+    let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
+try
+      ignore (proof_viewer#load_proof uri proof)
+with exn ->
+prerr_endline "proof_observer exception:";
+prerr_endline (Printexc.to_string exn);
+raise exn
+  in
+  let proof_observer_id =
+    proof#attach_observer ~interested_in:StatefulProofEngine.all_events
+      proof_observer
+  in
+*)
+  proof#notify;
   set_proof (Some proof)
 
 let quit () = (* quit program, asking for confirmation if needed *)
@@ -94,10 +127,10 @@ let _ =
       ()  (* abort new proof process *)
     else
       let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in
-      let (env, metasenv, term) =
+      let (env, metasenv, expr) =
         disambiguator#disambiguateTerm (Stream.of_string input)
       in
-      let proof = MatitaProof.proof ~typ:term ~metasenv () in
+      let proof = MatitaProof.proof ~typ:expr ~metasenv () in
       new_proof proof))
 
   (** <DEBUGGING> *)
@@ -129,7 +162,7 @@ let _ =
       prerr_endline
         (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ()));
     addDebugItem "dump proof status to stdout" (fun _ ->
-      print_endline ((get_proof ())#status#toString));
+      print_endline ((get_proof ())#toString));
   end
   (** </DEBUGGING> *)