]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0b42252) | patch
- Added DisambiguatingParser (that abstracts both the parser and the
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 23 Jan 2004 15:30:33 +0000 (15:30 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 23 Jan 2004 15:30:33 +0000 (15:30 +0000)
commit12809955a4a6c693072f5b924603165f83cc382e
treeb684c39e71922913693b2fc5cee79360eaa76203tree | snapshot
parent0b42252cabbfd9b0e5b132ad8f7c378fd2a9b29bcommit | diff
- Added DisambiguatingParser (that abstracts both the parser and the
  disambiguator used)
- Added ChosenTermEditor (used to swap quickly the editor used).
- moved disambiguate.ml* to oldDisambiguate.ml*
helm/gTopLevel/.depend diff | blob | history
helm/gTopLevel/Makefile diff | blob | history
helm/gTopLevel/chosenTermEditor.ml [new file with mode: 0644] blob
helm/gTopLevel/chosenTermEditor.mli [new file with mode: 0644] blob
helm/gTopLevel/disambiguatingParser.ml [new file with mode: 0644] blob
helm/gTopLevel/disambiguatingParser.mli [new file with mode: 0644] blob
helm/gTopLevel/gTopLevel.ml diff | blob | history
helm/gTopLevel/oldDisambiguate.ml [new file with mode: 0644] blob
helm/gTopLevel/oldDisambiguate.mli [new file with mode: 0644] blob
helm/gTopLevel/termEditor.ml diff | blob | history
helm/gTopLevel/termEditor.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.