ported to Dbi-disambiguation

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 197b6f1ee305b6db4d121934f19f228bd8d57795..4c6a6588b5094eda5bf1ea7eb9f8314465576222 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -62,7 +62,7 @@ let _ =
 (* GLOBAL CONSTANTS *)
 
 let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_handle = MQIC.init ~log:mqi_debug_fun ()
+let mqi_handle = MQIC.init_if_connected ~log:mqi_debug_fun ()
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
 
@@ -636,7 +636,10 @@ let refresh_goals ?(empty_notebook=true) notebook =
           begin
            notebook#set_current_page
             ~may_skip_switch_page_event:true metano ;
-           notebook#proofw#load_sequent metasenv currentsequent
+prerr_endline "CIAO CIAO" ;
+prerr_endline ("SEQUENTE CORRENTE: " ^ SequentPp.TextualPp.print_sequent currentsequent) ;
+           notebook#proofw#load_sequent metasenv currentsequent ;
+prerr_endline "pASSO CIAO CIAO"
           end
  with
   e ->
@@ -2869,13 +2872,16 @@ end
 (* MAIN *)
 
 let initialize_everything () =
+prerr_endline "STO PER CREARE LA PROOF WINDOW" ;
   let output =
     TermViewer.proof_viewer
      ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object
      ~width:350 ~height:280 ()
   in
+prerr_endline "CREATA" ;
   let notebook = new notebook in
   let rendering_window' = new rendering_window output notebook in
+prerr_endline "OK" ;
   rendering_window'#set_auto_disambiguation !auto_disambiguation;
   set_rendering_window rendering_window';
   let print_error_as_html prefix msg =
@@ -2893,6 +2899,7 @@ let initialize_everything () =
 ;;
 
 let main () =
+prerr_endline "CIAO" ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
  MQIC.close mqi_handle;