From: Luca Padovani <luca.padovani@unito.it>
Date: Tue, 28 Sep 2004 16:04:32 +0000 (+0000)
Subject: * minor correction to make the new mathml widget work better
X-Git-Tag: V_0_0_10~111
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=efd1d308c25b8167dfb0861e70c7381eb6dedc4b;p=helm.git

* minor correction to make the new mathml widget work better
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index ba0615246..6cf8f3618 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -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 ->
@@ -903,6 +906,7 @@ 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' ->
@@ -912,7 +916,10 @@ let
          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)
@@ -2869,13 +2876,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 +2903,7 @@ let initialize_everything () =
 ;;
 
 let main () =
+prerr_endline "CIAO" ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
  MQIC.close mqi_handle;
diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index 913cc9529..bd7d0066d 100644
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -127,10 +127,10 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
    let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
      mml_of_cic_sequent metasenv sequent
    in
+prerr_endline "PRIMA DI SALVARE IL FILE" ;
     self#load_root ~root:sequent_mml#get_documentElement ;
-(*
+prerr_endline "SALVO IL FILE IN TEMP" ;
 Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
-*)
      current_infos <-
       Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
  end
@@ -238,11 +238,13 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
     (* self#load_doc ~dom:mml ;
        current_mml <- Some mml ; *)
+Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml () ;
     (match current_mml with
       None ->
         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
diff --git a/helm/gTopLevel/xmlDiff.ml b/helm/gTopLevel/xmlDiff.ml
index cd19beb0c..c3a35ad34 100644
--- a/helm/gTopLevel/xmlDiff.ml
+++ b/helm/gTopLevel/xmlDiff.ml
@@ -181,7 +181,7 @@ let update_dom ~(from : Gdome.document) (d : Gdome.document) =
   else
    let t' = from#importNode t true in
     ignore (p#replaceChild ~newChild:t' ~oldChild:f) ;
-    ignore (highlight_node from t')
+    (* ignore (highlight_node from t') *)
   in
   match
    f#get_nodeType,t#get_nodeType
@@ -304,7 +304,8 @@ let update_dom ~(from : Gdome.document) (d : Gdome.document) =
                 (function n ->
                   let n' = from#importNode n true in
                     ignore (f#appendChild n') ;
-                    ignore (highlight_node from n')
+                    (* ignore (highlight_node from n') *)
+		    ()
                 ) tl2
             | tl1,[] ->
                List.iter (function n -> ignore (f#removeChild n)) tl1