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 ->
show_in_show_window_obj uri obj
in
let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) =
+prerr_endline "LUCA: HO RICEVUTO UN CLICK" ;
match n with
None -> ()
| Some n' ->
in
show_in_show_window_uri (UriManager.uri_of_string uri)
else
- ignore (mmlwidget#action_toggle n')
+prerr_endline "LUCA: AZIONO L'ACTION" ;
+ ignore (mmlwidget#action_toggle n') ;
+ let Some doc = n'#get_ownerDocument in
+ ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/clicked_doc" ~doc ())
in
let _ =
mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
(* 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 =
;;
let main () =
+prerr_endline "CIAO" ;
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
MQIC.close mqi_handle;