X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=cbaa08721cca870b1643e5005cbf7a62ae4a6825;hb=59945285cda6b39178eeffedb32a37d3141fe844;hp=34ca16d256e5460fd24f2f00d6b93d60e57abf87;hpb=8e6a30412bbac3acc0a020e0fe90d492b0fc6776;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 34ca16d25..cbaa08721 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -118,28 +118,7 @@ let wrap_with_make include_paths (f : GrafiteParser.statement) x =
           HLog.error "please create it.";
           raise (Failure ("No root file for "^mafilename))
       in
-      let initial_lexicon_status = 
-        CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script 
-      in
-      let b,x = 
-        try
-          GrafiteSync.push ();
-          LexiconSync.time_travel ~present:x ~past:initial_lexicon_status;
-          let rc = MatitacLib.Make.make root [tgt] in 
-          GrafiteSync.pop ();
-          CicNotation.reset ();
-          ignore(CicNotation2.load_notation ~include_paths:[]
-            BuildTimeConf.core_notation_script);
-          let x = List.fold_left (fun s c -> LexiconEngine.eval_command s c)
-            initial_lexicon_status (List.rev
-            x.LexiconEngine.lexicon_content_rev) 
-          in
-          rc,x
-        with 
-        | exn ->
-            HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
-            assert false
-      in
+      let b = MatitacLib.Make.make root [tgt] in
       if b then 
         try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
          raise 
@@ -440,7 +419,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
      [], "", parsed_text_length
   | TA.WHint (loc, term) ->
      let _subst = [] in
-     let s = ((None,[0,[],term], _subst, Cic.Meta (0,[]) ,term, []),0) in
+     let s = ((None,[0,[],term], _subst, lazy (Cic.Meta (0,[])) ,term, []),0) in
      let l = List.map fst (MQ.experimental_hint ~dbd s) in
      let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
@@ -561,25 +540,11 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
               cic2grafite cc menv proof_term 
             else
               (* alternative using FG stuff *)
-              let proof_term, how_many_lambdas = 
-                Auto.lambda_close ~prefix_name:"orrible_hack_" 
-                  proof_term menv cc 
-              in
-              let ty,_ = 
-                CicTypeChecker.type_of_aux'
-                  menv [] proof_term CicUniv.empty_ugraph
-              in
-              let obj = 
-                Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma])
-              in
-                Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+"
-                 (strip_comments
-                  (ApplyTransformation.txt_of_cic_object
-                    ~map_unicode_to_tex:(Helm_registry.get_bool
-                      "matita.paste_unicode_as_tex")
-                    ~skip_thm_and_qed:true
-                    ~skip_initial_lambdas:how_many_lambdas
-                    80 (GrafiteAst.Procedural None) "" obj)) 
+              let map_unicode_to_tex =
+	         Helm_registry.get_bool "matita.paste_unicode_as_tex"
+	      in
+	      ApplyTransformation.procedural_txt_of_cic_term
+                 ~map_unicode_to_tex 78 cc proof_term
         in
         let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
         [],text,parsed_text_length
@@ -587,12 +552,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) ->
+  | TA.Inline (_,style,suri,prefix,flavour) ->
        let str = 
          ApplyTransformation.txt_of_inline_macro
           ~map_unicode_to_tex:(Helm_registry.get_bool
             "matita.paste_unicode_as_tex")
-          style suri prefix 
+          style ?flavour prefix suri 
        in
        [], str, String.length parsed_text