From 7477c3dbbc2fafe248d48302be0d6ba4cb38d062 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Jun 2009 09:17:53 +0000 Subject: [PATCH] Stricter type: the type now shows that disambiguation only alter the lexicon. In this way we are forced to manually set the content of the object in place of setting the whole object, that leads to information loss since in the meanwhile new commands may have altered the rest of the state. --- .../components/grafite_parser/grafiteDisambiguate.ml | 2 ++ .../components/grafite_parser/grafiteDisambiguate.mli | 6 +++--- helm/software/matita/matitaEngine.ml | 2 +- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index a0558d9f6..6b5dfca61 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -633,6 +633,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = in UriManager.uri_of_string (baseuri ^ "/" ^ name) in +(* let _try_new cic = (NCicLibrary.clear_cache (); NCicEnvironment.invalidate (); @@ -721,6 +722,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = ) ) in +*) try diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli index 0592de671..6565a4d9f 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -35,21 +35,21 @@ type lazy_tactic = GrafiteAst.tactic val disambiguate_tactic: - #LexiconEngine.status ref -> + LexiconEngine.status ref -> Cic.context -> Cic.metasenv -> int option -> tactic Disambiguate.disambiguator_input -> Cic.metasenv * lazy_tactic val disambiguate_command: - #NEstatus.status as 'status -> + LexiconEngine.status as 'status -> ?baseuri:string -> Cic.metasenv -> ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> 'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command val disambiguate_macro: - #LexiconEngine.status ref -> + LexiconEngine.status ref -> Cic.metasenv -> Cic.context -> ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input -> diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 6e6213734..6b16891c8 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -61,7 +61,7 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context = let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) = let lexicon_status = GrafiteTypes.get_estatus grafite_status in let dump = not (Helm_registry.get_bool "matita.moo") in - let lexicon_status_ref = ref lexicon_status in + let lexicon_status_ref = ref (lexicon_status :> LexiconEngine.status) in let baseuri = GrafiteTypes.get_baseuri grafite_status in let new_grafite_status,new_objs = match ast with -- 2.39.2