initializer
self#source_buffer#set_language (Some MatitaGtkMisc.matita_lang);
self#source_buffer#set_highlight_syntax true;
initializer
self#source_buffer#set_language (Some MatitaGtkMisc.matita_lang);
self#source_buffer#set_highlight_syntax true;
'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit
= fun status obj ->
let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false
'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit
= fun status obj ->
let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false
(*
self#set_cic_info
(Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
(*
self#set_cic_info
(Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));