X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FgTopLevel.ml;h=e70946564a53b64b1d3b754b0e3b854429210993;hb=9e2b452ac3b4b5ba72834fd6e51e104e4faa032c;hp=0d0b7c4d171afe54dd25b143cbce86194ca8965c;hpb=78a92e3cc2deb60d306da93d9dcf987c1cb219ba;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 0d0b7c4d1..e70946564 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -172,6 +172,7 @@ let check_window uris =
       lazy 
        (let mmlwidget =
          TermViewer.sequent_viewer
+          ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
           ~packing:scrolled_window#add ~width:400 ~height:280 () in
         let expr =
          let term =
@@ -2270,6 +2271,7 @@ class scratch_window =
    ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let sequent_viewer =
   TermViewer.sequent_viewer
+   ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
 object(self)
  val mutable term = Cic.Rel 1                 (* dummy value *)
@@ -2350,8 +2352,9 @@ object(self)
     GBin.scrolled_window ~border_width:10
      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
    let proofw =
-    TermViewer.sequent_viewer ~width:400 ~height:275
-     ~packing:(scrolled_window1#add) () in
+    TermViewer.sequent_viewer
+     ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+     ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
    let _ = proofw_ref <- Some proofw in
    let hbox3 =
     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2530,8 +2533,9 @@ class empty_page =
   GBin.scrolled_window ~border_width:10
    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
  let proofw =
-  TermViewer.sequent_viewer ~width:400 ~height:275
-   ~packing:(scrolled_window1#add) () in
+  TermViewer.sequent_viewer
+   ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+   ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
 object(self)
  method proofw = (assert false : TermViewer.sequent_viewer)
  method content = vbox1
@@ -2848,7 +2852,11 @@ end
 (* MAIN *)
 
 let initialize_everything () =
-  let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
+  let output =
+    TermViewer.proof_viewer
+     ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object
+     ~width:350 ~height:280 ()
+  in
   let notebook = new notebook in
   let rendering_window' = new rendering_window output notebook in
   rendering_window'#set_auto_disambiguation !auto_disambiguation;