]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/gTopLevel.ml
Luca (bugged) debugging stuff removed.
[helm.git] / helm / gTopLevel / gTopLevel.ml
index 6cf8f361844dcaa08c7e576fc29c57c7d35c92a2..4c6a6588b5094eda5bf1ea7eb9f8314465576222 100644 (file)
@@ -906,7 +906,6 @@ let
     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' ->
@@ -916,10 +915,7 @@ prerr_endline "LUCA: HO RICEVUTO UN CLICK" ;
          in 
           show_in_show_window_uri (UriManager.uri_of_string uri)
         else
-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 ())
+         ignore (mmlwidget#action_toggle n')
    in
     let _ =
      mmlwidget#connect#click (show_in_show_window_callback mmlwidget)