X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=0066d1c1816fcc5d3a7ab8ea142d1eef1744ba4f;hb=650e3b3c9ff0b9cafb76a0edf8139a53446937ba;hp=610f22a4ec7943d6b3b53e7117fb10e9b5b1958b;hpb=39736960d48b9a19f3b7ca6e4d852a9dbcd4af76;p=helm.git diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 610f22a4e..0066d1c18 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -82,6 +82,7 @@ let script = let _ = let cic_math_view = MatitaMathView.cicMathView_instance () in let sequents_viewer = MatitaMathView.sequentsViewer_instance () in + sequents_viewer#load_logo; cic_math_view#set_href_callback (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri (UriManager.uri_of_string uri)))); @@ -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