X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaEngine.ml;h=c13004c24917f51fcbe1609607656636e745ed9d;hb=e1625ad8b8065269c7d7395a8675780228259657;hp=a2effbe039d6656a47b5ad5b06417d0cab15a0be;hpb=779859f7a9e317e378d258897c289f447adea7ad;p=helm.git

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index a2effbe03..c13004c24 100644
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -58,6 +58,25 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context =
  in
   GrafiteTypes.set_metasenv metasenv grafite_status,macro
 
+let eval_macro_screenshot (status : GrafiteTypes.status) name =
+  let _,_,metasenv,subst,_ = status#obj in
+  let sequent = List.hd metasenv in
+  let mathml = 
+    ApplyTransformation.nmml_of_cic_sequent 
+      status metasenv subst sequent 
+  in
+  let domImpl = Gdome.domImplementation () in
+  ignore(domImpl#saveDocumentToFile 
+    ~name:(name^".xml") ~doc:mathml ());
+  ignore(Sys.command ("mathmlsvg --verbose=1 --font-size=20 --cut-filename=no " ^ 
+    Filename.quote (name^".xml")));
+  ignore(Sys.command ("convert " ^ 
+    Filename.quote (name^".svg") ^ " " ^ 
+    Filename.quote (name^".png")));
+  HLog.debug ("generated " ^ name ^ ".png");
+  status, `New []
+;;
+
 let eval_ast ?do_heavy_checks status (text,prefix_len,ast) =
  let dump = not (Helm_registry.get_bool "matita.moo") in
  let lexicon_status_ref = ref (status :> LexiconEngine.status) in