]> matita.cs.unibo.it Git - helm.git/commit
Eureka!
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 23 Jan 2004 17:45:29 +0000 (17:45 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 23 Jan 2004 17:45:29 +0000 (17:45 +0000)
commit63f211d673ba5a9eb05b0bdad2585e2b251f2baa
tree331b9e62226daecc8a55ff9b94bffe38a5adb781
parent7dbfe197294523c1178dc4f3a126602fa48fbb00
Eureka!
It is now possible to choose independently:

 - the widget for the term editor
 - the disambiguating parser, i.e.
   * the parsing component
   * the disambiguating component
helm/gTopLevel/.depend
helm/gTopLevel/Makefile
helm/gTopLevel/chosenTermEditor.ml
helm/gTopLevel/disambiguatingParser.ml
helm/gTopLevel/oldDisambiguate.ml
helm/gTopLevel/oldDisambiguate.mli
helm/gTopLevel/texTermEditor.ml
helm/gTopLevel/texTermEditor.mli