]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c6b9538) | patch
Better handling of queries. Now both the locate and backward queries give
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 27 Sep 2002 16:59:23 +0000 (16:59 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 27 Sep 2002 16:59:23 +0000 (16:59 +0000)
commit2cad6cb43cd5ca2c2d371cc49a6354c95533c81f
tree9b9dad95fe8ff666e26f9f68b6f899410474ebe5tree | snapshot
parentc6b9538995874c6595874e88bc7bf8965e50f14bcommit | diff
Better handling of queries. Now both the locate and backward queries give
the user the possibility to disambiguate the answer, and write it in the
input window. Some bugs in the disambiguation process have been fixed.
Finally the output of the query process in the outputhtml window is now
much more verbose.
helm/gTopLevel/gTopLevel.ml diff | blob | history
helm/gTopLevel/mQueryGenerator.ml diff | blob | history
helm/gTopLevel/mQueryGenerator.mli diff | blob | history
helm/gTopLevel/topLevel/topLevel.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.