]> matita.cs.unibo.it Git - helm.git/commit - helm/matita/matitaInit.ml
1. Several files in grafite that should be in grafite_parser moved there.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Dec 2005 14:09:29 +0000 (14:09 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Dec 2005 14:09:29 +0000 (14:09 +0000)
commit7b995596c8b11be95c430646227d01928cc71219
tree9d9accd10dc0d2fc495771d9ba7953b4fa0bfa5a
parent6b38b8f5c675570ca5a70e917cf77c783ef2d092
1. Several files in grafite that should be in grafite_parser moved there.
2. grafiteEngine is now generalized over the function baseuri_of_script
   (that associates the baseuri to a .ma file). This function is used to
   execute the Include statement. However, it seems to me that this shows
   a problem in the architecture (since the only possible implementation of
   the function involves using the grafie_parser right now).

Modified Files in ocaml:
        METAS/meta.helm-grafite_parser.src grafite/.depend
        grafite/Makefile grafite/cicNotation.ml
        grafite/cicNotation.mli grafite2/disambiguatePp.ml
        grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml
        grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml
        grafite2/grafiteMisc.mli grafite_parser/.depend
        grafite_parser/Makefile
Modified Files in matita:
        matitaEngine.ml matitaEngine.mli matitaGui.ml matitaInit.ml
        matitaScript.ml matitacLib.ml matitaclean.ml matitadep.ml
Added Files in ocaml:
        grafite_parser/cicNotation2.ml grafite_parser/cicNotation2.mli
        grafite_parser/grafiteParser.ml
        grafite_parser/grafiteParser.mli
        grafite_parser/grafiteParserMisc.ml
        grafite_parser/grafiteParserMisc.mli
        grafite_parser/print_grammar.ml grafite_parser/test_dep.ml
        grafite_parser/test_parser.ml
Removed Files in ocaml:
        grafite/grafiteParser.ml grafite/grafiteParser.mli
        grafite/print_grammar.ml grafite/test_dep.ml
        grafite/test_parser.ml
helm/matita/matitaEngine.ml
helm/matita/matitaEngine.mli
helm/matita/matitaGui.ml
helm/matita/matitaInit.ml
helm/matita/matitaScript.ml
helm/matita/matitacLib.ml
helm/matita/matitaclean.ml
helm/matita/matitadep.ml