-let eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri status ast =
- GrafiteEngine.eval_ast
- ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths)
- ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
- ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ?do_heavy_checks ?clean_baseuri status ast
+let disambiguate_command lexicon_status_ref status cmd =
+ let lexicon_status,metasenv,cmd =
+ GrafiteDisambiguate.disambiguate_command
+ ~baseuri:(
+ try
+ Some (GrafiteTypes.get_string_option status "baseuri")
+ with
+ GrafiteTypes.Option_error _ -> None)
+ !lexicon_status_ref (GrafiteTypes.get_proof_metasenv status) cmd
+ in
+ lexicon_status_ref := lexicon_status;
+ GrafiteTypes.set_metasenv metasenv status,cmd
+
+let disambiguate_tactic lexicon_status_ref status goal tac =
+ let metasenv,tac =
+ GrafiteDisambiguate.disambiguate_tactic
+ lexicon_status_ref
+ (GrafiteTypes.get_proof_context status goal)
+ (GrafiteTypes.get_proof_metasenv status)
+ tac
+ in
+ GrafiteTypes.set_metasenv metasenv status,tac