snapshot

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index cd8f6f7ab4333e43e2dfbc4795fb3601bcbc94ce..dd813debeff745fa449ab42f57a396a1664a7ca2 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -28,27 +28,50 @@ open MatitaGtkMisc
 (** {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 -> assert false),
+   (fun proof -> current_proof := Some 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} *)
 
 let _ = Helm_registry.load_from "matita.conf.xml"
 let _ = GMain.Main.init ()
 let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
+let parserr = new MatitaDisambiguator.parserr ()
+let mqiconn = MQIConn.init ()
+let disambiguator =
+  new MatitaDisambiguator.disambiguator ~parserr ~mqiconn
+    ~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 ()
 
   (** quit program, possibly asking for confirmation *)
 let quit () = GMain.Main.quit ()
 
 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?")
@@ -56,17 +79,22 @@ let _ =
     then
       ()  (* abort new proof process *)
     else
-      prerr_endline "nuova prova"
-      (* TODO Zack: FINQUI ora mi serve il disambiguatore *)
-  ))
+      let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in
+      let (env, metasenv, term) =
+        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)))
 
   (** <DEBUGGING> *)
 let _ =
   if BuildTimeConf.debug then begin
     gui#main#debugMenu#misc#show ();
     let addDebugItem ~label callback =
-      let item = GMenu.menu_item ~label () in
-      gui#main#debugMenu_menu#append item;
+      let item =
+        GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
+      in
       ignore (item#connect#activate callback)
     in
     addDebugItem "interactive user uri choice" (fun _ ->
@@ -78,10 +106,17 @@ let _ =
             "cic:/cinque.var"]
         in
         List.iter prerr_endline uris
-      with MatitaTypes.No_choice -> MatitaTypes.error "no choice");
-      addDebugItem "toggle auto disambiguation" (fun _ ->
-        Helm_registry.set_bool "matita.auto_disambiguation"
-          (not (Helm_registry.get_bool "matita.auto_disambiguation")))
+      with MatitaGtkMisc.Cancel -> MatitaTypes.error "no choice");
+    addDebugItem "toggle auto disambiguation" (fun _ ->
+      Helm_registry.set_bool "matita.auto_disambiguation"
+        (not (Helm_registry.get_bool "matita.auto_disambiguation")));
+    addDebugItem "mono line text input" (fun _ ->
+      prerr_endline (ask_text ~gui ~title:"title" ~msg:"message" ()));
+    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> *)