* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
-let disambiguate_command lexicon_status_ref status cmd =
+let disambiguate_tactic lexicon_status_ref grafite_status goal tac =
+ let metasenv,tac =
+ GrafiteDisambiguate.disambiguate_tactic
+ lexicon_status_ref
+ (GrafiteTypes.get_proof_context grafite_status goal)
+ (GrafiteTypes.get_proof_metasenv grafite_status)
+ tac
+ in
+ GrafiteTypes.set_metasenv metasenv grafite_status,tac
+
+let disambiguate_command lexicon_status_ref grafite_status cmd =
let lexicon_status,metasenv,cmd =
GrafiteDisambiguate.disambiguate_command
~baseuri:(
try
- Some (GrafiteTypes.get_string_option status "baseuri")
+ Some (GrafiteTypes.get_string_option grafite_status "baseuri")
with
GrafiteTypes.Option_error _ -> None)
- !lexicon_status_ref (GrafiteTypes.get_proof_metasenv status) cmd
+ !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd
in
lexicon_status_ref := lexicon_status;
- GrafiteTypes.set_metasenv metasenv status,cmd
+ GrafiteTypes.set_metasenv metasenv grafite_status,cmd
-let disambiguate_tactic lexicon_status_ref status goal tac =
- let metasenv,tac =
- GrafiteDisambiguate.disambiguate_tactic
+let disambiguate_macro lexicon_status_ref grafite_status macro context =
+ let metasenv,macro =
+ GrafiteDisambiguate.disambiguate_macro
lexicon_status_ref
- (GrafiteTypes.get_proof_context status goal)
- (GrafiteTypes.get_proof_metasenv status)
- tac
+ (GrafiteTypes.get_proof_metasenv grafite_status)
+ context macro
in
- GrafiteTypes.set_metasenv metasenv status,tac
+ GrafiteTypes.set_metasenv metasenv grafite_status,macro
let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
grafite_status ast
GrafiteEngine.eval_ast
~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref)
~disambiguate_command:(disambiguate_command lexicon_status_ref)
+ ~disambiguate_macro:(disambiguate_macro lexicon_status_ref)
?do_heavy_checks ?clean_baseuri grafite_status ast in
let new_lexicon_status =
LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in