]> matita.cs.unibo.it Git - helm.git/commitdiff
Debugging code inserted bug in the code ;-)
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 22 Jul 2003 14:29:16 +0000 (14:29 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 22 Jul 2003 14:29:16 +0000 (14:29 +0000)
helm/gTopLevel/termViewer.ml

index 4f57d80ede454fae9f0e2403d37f17de00df6240..d5950a1c9043cdd3985d3963e2b980f58e7c515c 100644 (file)
@@ -33,7 +33,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-let use_stylesheets = ref false;;(* false performs the transformations in OCaml*)
+let use_stylesheets = ref true;;(* false performs the transformations in OCaml*)
 
 (* List utility functions *)
 exception Skip;;
@@ -198,22 +198,34 @@ class proof_viewer obj =
     =
      Cic2acic.acic_object_of_cic_object (Content2cic.cobj2obj cobj)
     in
+prerr_endline "0000000000000000 USO GLI STYLESHEETS" ;
      let mml =
       ApplyStylesheets.mml_of_cic_object
        ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
      in
+      (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) ;
    else
-prerr_endline "(******** INIZIO CONTENT ==> PRES **********)";
     let pres = Content2pres.content2pres ~ids_to_inner_sorts cobj in
     let time2 = Sys.time () in
     (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
     let xmlpres = Mpresentation.print_mpres pres in
     let time25 = Sys.time () in
+prerr_endline "(******** INIZIO CONTENT ==> PRES **********)";
      (*
      prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2)));
      Xml.pp xmlpres (Some "tmp");