]> matita.cs.unibo.it Git - helm.git/commit - helm/ocaml/METAS/meta.helm-grafite_parser.src
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:31 +0000 (14:09 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Dec 2005 14:09:31 +0000 (14:09 +0000)
commita696aae5ea794cd43fd3d83d37a0345d2a1387b3
tree7b18192a8e92ee479e78e9a8b2f48fbb476569f6
parent7b995596c8b11be95c430646227d01928cc71219
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
27 files changed:
helm/ocaml/METAS/meta.helm-grafite_parser.src
helm/ocaml/grafite/.depend
helm/ocaml/grafite/Makefile
helm/ocaml/grafite/cicNotation.ml
helm/ocaml/grafite/cicNotation.mli
helm/ocaml/grafite/grafiteParser.ml [deleted file]
helm/ocaml/grafite/grafiteParser.mli [deleted file]
helm/ocaml/grafite/print_grammar.ml [deleted file]
helm/ocaml/grafite/test_dep.ml [deleted file]
helm/ocaml/grafite/test_parser.ml [deleted file]
helm/ocaml/grafite2/disambiguatePp.ml
helm/ocaml/grafite2/disambiguatePp.mli
helm/ocaml/grafite2/grafiteEngine.ml
helm/ocaml/grafite2/grafiteEngine.mli
helm/ocaml/grafite2/grafiteMisc.ml
helm/ocaml/grafite2/grafiteMisc.mli
helm/ocaml/grafite_parser/.depend
helm/ocaml/grafite_parser/Makefile
helm/ocaml/grafite_parser/cicNotation2.ml [new file with mode: 0644]
helm/ocaml/grafite_parser/cicNotation2.mli [new file with mode: 0644]
helm/ocaml/grafite_parser/grafiteParser.ml [new file with mode: 0644]
helm/ocaml/grafite_parser/grafiteParser.mli [new file with mode: 0644]
helm/ocaml/grafite_parser/grafiteParserMisc.ml [new file with mode: 0644]
helm/ocaml/grafite_parser/grafiteParserMisc.mli [new file with mode: 0644]
helm/ocaml/grafite_parser/print_grammar.ml [new file with mode: 0644]
helm/ocaml/grafite_parser/test_dep.ml [new file with mode: 0644]
helm/ocaml/grafite_parser/test_parser.ml [new file with mode: 0644]