From f60cb106a6a0aafff8f90d0240952516f04663f0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 22 Jul 2003 14:29:16 +0000 Subject: [PATCH] Debugging code inserted bug in the code ;-) --- helm/gTopLevel/termViewer.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 4f57d80ed..d5950a1c9 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -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"); -- 2.39.2