snapshot

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index cd8f6f7ab4333e43e2dfbc4795fb3601bcbc94ce..530e477a8f45bcb319f1bfee256d7bd859f3f672 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -40,6 +40,13 @@ let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.def"
 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)
+    ()
 
   (** quit program, possibly asking for confirmation *)
 let quit () = GMain.Main.quit ()
@@ -56,8 +63,12 @@ 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
+      prerr_endline ("nuova prova: " ^ CicPp.ppterm term)
+      (* TODO Zack: FINQUI *)
   ))
 
   (** <DEBUGGING> *)
@@ -65,8 +76,9 @@ 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 +90,15 @@ 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" ()));
   end
   (** </DEBUGGING> *)