From: Andrea Asperti Date: Fri, 5 Nov 2010 09:39:58 +0000 (+0000) Subject: - lexiconSync merged into grafiteDisambiguate X-Git-Tag: make_still_working~2721 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb4cdb69cadc581f4f32e73c055dbadda0ed8703;p=helm.git - lexiconSync merged into grafiteDisambiguate --- diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 8d299a533..30c176fd2 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -409,7 +409,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status, composites = NCicCoercDeclaration.eval_ncoercion status name t ty source target in - LexiconSync.add_aliases_for_objs status composites + GrafiteDisambiguate.add_aliases_for_objs status composites | GrafiteAst.NQed loc -> if status#ng_mode <> `ProofMode then raise (GrafiteTypes.Command_error "Not in proof mode") @@ -479,7 +479,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let uris = uri::List.rev uris_rev in *) let status = status#set_ng_mode `CommandMode in - let status = LexiconSync.add_aliases_for_objs status [uri] in + let status = GrafiteDisambiguate.add_aliases_for_objs status [uri] in let status = List.fold_left (fun status boxml -> @@ -550,7 +550,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = basic_eval_and_record_ncoercion_from_t_cpos_arity status (name,t,cpos,arity) in - LexiconSync.add_aliases_for_objs status nuris + GrafiteDisambiguate.add_aliases_for_objs status nuris with MultiPassDisambiguator.DisambiguationError _-> HLog.warn ("error in generating coercion: "^name); status) diff --git a/matita/components/lexicon/Makefile b/matita/components/lexicon/Makefile index b7aba0ebd..273aade43 100644 --- a/matita/components/lexicon/Makefile +++ b/matita/components/lexicon/Makefile @@ -3,7 +3,6 @@ PREDICATES = INTERFACE_FILES = \ grafiteDisambiguate.mli \ - lexiconSync.mli \ $(NULL) IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) diff --git a/matita/components/lexicon/grafiteDisambiguate.ml b/matita/components/lexicon/grafiteDisambiguate.ml index 058ddaec3..88915c893 100644 --- a/matita/components/lexicon/grafiteDisambiguate.ml +++ b/matita/components/lexicon/grafiteDisambiguate.ml @@ -314,3 +314,19 @@ let disambiguate_cic_appl_pattern status args = in disambiguate ;; + +let add_aliases_for_objs status = + List.fold_left + (fun status nref -> + let references = NCicLibrary.aliases_of nref in + let new_env = + List.map + (fun u -> + let name = NCicPp.r2s true u in + DisambiguateTypes.Id name, + GrafiteAst.Ident_alias (name,NReference.string_of_reference u) + ) references + in + set_proof_aliases status ~implicit_aliases:false + GrafiteAst.WithPreferences new_env + ) status diff --git a/matita/components/lexicon/grafiteDisambiguate.mli b/matita/components/lexicon/grafiteDisambiguate.mli index 401eba115..15dc42ae4 100644 --- a/matita/components/lexicon/grafiteDisambiguate.mli +++ b/matita/components/lexicon/grafiteDisambiguate.mli @@ -49,6 +49,8 @@ val set_proof_aliases: GrafiteAst.inclusion_mode -> (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status +val add_aliases_for_objs: #status as 'status -> NUri.uri list -> 'status + (* args: print function, message (may be empty), status *) val dump_aliases: (string -> unit) -> string -> #status -> unit diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml deleted file mode 100644 index e06c04372..000000000 --- a/matita/components/lexicon/lexiconSync.ml +++ /dev/null @@ -1,42 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let add_aliases_for_objs status = - List.fold_left - (fun status nref -> - let references = NCicLibrary.aliases_of nref in - let new_env = - List.map - (fun u -> - let name = NCicPp.r2s true u in - DisambiguateTypes.Id name, - GrafiteAst.Ident_alias (name,NReference.string_of_reference u) - ) references - in - GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false - GrafiteAst.WithPreferences new_env - ) status diff --git a/matita/components/lexicon/lexiconSync.mli b/matita/components/lexicon/lexiconSync.mli deleted file mode 100644 index b46af6fbb..000000000 --- a/matita/components/lexicon/lexiconSync.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -val add_aliases_for_objs: - #GrafiteDisambiguate.status as 'status -> NUri.uri list -> 'status