]> matita.cs.unibo.it Git - helm.git/commitdiff
dependencies between statuses simplified
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 4 Nov 2010 21:00:26 +0000 (21:00 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 4 Nov 2010 21:00:26 +0000 (21:00 +0000)
matita/components/grafite_parser/grafiteParser.ml
matita/components/grafite_parser/grafiteParser.mli
matita/components/statuses.txt

index 9485190867edd74a55b8689049550f20424371aa..5b092a6d310fc2dc3641374cc026a2a73118d194 100644 (file)
@@ -630,19 +630,19 @@ type db = ast_statement localized_option Grammar.Entry.e ;;
 
 class type g_status =
  object
-  inherit LexiconTypes.g_status
+  inherit CicNotationParser.g_status
   method parser_db: db
  end
 
 class status =
  object(self)
-  inherit LexiconTypes.status as super
+  inherit CicNotationParser.status ~keywords:[]
   val mutable db = None
   method parser_db = match db with None -> assert false | Some x -> x
   method set_parser_db v = {< db = Some v >}
   method set_parser_status
    : 'status. #g_status as 'status -> 'self
-   = fun o -> {< db = Some o#parser_db >}#set_lexicon_engine_status o
+   = fun o -> {< db = Some o#parser_db >}#set_notation_parser_status o
   initializer
    let grammar = CicNotationParser.level2_ast_grammar self in
    db <- Some (mk_parser (Grammar.Entry.create grammar "statement") self)
index 11fbccaed53b286e4c5363375be058a8c2c330b8..451c17c68aa99b8e02d6e8b281aa2238f7aebe26 100644 (file)
@@ -33,13 +33,13 @@ type db
 
 class type g_status =
  object
-  inherit LexiconTypes.g_status
+  inherit CicNotationParser.g_status
   method parser_db: db
  end
 
 class status :
  object('self)
-  inherit LexiconTypes.status
+  inherit CicNotationParser.status
   method parser_db : db
   method set_parser_db : db -> 'self
   method set_parser_status : 'status. #g_status as 'status -> 'self
index d4fb967b7be6c46b5acec12213c891abdcf48661..2e9c9e3ddfbc3594956ca01582b5cb0409d810fe 100644 (file)
@@ -1,15 +1,15 @@
 grafitetypes
  |--> dumpable
  |--> nciclibrary
- |--> grafiteparser -----
- |--> tac               |
-       |--> auto        |
-       |--> eq          |
-       |-------------> lexicon
-                        |--> notation_parser
-                        |--> interpretation
-                        |       |--> nciccoercion --> unif_hint
-                        |--> termcontentpres
+ |--> grafiteparser --> notation_parser
+ |--> tac                
+       |--> auto         
+       |--> eq           
+       |--> lexicon
+             |--> notation_parser
+             |--> interpretation
+             |       |--> nciccoercion --> unif_hint
+             |--> termcontentpres
 
 applytransformation
     |