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
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 =
'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));