X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitacLib.ml;h=eb4ed69915f1e17cbc4b36639ed7500f1ef5d164;hb=729e08f5fb86b3ffee460fda4577b024ab5888aa;hp=706981937df97aace3cbf6369ff1321912962ad6;hpb=d284dd23d0e12a62a001d3473eadf4942d12ffaa;p=helm.git diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index 706981937..eb4ed6991 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -217,7 +217,6 @@ let compile atstart options fname = in let grafite_status = let rec aux_for_dump x grafite_status = - try match MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths grafite_status buf x @@ -226,21 +225,6 @@ let compile atstart options fname = | (g,None)::_ -> g | (g,Some _)::_ -> raise (AttemptToInsertAnAlias (g :> LexiconEngine.status)) - with MatitaEngine.EnrichedWithStatus - (GrafiteEngine.Macro (floc, f), grafite) as exn -> - match f (get_macro_context (Some grafite)) with - | _, GrafiteAst.Inline (_, _suri, _params) -> -(* - let str = - ApplyTransformation.txt_of_inline_macro style prefix suri - ?flavour - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - in - !out str; -*) - aux_for_dump x grafite - |_-> raise exn in aux_for_dump print_cb grafite_status in