]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 06edf68) | patch
BIG BUG FIXED (???): in place of using Grammar.Entry.parse we should have
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 10 Dec 2010 22:30:55 +0000 (22:30 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 10 Dec 2010 22:30:55 +0000 (22:30 +0000)
commit5e924927db28c0a5bbbaa4e56515d9afe0b1360f
tree58876aab5eb3f69c835bf32a4267bc80c9aa2d66tree | snapshot
parent06edf68934062515225fb241e1cfb94d7d10208fcommit | diff
BIG BUG FIXED (???): in place of using Grammar.Entry.parse we should have
used from the beginning Grammar.Entry.parse_parsable in order to avoid token
loss (because of backtracking) between consecutive reads. I have fixed the issue
for statements only (since they are the one that show the problem). Should I
do the same everywhere?
matita/components/grafite_parser/grafiteParser.ml diff | blob | history
matita/components/grafite_parser/grafiteParser.mli diff | blob | history
matita/matita/matitaEngine.ml diff | blob | history
matita/matita/matitaEngine.mli diff | blob | history
matita/matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.