X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FapplyTransformation.mli;h=d5886abd8a7e8b82aff0fae35b121264238560d4;hb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;hp=1b1b749e7653318e8c7c860b5217ac573b843e4e;hpb=0fde70bd19b8fdfa72b807b9713a02ad1bd91b5b;p=helm.git

diff --git a/matita/matita/applyTransformation.mli b/matita/matita/applyTransformation.mli
index 1b1b749e7..d5886abd8 100644
--- a/matita/matita/applyTransformation.mli
+++ b/matita/matita/applyTransformation.mli
@@ -33,94 +33,21 @@
 (*                                                                         *)
 (***************************************************************************)
 
-val mml_of_cic_sequent:
- Cic.metasenv ->                              (* metasenv *)
- Cic.conjecture ->                            (* sequent *)
-  Gdome.document *                              (* Math ML *)
-   Cic.conjecture *                             (* unshared sequent *)
-   (Cic.annconjecture *                         (* annsequent *)
-    ((Cic.id, Cic.term) Hashtbl.t *             (* id -> term *)
-     (Cic.id, Cic.id option) Hashtbl.t *        (* id -> father id *)
-     (Cic.id, Cic.hypothesis) Hashtbl.t *       (* id -> hypothesis *)
-     (Cic.id, Cic2acic.sort_kind) Hashtbl.t))   (* ids_to_inner_sorts *)
+val use_high_level_pretty_printer: bool ref
 
-val nmml_of_cic_sequent:
- #NCicCoercion.status ->
- NCic.metasenv -> NCic.substitution ->          (* metasenv, substitution *)
- int * NCic.conjecture ->                       (* sequent *)
-  Gdome.document                                (* Math ML *)
+class status :
+ object
+  inherit NCic.cstatus
+  inherit Interpretations.status
+  inherit TermContentPres.status
+ end
 
 val ntxt_of_cic_sequent:
- map_unicode_to_tex:bool -> int ->
- #NCicCoercion.status ->
- NCic.metasenv -> NCic.substitution ->          (* metasenv, substitution *)
+ metasenv:NCic.metasenv -> subst:NCic.substitution -> (* metasenv,substitution*)
+ map_unicode_to_tex:bool -> int -> #status ->
  int * NCic.conjecture ->                       (* sequent *)
-  string                                        (* text *)
-
-val mml_of_cic_object:
-  Cic.obj ->                                  (* object *)
-    Gdome.document *                            (* Math ML *)
-     (Cic.annobj *                              (* annobj *)
-      ((Cic.id, Cic.term) Hashtbl.t *           (* id -> term *)
-       (Cic.id, Cic.id option) Hashtbl.t *      (* id -> father id *)
-       (Cic.id, Cic.conjecture) Hashtbl.t *     (* id -> conjecture *)
-       (Cic.id, Cic.hypothesis) Hashtbl.t *     (* id -> hypothesis *)
-       (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
-       (Cic.id, Cic2acic.anntypes) Hashtbl.t))  (* ids_to_inner_types *)
-
-val nmml_of_cic_object: #NCicCoercion.status -> NCic.obj -> Gdome.document
+  (int * int * string) list * string            (* hyperlinks, text *)
 
 val ntxt_of_cic_object:
- map_unicode_to_tex:bool -> int -> #NCicCoercion.status -> NCic.obj -> string
-
-val txt_of_cic_sequent_all:
- map_unicode_to_tex:bool -> int ->
- Cic.metasenv ->                              (* metasenv *)
- Cic.conjecture ->                            (* sequent *)
-  string *                                    (* text *)
-   Cic.conjecture *                             (* unshared sequent *)
-   (Cic.annconjecture *                         (* annsequent *)
-    ((Cic.id, Cic.term) Hashtbl.t *             (* id -> term *)
-     (Cic.id, Cic.id option) Hashtbl.t *        (* id -> father id *)
-     (Cic.id, Cic.hypothesis) Hashtbl.t *       (* id -> hypothesis *)
-     (Cic.id, Cic2acic.sort_kind) Hashtbl.t))   (* ids_to_inner_sorts *)
-
-val txt_of_cic_term: 
-  map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term ->
-   string 
-val txt_of_cic_sequent: 
-  map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> string
-val txt_of_cic_sequent_conclusion: 
-  map_unicode_to_tex:bool -> output_type:[`Pattern | `Term] -> int ->
-   Cic.metasenv -> Cic.conjecture -> string
-
-(* columns, params, object *)
-val txt_of_cic_object: 
-  map_unicode_to_tex:bool -> 
-  ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:int -> 
-  int -> GrafiteAst.inline_param list -> Cic.obj ->
-    string
-
-val txt_of_cic_object_all: 
-  map_unicode_to_tex:bool -> 
-  ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:int -> 
-  int -> GrafiteAst.inline_param list -> Cic.obj ->
-    string *                                    (* text *)
-     (Cic.annobj *                              (* annobj *)
-      ((Cic.id, Cic.term) Hashtbl.t *           (* id -> term *)
-       (Cic.id, Cic.id option) Hashtbl.t *      (* id -> father id *)
-       (Cic.id, Cic.conjecture) Hashtbl.t *     (* id -> conjecture *)
-       (Cic.id, Cic.hypothesis) Hashtbl.t *     (* id -> hypothesis *)
-       (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
-       (Cic.id, Cic2acic.anntypes) Hashtbl.t))  (* ids_to_inner_types *)
-
-(* params, uri or baseuri *)
-val txt_of_inline_macro:
-  map_unicode_to_tex:bool -> GrafiteAst.inline_param list -> string ->
-    string
-
-val txt_of_macro:
-  map_unicode_to_tex:bool ->
-    Cic.metasenv ->
-    Cic.context ->
-    (Cic.term, Cic.lazy_term) GrafiteAst.macro -> string
+ map_unicode_to_tex:bool -> int -> #status -> NCic.obj ->
+  (int * int * string) list * string            (* hyperlinks, text *)