(* $Id$ *)
-open Printf
+module G = GrafiteAst
let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
let eval_ast ?do_heavy_checks lexicon_status
grafite_status (text,prefix_len,ast)
=
+ let dump = not (Helm_registry.get_bool "matita.moo") in
let lexicon_status_ref = ref lexicon_status in
let baseuri = GrafiteTypes.get_baseuri grafite_status in
let changed_lexicon = ref false in
{ s with NTacStatus.istatus = { s.NTacStatus.istatus with NTacStatus.lstatus = lexicon_status }}}
in
let new_grafite_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 *)
+ grafite_status, `Old []
+ | ast ->
GrafiteEngine.eval_ast
~disambiguate_tactic:(wrap (disambiguate_tactic text prefix_len lexicon_status_ref))
~disambiguate_command:(wrap (disambiguate_command lexicon_status_ref))
~disambiguate_macro:(wrap (disambiguate_macro lexicon_status_ref))
- ?do_heavy_checks grafite_status (text,prefix_len,ast) in
+ ?do_heavy_checks grafite_status (text,prefix_len,ast)
+ in
let new_lexicon_status =
if !changed_lexicon then
!lexicon_status_ref