dependencies between statuses simplified

diff --git a/matita/components/lexicon/lexiconTypes.ml b/matita/components/lexicon/lexiconTypes.ml
index 3aa2dadab344a166da168bcadc81bf39e1defd8a..4f57cbfc3a9a6033ef9aafa4f3565c04629b7578 100644 (file)
--- 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 b94aa076fbb42046bc4ffa4765c24aee263643af..0ffd78bacb196faad7d37c2e715513b2b3fe8244 100644 (file)
--- 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 2e9c9e3ddfbc3594956ca01582b5cb0409d810fe..18fe97ab43cc418e122c3ff9708203e5ac4bc60c 100644 (file)
--- 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 442a7eb3c998a20aefac1fe0baeceff3babc3d40..da250c912926f0491086a8556b477664e7251ba0 100644 (file)
--- 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 4b95e5370013d4a063adbafee34a9fca580a388b..d5c99447d6ddfb55444478ba99a4fa37f5fd0cf7 100644 (file)
--- 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 ddd08caf635a113203a4ff071c0fe7fc5cf2582c..f7c9a7b9fa2b82699d81ae86c5a770b12737191b 100644 (file)
--- 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 4b7b376b417933ad23d3e3f76cf47792e571f303..280ade3ee11ac559fa3494d0fe2e4d81175a8bb8 100644 (file)
--- 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