From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 4 Nov 2010 21:05:56 +0000 (+0000)
Subject: dependencies between statuses simplified
X-Git-Tag: make_still_working~2730
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=16250ed29f9200595694cd49dfc1aed76280dcb9;p=helm.git

dependencies between statuses simplified
---

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