From 8e6a30412bbac3acc0a020e0fe90d492b0fc6776 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 17 Jun 2008 14:18:12 +0000 Subject: [PATCH] reordering of lexicon status partially avoided to make it sure that interpretations are not moved around. I still argue that an alias can be removed from the back of an interpretation, no idea how this would interfere with CSC recent patch --- .../acic_content/termAcicContent.ml | 8 ++++++-- .../content_pres/termContentPres.ml | 5 ++++- .../components/lexicon/lexiconEngine.ml | 19 +++++++++++++++---- helm/software/matita/matitaExcPp.ml | 2 ++ helm/software/matita/matitaScript.ml | 1 - 5 files changed, 27 insertions(+), 8 deletions(-) diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index da5aa4960..4c98e1ad9 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -381,7 +381,11 @@ let ast_of_acic ~output_type id_to_sort annterm = ast, term_info.uri let counter = ref ~-1 -let reset () = counter := ~-1;; +let reset () = + counter := ~-1; + Hashtbl.clear level2_patterns32; + Hashtbl.clear interpretations +;; let fresh_id = fun () -> incr counter; @@ -443,7 +447,7 @@ let lookup_interpretations symbol = let remove_interpretation id = (try - let _, symbol, _, _ = Hashtbl.find level2_patterns32 id in + let dsc, symbol, _, _ = Hashtbl.find level2_patterns32 id in let ids = Hashtbl.find interpretations symbol in ids := List.filter ((<>) id) !ids; Hashtbl.remove level2_patterns32 id; diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 1ee406623..e83fbc923 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -470,7 +470,10 @@ let fill_pos_info l1_pattern = l1_pattern aux true l1_pattern *) let counter = ref ~-1 -let reset () = counter := ~-1;; +let reset () = + counter := ~-1; + Hashtbl.clear level1_patterns21 +;; let fresh_id = fun () -> incr counter; diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index aadb3ddf2..8a51e9523 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -51,7 +51,12 @@ let add_lexicon_content cmds status = let content = status.lexicon_content_rev in let content' = List.fold_right - (fun cmd acc -> cmd :: (List.filter ((<>) cmd) acc)) + (fun cmd acc -> + match cmd with + | LexiconAst.Alias _ + | LexiconAst.Include _ + | LexiconAst.Notation _ -> cmd :: (List.filter ((<>) cmd) acc) + | LexiconAst.Interpretation _ -> if List.exists ((=) cmd) acc then acc else cmd::acc) cmds content in (* prerr_endline ("new lexicon content: " ^ String.concat " " (List.map @@ -156,12 +161,18 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = | LexiconAst.Interpretation (_, dsc, (symbol, _), _) as stm -> let status = add_lexicon_content [stm] status in let diff = - [DisambiguateTypes.Symbol (symbol, 0), - DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] + try + [DisambiguateTypes.Symbol (symbol, 0), + DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] + with + DisambiguateChoices.Choice_not_found msg -> + prerr_endline (Lazy.force msg); + assert false in let status = set_proof_aliases mode status diff in status - | LexiconAst.Notation _ as stm -> add_lexicon_content [stm] status + | LexiconAst.Notation _ as stm -> + add_lexicon_content [stm] status let eval_command = eval_command ?mode:None diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index 24981af6b..312a9a4f8 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -147,6 +147,8 @@ let rec to_string = None, "Already defined: " ^ UriManager.string_of_uri s | CoercDb.EqCarrNotImplemented msg -> None, ("EqCarrNotImplemented: " ^ Lazy.force msg) + | DisambiguateChoices.Choice_not_found msg -> + None, ("Disambiguation choice not found: " ^ Lazy.force msg) | MatitaEngine.EnrichedWithLexiconStatus (exn,_) -> None, "EnrichedWithLexiconStatus "^snd(to_string exn) | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 9e0f85b58..34ca16d25 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -1115,7 +1115,6 @@ object (self) let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in (* CSC: why +1 in the following lines ???? *) let parsed_text_length = parsed_text_length + 1 in -prerr_endline ("## " ^ string_of_int parsed_text_length); let remain_len = String.length s - parsed_text_length in let next = String.sub s parsed_text_length remain_len in is_there_only_comments lexicon_status next -- 2.39.2