From 5553ac7623425bce6f34eed6e17d4f0f8163e9aa Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Oct 2010 09:01:00 +0000 Subject: [PATCH] - acic_content ==> content - termAcicContent ==> interpretations --- .../components/METAS/meta.helm-acic_content.src | 4 ---- matita/components/METAS/meta.helm-content.src | 4 ++++ .../components/METAS/meta.helm-content_pres.src | 2 +- .../METAS/meta.helm-disambiguation.src | 2 +- matita/components/METAS/meta.helm-grafite.src | 2 +- .../METAS/meta.helm-ng_cic_content.src | 2 +- .../METAS/meta.helm-ng_disambiguation.src | 2 +- matita/components/Makefile | 2 +- .../components/{acic_content => content}/.depend | 10 +++++----- .../{acic_content => content}/.depend.opt | 10 +++++----- .../{acic_content => content}/Makefile | 4 ++-- .../{acic_content => content}/cicNotationEnv.ml | 0 .../{acic_content => content}/cicNotationEnv.mli | 0 .../{acic_content => content}/cicNotationPp.ml | 0 .../{acic_content => content}/cicNotationPp.mli | 0 .../{acic_content => content}/cicNotationPt.ml | 0 .../{acic_content => content}/cicNotationUtil.ml | 0 .../cicNotationUtil.mli | 0 .../{acic_content => content}/content.ml | 0 .../{acic_content => content}/content.mli | 0 .../interpretations.ml} | 0 .../interpretations.mli} | 2 +- matita/components/lexicon/cicNotation.ml | 16 ++++++++-------- .../components/ng_cic_content/nTermCicContent.ml | 6 +++--- .../ng_disambiguation/disambiguateChoices.ml | 6 +++--- 25 files changed, 37 insertions(+), 37 deletions(-) delete mode 100644 matita/components/METAS/meta.helm-acic_content.src create mode 100644 matita/components/METAS/meta.helm-content.src rename matita/components/{acic_content => content}/.depend (72%) rename matita/components/{acic_content => content}/.depend.opt (72%) rename matita/components/{acic_content => content}/Makefile (84%) rename matita/components/{acic_content => content}/cicNotationEnv.ml (100%) rename matita/components/{acic_content => content}/cicNotationEnv.mli (100%) rename matita/components/{acic_content => content}/cicNotationPp.ml (100%) rename matita/components/{acic_content => content}/cicNotationPp.mli (100%) rename matita/components/{acic_content => content}/cicNotationPt.ml (100%) rename matita/components/{acic_content => content}/cicNotationUtil.ml (100%) rename matita/components/{acic_content => content}/cicNotationUtil.mli (100%) rename matita/components/{acic_content => content}/content.ml (100%) rename matita/components/{acic_content => content}/content.mli (100%) rename matita/components/{acic_content/termAcicContent.ml => content/interpretations.ml} (100%) rename matita/components/{acic_content/termAcicContent.mli => content/interpretations.mli} (98%) diff --git a/matita/components/METAS/meta.helm-acic_content.src b/matita/components/METAS/meta.helm-acic_content.src deleted file mode 100644 index 0013afa41..000000000 --- a/matita/components/METAS/meta.helm-acic_content.src +++ /dev/null @@ -1,4 +0,0 @@ -requires="helm-library helm-ng_kernel" -version="0.0.1" -archive(byte)="acic_content.cma" -archive(native)="acic_content.cmxa" diff --git a/matita/components/METAS/meta.helm-content.src b/matita/components/METAS/meta.helm-content.src new file mode 100644 index 000000000..6973a54d9 --- /dev/null +++ b/matita/components/METAS/meta.helm-content.src @@ -0,0 +1,4 @@ +requires="helm-library helm-ng_kernel" +version="0.0.1" +archive(byte)="content.cma" +archive(native)="content.cmxa" diff --git a/matita/components/METAS/meta.helm-content_pres.src b/matita/components/METAS/meta.helm-content_pres.src index 74b1b23c9..8db3fca82 100644 --- a/matita/components/METAS/meta.helm-content_pres.src +++ b/matita/components/METAS/meta.helm-content_pres.src @@ -1,4 +1,4 @@ -requires="helm-acic_content helm-ng_cic_content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite" +requires="helm-content helm-ng_cic_content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite" version="0.0.1" archive(byte)="content_pres.cma" archive(native)="content_pres.cmxa" diff --git a/matita/components/METAS/meta.helm-disambiguation.src b/matita/components/METAS/meta.helm-disambiguation.src index 706f6dd12..6c286ea71 100644 --- a/matita/components/METAS/meta.helm-disambiguation.src +++ b/matita/components/METAS/meta.helm-disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-acic_content" +requires="helm-content" version="0.0.1" archive(byte)="disambiguation.cma" archive(native)="disambiguation.cmxa" diff --git a/matita/components/METAS/meta.helm-grafite.src b/matita/components/METAS/meta.helm-grafite.src index 46a6fb338..f45beff90 100644 --- a/matita/components/METAS/meta.helm-grafite.src +++ b/matita/components/METAS/meta.helm-grafite.src @@ -1,4 +1,4 @@ -requires="helm-cic helm-acic_content helm-ng_kernel" +requires="helm-cic helm-content helm-ng_kernel" version="0.0.1" archive(byte)="grafite.cma" archive(native)="grafite.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_cic_content.src b/matita/components/METAS/meta.helm-ng_cic_content.src index 4823c8bc6..a2c08e135 100644 --- a/matita/components/METAS/meta.helm-ng_cic_content.src +++ b/matita/components/METAS/meta.helm-ng_cic_content.src @@ -1,4 +1,4 @@ -requires="helm-library helm-acic_content helm-ng_refiner" +requires="helm-library helm-content helm-ng_refiner" version="0.0.1" archive(byte)="ng_cic_content.cma" archive(native)="ng_cic_content.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_disambiguation.src b/matita/components/METAS/meta.helm-ng_disambiguation.src index 7910e8dff..84eeab3fe 100644 --- a/matita/components/METAS/meta.helm-ng_disambiguation.src +++ b/matita/components/METAS/meta.helm-ng_disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-acic_content helm-ng_refiner helm-disambiguation" +requires="helm-content helm-ng_refiner helm-disambiguation" version="0.0.1" archive(byte)="ng_disambiguation.cma" archive(native)="ng_disambiguation.cmxa" diff --git a/matita/components/Makefile b/matita/components/Makefile index 6b248d0e6..86fc08c69 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -19,7 +19,7 @@ MODULES = \ cic \ library \ ng_kernel \ - acic_content \ + content \ grafite \ disambiguation \ ng_kernel \ diff --git a/matita/components/acic_content/.depend b/matita/components/content/.depend similarity index 72% rename from matita/components/acic_content/.depend rename to matita/components/content/.depend index e8b9a6135..50d486b4f 100644 --- a/matita/components/acic_content/.depend +++ b/matita/components/content/.depend @@ -2,7 +2,7 @@ content.cmi: cicNotationUtil.cmi: cicNotationPt.cmo cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi -termAcicContent.cmi: cicNotationPt.cmo +interpretations.cmi: cicNotationPt.cmo cicNotationPt.cmo: cicNotationPt.cmx: content.cmo: content.cmi @@ -13,7 +13,7 @@ cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi -termAcicContent.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationPp.cmi \ - termAcicContent.cmi -termAcicContent.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationPp.cmx \ - termAcicContent.cmi +interpretations.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ + interpretations.cmi +interpretations.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ + interpretations.cmi diff --git a/matita/components/acic_content/.depend.opt b/matita/components/content/.depend.opt similarity index 72% rename from matita/components/acic_content/.depend.opt rename to matita/components/content/.depend.opt index a679f7253..9af10948d 100644 --- a/matita/components/acic_content/.depend.opt +++ b/matita/components/content/.depend.opt @@ -2,7 +2,7 @@ content.cmi: cicNotationUtil.cmi: cicNotationPt.cmx cicNotationEnv.cmi: cicNotationPt.cmx cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi -termAcicContent.cmi: cicNotationPt.cmx +interpretations.cmi: cicNotationPt.cmx cicNotationPt.cmo: cicNotationPt.cmx: content.cmo: content.cmi @@ -13,7 +13,7 @@ cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmx cicNotationEnv.cmi cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmo: cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmi cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi -termAcicContent.cmo: cicNotationUtil.cmi cicNotationPt.cmx cicNotationPp.cmi \ - termAcicContent.cmi -termAcicContent.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationPp.cmx \ - termAcicContent.cmi +interpretations.cmo: cicNotationUtil.cmi cicNotationPt.cmx \ + interpretations.cmi +interpretations.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ + interpretations.cmi diff --git a/matita/components/acic_content/Makefile b/matita/components/content/Makefile similarity index 84% rename from matita/components/acic_content/Makefile rename to matita/components/content/Makefile index 119aaaa73..2f1a3896a 100644 --- a/matita/components/acic_content/Makefile +++ b/matita/components/content/Makefile @@ -1,4 +1,4 @@ -PACKAGE = acic_content +PACKAGE = content PREDICATES = INTERFACE_FILES = \ @@ -6,7 +6,7 @@ INTERFACE_FILES = \ cicNotationUtil.mli \ cicNotationEnv.mli \ cicNotationPp.mli \ - termAcicContent.mli \ + interpretations.mli \ $(NULL) IMPLEMENTATION_FILES = \ cicNotationPt.ml \ diff --git a/matita/components/acic_content/cicNotationEnv.ml b/matita/components/content/cicNotationEnv.ml similarity index 100% rename from matita/components/acic_content/cicNotationEnv.ml rename to matita/components/content/cicNotationEnv.ml diff --git a/matita/components/acic_content/cicNotationEnv.mli b/matita/components/content/cicNotationEnv.mli similarity index 100% rename from matita/components/acic_content/cicNotationEnv.mli rename to matita/components/content/cicNotationEnv.mli diff --git a/matita/components/acic_content/cicNotationPp.ml b/matita/components/content/cicNotationPp.ml similarity index 100% rename from matita/components/acic_content/cicNotationPp.ml rename to matita/components/content/cicNotationPp.ml diff --git a/matita/components/acic_content/cicNotationPp.mli b/matita/components/content/cicNotationPp.mli similarity index 100% rename from matita/components/acic_content/cicNotationPp.mli rename to matita/components/content/cicNotationPp.mli diff --git a/matita/components/acic_content/cicNotationPt.ml b/matita/components/content/cicNotationPt.ml similarity index 100% rename from matita/components/acic_content/cicNotationPt.ml rename to matita/components/content/cicNotationPt.ml diff --git a/matita/components/acic_content/cicNotationUtil.ml b/matita/components/content/cicNotationUtil.ml similarity index 100% rename from matita/components/acic_content/cicNotationUtil.ml rename to matita/components/content/cicNotationUtil.ml diff --git a/matita/components/acic_content/cicNotationUtil.mli b/matita/components/content/cicNotationUtil.mli similarity index 100% rename from matita/components/acic_content/cicNotationUtil.mli rename to matita/components/content/cicNotationUtil.mli diff --git a/matita/components/acic_content/content.ml b/matita/components/content/content.ml similarity index 100% rename from matita/components/acic_content/content.ml rename to matita/components/content/content.ml diff --git a/matita/components/acic_content/content.mli b/matita/components/content/content.mli similarity index 100% rename from matita/components/acic_content/content.mli rename to matita/components/content/content.mli diff --git a/matita/components/acic_content/termAcicContent.ml b/matita/components/content/interpretations.ml similarity index 100% rename from matita/components/acic_content/termAcicContent.ml rename to matita/components/content/interpretations.ml diff --git a/matita/components/acic_content/termAcicContent.mli b/matita/components/content/interpretations.mli similarity index 98% rename from matita/components/acic_content/termAcicContent.mli rename to matita/components/content/interpretations.mli index f7ac8ccc6..259a7b1ac 100644 --- a/matita/components/acic_content/termAcicContent.mli +++ b/matita/components/content/interpretations.mli @@ -51,7 +51,7 @@ val get_all_interpretations: unit -> (interpretation_id * string) list val get_active_interpretations: unit -> interpretation_id list val set_active_interpretations: interpretation_id list -> unit - (** {2 content -> acic} *) + (** {2 content -> cic} *) (** @param env environment from argument_pattern to cic terms * @param pat cic_appl_pattern *) diff --git a/matita/components/lexicon/cicNotation.ml b/matita/components/lexicon/cicNotation.ml index ebc9463ee..7351596fa 100644 --- a/matita/components/lexicon/cicNotation.ml +++ b/matita/components/lexicon/cicNotation.ml @@ -29,7 +29,7 @@ open LexiconAst type notation_id = | RuleId of CicNotationParser.rule_id - | InterpretationId of TermAcicContent.interpretation_id + | InterpretationId of Interpretations.interpretation_id | PrettyPrinterId of TermContentPres.pretty_printer_id let compare_notation_id x y = @@ -77,7 +77,7 @@ let process_notation st = in !rule_id @ pp_id | Interpretation (loc, dsc, l2, l3) -> - let interp_id = TermAcicContent.add_interpretation dsc l2 l3 in + let interp_id = Interpretations.add_interpretation dsc l2 l3 in [InterpretationId interp_id] | st -> [] @@ -90,17 +90,17 @@ let remove_notation = function RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id) !parser_ref_counter item | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id - | InterpretationId id -> TermAcicContent.remove_interpretation id + | InterpretationId id -> Interpretations.remove_interpretation id let get_all_notations () = List.map (fun (interp_id, dsc) -> InterpretationId interp_id, "interpretation: " ^ dsc) - (TermAcicContent.get_all_interpretations ()) + (Interpretations.get_all_interpretations ()) let get_active_notations () = List.map (fun id -> InterpretationId id) - (TermAcicContent.get_active_interpretations ()) + (Interpretations.get_active_interpretations ()) let set_active_notations ids = let interp_ids = @@ -108,7 +108,7 @@ let set_active_notations ids = (function InterpretationId interp_id -> Some interp_id | _ -> None) ids in - TermAcicContent.set_active_interpretations interp_ids + Interpretations.set_active_interpretations interp_ids let history = ref [];; @@ -117,13 +117,13 @@ let push () = parser_ref_counter := initial_parser_ref_counter (); rule_ids_to_items := initial_rule_ids_to_items (); TermContentPres.push (); - TermAcicContent.push (); + Interpretations.push (); CicNotationParser.push () ;; let pop () = TermContentPres.pop (); - TermAcicContent.pop (); + Interpretations.pop (); CicNotationParser.pop (); match !history with | [] -> assert false diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml index 26d7e98fb..b8d474cc2 100644 --- a/matita/components/ng_cic_content/nTermCicContent.ml +++ b/matita/components/ng_cic_content/nTermCicContent.ml @@ -322,7 +322,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = in let _, symbol, args, _ = try - TermAcicContent.find_level2_patterns32 pid + Interpretations.find_level2_patterns32 pid with Not_found -> assert false in let ast = instantiate32 idrefs env symbol args in @@ -335,8 +335,8 @@ let load_patterns32 t = in set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t)) in - TermAcicContent.add_load_patterns32 load_patterns32; - TermAcicContent.init () + Interpretations.add_load_patterns32 load_patterns32; + Interpretations.init () ;; (* diff --git a/matita/components/ng_disambiguation/disambiguateChoices.ml b/matita/components/ng_disambiguation/disambiguateChoices.ml index 6d4d63b70..3da5f9baa 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.ml +++ b/matita/components/ng_disambiguation/disambiguateChoices.ml @@ -74,7 +74,7 @@ let mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl "The notation " ^ dsc ^ " expects more arguments"))) in let combined = - TermAcicContent.instantiate_appl_pattern + Interpretations.instantiate_appl_pattern ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env' appl_pattern in match rest with @@ -82,11 +82,11 @@ let mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl | _::_ -> mk_appl (combined::rest)) let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref symbol dsc = - let interpretations = TermAcicContent.lookup_interpretations ~sorted:false symbol in + let interpretations = Interpretations.lookup_interpretations ~sorted:false symbol in try mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (List.find (fun (dsc', _, _) -> dsc = dsc') interpretations) - with TermAcicContent.Interpretation_not_found | Not_found -> + with Interpretations.Interpretation_not_found | Not_found -> raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc))) let cic_lookup_symbol_by_dsc = lookup_symbol_by_dsc -- 2.39.2