matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaEngine.cmi
matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx
-matitadaemon.cmo: matitaInit.cmi matitaGtkMisc.cmi matitaEngine.cmi
-matitadaemon.cmx: matitaInit.cmx matitaGtkMisc.cmx matitaEngine.cmx
+matitadaemon.cmo: matitaInit.cmi matitaGtkMisc.cmi matitaEngine.cmi \
+ applyTransformation.cmi
+matitadaemon.cmx: matitaInit.cmx matitaGtkMisc.cmx matitaEngine.cmx \
+ applyTransformation.cmx
matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi
matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi
matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
method ppmetasenv ~subst metasenv =
String.concat "\n"
(List.map
- (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 80 self
+ (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 20 self
~metasenv ~subst m) metasenv)
(*
method ppobj obj =
object
inherit NCic.cstatus
inherit Interpretations.status
- inherit TermContentPres.status
+ inherit TermContentPres.status
end
val ntxt_of_cic_sequent:
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 20 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));