]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/mmlinterface.ml
Initial revision
[helm.git] / helm / interface / mmlinterface.ml
index ddb273c894b2c7cf6f1a49672e76d548070b3d65..b95303d2f0805cac49c62d046f6bbec222ec8822 100755 (executable)
@@ -683,7 +683,9 @@ object(self)
   ignore(output#connect#selection_changed (choose_selection self)) ;
   ignore(nextb#connect#clicked (next self)) ;
   ignore(prevb#connect#clicked (prev self)) ;
-  ignore(checkb#connect#clicked (check self)) ;
+  (* LUCA: check disabled while compression is not fully implemented *)
+  (* ignore(checkb#connect#clicked (check self)) ; *)
+  checkb#misc#set_sensitive false ;
   ignore(closeb#connect#clicked window#misc#hide) ;
   ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
   let settings_window = new settings_window output scrolled_window0
@@ -789,6 +791,8 @@ end;;
 (* MAIN *)
 
 let _ =
+ (* first of all initialize the processor by requiring the desired stylesheets *)
+ XsltProcessor.initialize () ;
  build_uri_tree () ;
  let output = GMathView.math_view ~width:400 ~height:380 ()
  and label = GMisc.label ~text:"???" () in