From 16250ed29f9200595694cd49dfc1aed76280dcb9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 4 Nov 2010 21:05:56 +0000 Subject: [PATCH] dependencies between statuses simplified --- matita/components/lexicon/lexiconTypes.ml | 4 +--- matita/components/lexicon/lexiconTypes.mli | 2 -- matita/components/statuses.txt | 12 +----------- matita/matita/applyTransformation.ml | 7 ------- matita/matita/applyTransformation.mli | 10 ++-------- matita/matita/matitaGuiTypes.mli | 6 +++--- matita/matita/matitaMathView.ml | 8 ++++---- 7 files changed, 11 insertions(+), 38 deletions(-) diff --git a/matita/components/lexicon/lexiconTypes.ml b/matita/components/lexicon/lexiconTypes.ml index 3aa2dadab..4f57cbfc3 100644 --- a/matita/components/lexicon/lexiconTypes.ml +++ b/matita/components/lexicon/lexiconTypes.ml @@ -41,7 +41,6 @@ class type g_status = object inherit Interpretations.g_status inherit TermContentPres.g_status - inherit CicNotationParser.g_status method lstatus: lexicon_status end @@ -49,10 +48,9 @@ class status = object(self) inherit Interpretations.status inherit TermContentPres.status - inherit CicNotationParser.status ~keywords:[] val lstatus = initial_status method lstatus = lstatus method set_lstatus v = {< lstatus = v >} method set_lexicon_engine_status : 'status. #g_status as 'status -> 'self - = fun o -> (((self#set_lstatus o#lstatus)#set_interp_status o)#set_content_pres_status o)#set_notation_parser_status o + = fun o -> ((self#set_lstatus o#lstatus)#set_interp_status o)#set_content_pres_status o end diff --git a/matita/components/lexicon/lexiconTypes.mli b/matita/components/lexicon/lexiconTypes.mli index b94aa076f..0ffd78bac 100644 --- a/matita/components/lexicon/lexiconTypes.mli +++ b/matita/components/lexicon/lexiconTypes.mli @@ -33,7 +33,6 @@ class type g_status = object inherit Interpretations.g_status inherit TermContentPres.g_status - inherit CicNotationParser.g_status method lstatus: lexicon_status end @@ -42,7 +41,6 @@ class status : inherit g_status inherit Interpretations.status inherit TermContentPres.status - inherit CicNotationParser.status method set_lstatus: lexicon_status -> 'self method set_lexicon_engine_status: #g_status -> 'self end diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt index 2e9c9e3dd..18fe97ab4 100644 --- a/matita/components/statuses.txt +++ b/matita/components/statuses.txt @@ -6,15 +6,5 @@ grafitetypes |--> auto |--> eq |--> lexicon - |--> notation_parser - |--> interpretation - | |--> nciccoercion --> unif_hint + |--> interpretation --> nciccoercion --> unif_hint |--> termcontentpres - -applytransformation - | - |-> interpretation -> nciccoercion - | | - | unif_hint - | - |-> termcontentpres diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml index 442a7eb3c..da250c912 100644 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@ -35,13 +35,6 @@ (* $Id$ *) -class status = - object - inherit Interpretations.status - inherit TermContentPres.status - end - - let mpres_document pres_box = Xml.add_xml_declaration (CicNotationPres.print_box pres_box) diff --git a/matita/matita/applyTransformation.mli b/matita/matita/applyTransformation.mli index 4b95e5370..d5c99447d 100644 --- a/matita/matita/applyTransformation.mli +++ b/matita/matita/applyTransformation.mli @@ -33,17 +33,11 @@ (* *) (***************************************************************************) -class status : - object ('self) - inherit Interpretations.status - inherit TermContentPres.status - end - val ntxt_of_cic_sequent: - map_unicode_to_tex:bool -> int -> #status -> + map_unicode_to_tex:bool -> int -> #LexiconTypes.status -> NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *) int * NCic.conjecture -> (* sequent *) string (* text *) val ntxt_of_cic_object: - map_unicode_to_tex:bool -> int -> #status -> NCic.obj -> string + map_unicode_to_tex:bool -> int -> #LexiconTypes.status -> NCic.obj -> string diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index ddd08caf6..f7c9a7b9f 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -131,9 +131,9 @@ object (** load a sequent and render it into parent widget *) method nload_sequent: - #ApplyTransformation.status -> NCic.metasenv -> NCic.substitution -> int -> unit + #LexiconTypes.status -> NCic.metasenv -> NCic.substitution -> int -> unit - method load_nobject: #ApplyTransformation.status -> NCic.obj -> unit + method load_nobject: #LexiconTypes.status -> NCic.obj -> unit end class type sequentsViewer = @@ -143,7 +143,7 @@ object method load_logo_with_qed: unit method nload_sequents: #NTacStatus.tac_status -> unit method goto_sequent: - #ApplyTransformation.status -> int -> unit (* to be called _after_ load_sequents *) + #LexiconTypes.status -> int -> unit (* to be called _after_ load_sequents *) method cicMathView: cicMathView end diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 4b7b376b4..280ade3ee 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -620,7 +620,7 @@ object (self) val mutable current_mathml = None method nload_sequent: - 'status. #ApplyTransformation.status as 'status -> NCic.metasenv -> + 'status. #LexiconTypes.status as 'status -> NCic.metasenv -> NCic.substitution -> int -> unit = fun status metasenv subst metano -> let sequent = List.assoc metano metasenv in @@ -637,7 +637,7 @@ object (self) self#load_root ~root:txt method load_nobject : - 'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit + 'status. #LexiconTypes.status as 'status -> NCic.obj -> unit = fun status obj -> let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false 80 status obj in @@ -808,7 +808,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#render_page status ~page ~goal_switch)) method private render_page: - 'status. #ApplyTransformation.status as 'status -> page:int -> + 'status. #LexiconTypes.status as 'status -> page:int -> goal_switch:Stack.switch -> unit = fun status ~page ~goal_switch -> (match goal_switch with @@ -825,7 +825,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = List.assoc goal_switch goal2win () with Not_found -> assert false) - method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit + method goto_sequent: 'status. #LexiconTypes.status as 'status -> int -> unit = fun status goal -> let goal_switch, page = try -- 2.39.2