From f5065f33e0689753c3f2744928b96851ca77ca8d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 4 Nov 2010 20:39:17 +0000
Subject: [PATCH] - dependencies between statuses simplified

---
 .../grafite_parser/grafiteDisambiguate.ml     |  4 +--
 .../grafite_parser/grafiteDisambiguate.mli    | 17 ++----------
 matita/components/ng_tactics/nTacStatus.ml    |  4 +--
 matita/components/ng_tactics/nTacStatus.mli   |  4 +--
 matita/components/statuses.txt                | 26 +++++++++++--------
 5 files changed, 22 insertions(+), 33 deletions(-)

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index 58a241e3f..7511e02aa 100644
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -28,16 +28,14 @@
 class type g_status =
   object
    inherit LexiconTypes.g_status
-   inherit NCicCoercion.g_status
   end
 
 class status =
  object (self)
   inherit LexiconTypes.status
-  inherit NCicCoercion.status
   method set_grafite_disambiguate_status
    : 'status. #g_status as 'status -> 'self
-      = fun o -> (self#set_lexicon_engine_status o)#set_coercion_status o
+      = fun o -> (self#set_lexicon_engine_status o)
  end
 
 exception BaseUriNotSetYet
diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index 0074b2916..6caf5301f 100644
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -25,28 +25,15 @@
 
 exception BaseUriNotSetYet
 
-class type g_status =
- object
-  inherit LexiconTypes.g_status
-  inherit NCicCoercion.g_status
- end
-
-class status :
- object ('self)
-  inherit LexiconTypes.status
-  inherit NCicCoercion.status
-  method set_grafite_disambiguate_status: #g_status -> 'self
- end
-
 val disambiguate_nterm :
  NCic.term option -> 
- (#status as 'status) ->
+ (#LexiconTypes.status as 'status) ->
  NCic.context -> NCic.metasenv -> NCic.substitution ->
  NotationPt.term Disambiguate.disambiguator_input ->
    NCic.metasenv * NCic.substitution * 'status * NCic.term
 
 val disambiguate_nobj :
- #status as 'status ->
+ #LexiconTypes.status as 'status ->
  ?baseuri:string ->
  (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
   'status * NCic.obj
diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index 9504e64ba..fbcdccb31 100644
--- a/matita/components/ng_tactics/nTacStatus.ml
+++ b/matita/components/ng_tactics/nTacStatus.ml
@@ -66,7 +66,7 @@ class auto_status =
 
 class type g_pstatus =
  object
-  inherit GrafiteDisambiguate.g_status
+  inherit LexiconTypes.g_status
   inherit g_auto_status
   inherit g_eq_status
   method obj: NCic.obj
@@ -75,7 +75,7 @@ class type g_pstatus =
 class pstatus =
  fun (o: NCic.obj) ->
  object (self)
-   inherit GrafiteDisambiguate.status
+   inherit LexiconTypes.status
    inherit auto_status
    inherit eq_status
    val obj = o
diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index cfb7123bb..ddaf9da80 100644
--- a/matita/components/ng_tactics/nTacStatus.mli
+++ b/matita/components/ng_tactics/nTacStatus.mli
@@ -43,7 +43,7 @@ class auto_status :
 
 class type g_pstatus =
  object
-  inherit GrafiteDisambiguate.g_status
+  inherit LexiconTypes.g_status
   inherit g_auto_status
   inherit g_eq_status
   method obj: NCic.obj
@@ -52,7 +52,7 @@ class type g_pstatus =
 class pstatus :
  NCic.obj ->
   object ('self)
-   inherit GrafiteDisambiguate.status
+   inherit LexiconTypes.status
    inherit auto_status
    inherit eq_status
    method obj: NCic.obj
diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt
index 104a90938..d4fb967b7 100644
--- a/matita/components/statuses.txt
+++ b/matita/components/statuses.txt
@@ -1,16 +1,20 @@
-grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon+nciccoercion)
-           |--> dumpable                                    |             |
-           |--> nciclibrary                                 |       unif_hint
-           |--> grafiteparser -> lexicon -> ...             |
-                                                            |-> interpretation
-                                                            |-> termcontentpres
-                                                            |-> notation_parser
-
+grafitetypes
+ |--> dumpable
+ |--> nciclibrary
+ |--> grafiteparser -----
+ |--> tac               |
+       |--> auto        |
+       |--> eq          |
+       |-------------> lexicon
+                        |--> notation_parser
+                        |--> interpretation
+                        |       |--> nciccoercion --> unif_hint
+                        |--> termcontentpres
 
 applytransformation
     |
-    |-> ntermciccontent = nciccoercion+interpretation
-    |                       |
-    |                    unif_hint
+    |-> interpretation -> nciccoercion
+    |                         |
+    |                     unif_hint
     |
     |-> termcontentpres
-- 
2.39.2