added support for (textual) cut and paste of mathml/boxml markup

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index fbf3d500e07fa93736e8088480f340bc05a64183..69bee68a534ee659b566e6f894945e901be28436 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -52,7 +52,7 @@ let gui = MatitaGui.instance ()
 let script =
   let s = 
     MatitaScript.script 
-      ~view:(gui#sourceView :> GText.view)
+      ~source_view:gui#sourceView
       ~init:(Lazy.force MatitaEngine.initial_status) 
       ~mathviewer:(MatitaMathView.mathViewer ())
       ~urichooser:(fun uris ->
@@ -129,9 +129,9 @@ let _ =
       List.iter (fun (u,_,_) -> 
         prerr_endline (UriManager.string_of_uri u)) 
         (CicEnvironment.list_obj ()));
-    addDebugItem "print selected terms" (fun () ->
+    addDebugItem "print selections" (fun () ->
       let sequentViewer = MatitaMathView.sequentViewer_instance () in
-      MatitaLog.debug (sequentViewer#string_of_selected_terms));
+      List.iter MatitaLog.debug (sequentViewer#string_of_selections));
     addDebugItem "dump getter settings" (fun _ ->
       prerr_endline (Http_getter_env.env_to_string ()));
     addDebugItem "getter: getalluris" (fun _ ->