Huge commit with several changes:

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a941bf0883476f87144b7fdafcb3dab8ff59725d..b221919d2e33a38433f3216bcb3498718541c06a 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -346,8 +346,8 @@ let cic2grafite context menv t =
     let width = max_int in
     let term_pp content_term =
       let pres_term = TermContentPres.pp_ast content_term in
-      let dummy_tbl = Hashtbl.create 1 in
-      let markup = CicNotationPres.render dummy_tbl pres_term in
+      let lookup_uri = fun _ -> None in
+      let markup = CicNotationPres.render ~lookup_uri pres_term in
       let s = "(" ^ BoxPp.render_to_string
        ~map_unicode_to_tex:(Helm_registry.get_bool
          "matita.paste_unicode_as_tex")
@@ -549,7 +549,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
                   "matita.paste_unicode_as_tex")
                 ~skip_thm_and_qed:true
                 ~skip_initial_lambdas:how_many_lambdas
-                80 GrafiteAst.Declarative "" obj
+                80 [] obj
           else
             if true then
               (* use cic2grafite *)
@@ -560,7 +560,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
                 Helm_registry.get_bool "matita.paste_unicode_as_tex"
              in
              ApplyTransformation.procedural_txt_of_cic_term
-                 ~map_unicode_to_tex 78 cc proof_term
+                 ~map_unicode_to_tex 78 [] cc proof_term
         in
         let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
         [],text,parsed_text_length
@@ -568,12 +568,12 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
         ProofEngineTypes.Fail _ as exn -> 
           raise exn
           (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
-  | TA.Inline (_,style,suri,prefix,flavour) ->
-       let str = 
+  | TA.Inline (_, suri, params) ->
+       let str = "\n\n" ^ 
          ApplyTransformation.txt_of_inline_macro
           ~map_unicode_to_tex:(Helm_registry.get_bool
             "matita.paste_unicode_as_tex")
-          style ?flavour prefix suri 
+          params suri 
        in
        [], str, String.length parsed_text