X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FcicMathView.ml;h=effa760014fe0bb87ff4734c733f92d3b03022c1;hb=b3afed9fd3cc38ecd4578f6b0741be50872a2828;hp=d619482de46779081001caffab56a328dcd8c8ff;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/matita/cicMathView.ml b/matitaB/matita/cicMathView.ml
index d619482de..effa76001 100644
--- a/matitaB/matita/cicMathView.ml
+++ b/matitaB/matita/cicMathView.ml
@@ -242,7 +242,7 @@ object (self)
   initializer
     self#source_buffer#set_language (Some MatitaGtkMisc.matita_lang);
     self#source_buffer#set_highlight_syntax true;
-    self#set_editable false;
+    self#set_editable false; 
     MatitaMisc.observe_font_size
      (fun size ->
        self#misc#modify_font_by_name
@@ -637,7 +637,7 @@ object (self)
     let sequent = List.assoc metano metasenv in
     let txt =
      ApplyTransformation.ntxt_of_cic_sequent
-      ~map_unicode_to_tex:false 80 status ~metasenv ~subst (metano,sequent)
+      ~map_unicode_to_tex:false 50 status ~metasenv ~subst (metano,sequent)
     in
     (* MATITA 1.0 if BuildTimeConf.debug then begin
       let name =
@@ -651,7 +651,7 @@ object (self)
    'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit
    = fun status obj ->
     let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false
-    80 status obj in
+    20 status obj in
 (*
     self#set_cic_info
       (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));