-let eval_ast ?do_heavy_checks lexicon_status
- grafite_status (text,prefix_len,ast)
-=
- let lexicon_status_ref = ref lexicon_status in
- let baseuri = GrafiteTypes.get_baseuri grafite_status in
- let changed_lexicon = ref false in
- let wrap f x = changed_lexicon := true; f x in
- let grafite_status =
- match grafite_status.GrafiteTypes.ng_status with
- | GrafiteTypes.CommandMode _ ->
- { grafite_status with GrafiteTypes.ng_status =
- GrafiteTypes.CommandMode lexicon_status }
- | GrafiteTypes.ProofMode s ->
- { grafite_status with GrafiteTypes.ng_status =
- GrafiteTypes.ProofMode
- { s with NTacStatus.istatus = { s.NTacStatus.istatus with NTacStatus.lstatus = lexicon_status }}}
- in
- let new_grafite_status,new_objs =
+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
+ let baseuri = status#baseuri in
+ let new_status,new_objs =
+ match ast with
+ | G.Executable (_, G.Command (_, G.Coercion _)) when dump ->
+(* FG: some commands can not be executed when mmas are parsed *************)
+(* To be removed when mmas will be executed *)
+ status, `Old []
+ | ast ->