X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;h=91b2dd1a795fe470f8c72b282892ac04a7616df0;hb=98295941bee765a0cb4070eb3f2df553228c11c8;hp=409c7cd70f4a82ad2aa587cf89acfeb815883d89;hpb=4be3764541d8caa00737a686156907e7f2ae720c;p=helm.git diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 409c7cd70..91b2dd1a7 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -32,8 +32,6 @@ (* *) (***************************************************************************) -let use_stylesheets = ref false;;(* false performs the transformations in OCaml*) - (* List utility functions *) exception Skip;; @@ -110,10 +108,7 @@ class sequent_viewer obj = method load_sequent metasenv sequent = (**** SIAM QUI ****) let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) = - if !use_stylesheets then - ApplyStylesheets.mml_of_cic_sequent metasenv sequent - else - ApplyTransformation.mml_of_cic_sequent metasenv sequent + ChosenTransformer.mml_of_cic_sequent metasenv sequent in self#load_doc ~dom:sequent_mml ; (* @@ -213,12 +208,9 @@ class proof_viewer obj = = Cic2acic.acic_object_of_cic_object currentproof in let mml = - if !use_stylesheets then - ApplyStylesheets.mml_of_cic_object - ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types - else - ApplyTransformation.mml_of_cic_object - ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types in + ChosenTransformer.mml_of_cic_object + ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types + in current_infos <- Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);