X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Fmatita.ml;h=0066d1c1816fcc5d3a7ab8ea142d1eef1744ba4f;hb=650e3b3c9ff0b9cafb76a0edf8139a53446937ba;hp=fbf3d500e07fa93736e8088480f340bc05a64183;hpb=ddff8ae1e15c9fcaf83320978a5cad509d734a74;p=helm.git

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index fbf3d500e..0066d1c18 100644
--- 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 ->
@@ -80,9 +80,10 @@ let script =
   
   (* math viewers *)
 let _ =
-  let sequent_viewer = MatitaMathView.sequentViewer_instance () in
+  let cic_math_view = MatitaMathView.cicMathView_instance () in
   let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
-  sequent_viewer#set_href_callback
+  sequents_viewer#load_logo;
+  cic_math_view#set_href_callback
     (Some (fun uri -> (MatitaMathView.cicBrowser ())#load
       (`Uri (UriManager.uri_of_string uri))));
   let browser_observer _ = MatitaMathView.refresh_all_browsers () in
@@ -93,9 +94,9 @@ let _ =
         sequents_viewer#load_sequents status;
         sequents_viewer#goto_sequent goal
     | Proof proof -> 
-        prerr_endline "sequents_viewer#load_logo_with_qed (no proof)"; ()
+        sequents_viewer#load_logo_with_qed
     | No_proof -> 
-        prerr_endline "sequents_viewer#load_logo (no proof)"; ()
+        sequents_viewer#load_logo
     | Intermediate _ -> 
         assert false (* only the engine may be in this state *)
   in
@@ -129,9 +130,9 @@ let _ =
       List.iter (fun (u,_,_) -> 
         prerr_endline (UriManager.string_of_uri u)) 
         (CicEnvironment.list_obj ()));
-    addDebugItem "print selected terms" (fun () ->
-      let sequentViewer = MatitaMathView.sequentViewer_instance () in
-      MatitaLog.debug (sequentViewer#string_of_selected_terms));
+    addDebugItem "print selections" (fun () ->
+      let cicMathView = MatitaMathView.cicMathView_instance () in
+      List.iter MatitaLog.debug (cicMathView#string_of_selections));
     addDebugItem "dump getter settings" (fun _ ->
       prerr_endline (Http_getter_env.env_to_string ()));
     addDebugItem "getter: getalluris" (fun _ ->