MathML widget no longer used. Requesciat in pacem

[helm.git] / matita / matita / applyTransformation.mli

diff --git a/matita/matita/applyTransformation.mli b/matita/matita/applyTransformation.mli
index dbd0343ff600d4bdd3e09e62963c340e5adcacdb..7e1cfb6fb1c3860f1476492039266bcd87810951 100644 (file)
--- a/matita/matita/applyTransformation.mli
+++ b/matita/matita/applyTransformation.mli
@@ -50,6 +50,13 @@ val nmml_of_cic_sequent:
  int * NCic.conjecture ->                       (* sequent *)
   Gdome.document                                (* Math ML *)
 
+val ntxt_of_cic_sequent:
+ map_unicode_to_tex:bool -> int ->
+ #NCicCoercion.status ->
+ NCic.metasenv -> NCic.substitution ->          (* metasenv, substitution *)
+ int * NCic.conjecture ->                       (* sequent *)
+  string                                        (* text *)
+
 val mml_of_cic_object:
   Cic.obj ->                                  (* object *)
     Gdome.document *                            (* Math ML *)
@@ -63,6 +70,21 @@ val mml_of_cic_object:
 
 val nmml_of_cic_object: #NCicCoercion.status -> NCic.obj -> Gdome.document
 
+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 
@@ -79,6 +101,19 @@ val txt_of_cic_object:
   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 ->