+let rec eval_command ?(mode=L.WithPreferences) status cmd =
+(*
+ let bmode = match mode with L.WithPreferences -> true | _ -> false in
+ Printf.eprintf "Include preferences: %b\n" bmode;
+*)
+ let cmd =
+ match cmd with
+ | L.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
+ let rec disambiguate =
+ function
+ CicNotationPt.ApplPattern l ->
+ CicNotationPt.ApplPattern (List.map disambiguate l)
+ | CicNotationPt.VarPattern id
+ when not
+ (List.exists
+ (function (CicNotationPt.IdentArg (_,id')) -> id'=id) args)
+ ->
+ let item = DisambiguateTypes.Id id in
+ begin try
+ let uri =
+ match DisambiguateTypes.Environment.find item status.aliases with
+ L.Ident_alias (_, uri)-> UriManager.uri_of_string uri
+ | _ -> assert false
+ in
+ CicNotationPt.UriPattern uri
+ with Not_found ->
+ prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^
+ (DisambiguateTypes.string_of_domain_item item));
+ dump_aliases prerr_endline "" status;
+ assert false
+ end
+ | p -> p
+ in
+ L.Interpretation
+ (loc, dsc, (symbol, args), disambiguate cic_appl_pattern)
+ | _-> cmd
+ in