]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matita.ml
proof of concept implementation of cut and paste from gtkMathView to text
[helm.git] / helm / matita / matita.ml
index aae334abd56e79927c748b3636c02a3160222468..9207b1c05d1580e81330ad4cffd12057ce0ab34d 100644 (file)
@@ -44,7 +44,6 @@ let _ =
   MatitaDb.create_owner_environment ();
   MatitamakeLib.initialize ();
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
-  prerr_endline BuildTimeConf.gtkmathview_conf;
   GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
   ignore (GMain.Main.init ());
   CicEnvironment.set_trust (* environment trust *)
@@ -113,7 +112,8 @@ let _ =
   let sequent_viewer = MatitaMathView.sequentViewer_instance () in
   let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
   sequent_viewer#set_href_callback
-    (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri (UriManager.uri_of_string uri))));
+    (Some (fun uri -> (MatitaMathView.cicBrowser ())#load
+      (`Uri (UriManager.uri_of_string uri))));
   let browser_observer _ = MatitaMathView.refresh_all_browsers () in
   let sequents_observer status =
     sequents_viewer#reset;
@@ -159,12 +159,8 @@ let _ =
         prerr_endline (UriManager.string_of_uri u)) 
         (CicEnvironment.list_obj ()));
     addDebugItem "print selected terms" (fun () ->
-      let i = ref 0 in
-      List.iter
-        (fun t ->
-           incr i;
-           MatitaLog.debug (sprintf "%d: %s" !i (CicPp.ppterm t)))
-        (MatitaMathView.sequentViewer_instance ())#get_selected_terms);
+      let sequentViewer = MatitaMathView.sequentViewer_instance () in
+      MatitaLog.debug (sequentViewer#string_of_selected_terms));
     addDebugItem "dump getter settings" (fun _ ->
       prerr_endline (Http_getter_env.env_to_string ()));
     addDebugItem "getter: getalluris" (fun _ ->