Luca (bugged) debugging stuff removed.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 6cf8f361844dcaa08c7e576fc29c57c7d35c92a2..4c6a6588b5094eda5bf1ea7eb9f8314465576222 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -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)

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index bd7d0066dc9bcced6082d94612d7a526b61af296..25570868b9385120b76881a667dd1a802d34ea04 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -244,7 +244,6 @@ Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml () ;
         let time1 = Sys.time () in
         self#load_root ~root:mml#get_documentElement ;
         let time2 = Sys.time () in
-       prerr_endline "LUCA: PASSO DA DOVE DEVO PASSARE" ; 
         debug_print ("Loading and displaying the proof took " ^
           string_of_float (time2 -. time1) ^ "seconds") ;
         current_mml <- Some mml