X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=0066d1c1816fcc5d3a7ab8ea142d1eef1744ba4f;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=69bee68a534ee659b566e6f894945e901be28436;hpb=5c56a926588a63ceac31e6ddd6e3eeb02fadf3a9;p=helm.git diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 69bee68a5..0066d1c18 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -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 @@ -130,8 +131,8 @@ let _ = prerr_endline (UriManager.string_of_uri u)) (CicEnvironment.list_obj ())); addDebugItem "print selections" (fun () -> - let sequentViewer = MatitaMathView.sequentViewer_instance () in - List.iter MatitaLog.debug (sequentViewer#string_of_selections)); + 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 _ ->