- selection attribute of maction is now explicitly generated

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

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index c35cdb377d700c8df6de42375fa80a34617359ab..06ba96a221da88f91ce8f623e1b4e634bcce00da 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -33,6 +33,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
+let use_stylesheets = ref true;;(* false performs the transformations in OCaml*)
+
 (* List utility functions *)
 exception Skip;;
 
@@ -145,7 +147,10 @@ class proof_viewer obj =
 
   inherit GMathViewAux.single_selection_math_view obj
 
+  initializer self#set_font_size 10
+
   val mutable current_infos = None
+  val mutable current_mml = None
 
   method make_sequent_of_selected_term =
    match self#get_selection with
@@ -196,11 +201,23 @@ class proof_viewer obj =
      ApplyStylesheets.mml_of_cic_object
       ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
     in
-     self#load_doc ~dom:mml ;
+      (match current_mml with
+          None ->
+prerr_endline "0000000000000000 CARICO L'mml PRODOTTO" ;
+           self#load_doc ~dom:mml ;
+           current_mml <- Some mml
+        | Some current_mml ->
+           self#freeze ;
+           XmlDiff.update_dom ~from:current_mml mml ;
+           self#thaw) ;
+(*
+      self#load_doc ~dom:mml ;
+      current_mml <- Some mml ;
+*)
      current_infos <-
       Some
        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ;
-     (acic, ids_to_inner_types, ids_to_inner_sorts)
+    (acic, ids_to_inner_types, ids_to_inner_sorts)
  end
 ;;
 
@@ -226,3 +243,7 @@ let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager
   end;
   mathview
 ;;
+
+let _ =
+ Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount
+;;