]> matita.cs.unibo.it Git - helm.git/commit
- added callbacks parameters to hbugsClient constructor (on_exit,
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 19 Feb 2003 13:59:06 +0000 (13:59 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 19 Feb 2003 13:59:06 +0000 (13:59 +0000)
commit594ea125d8bdd2c0a210e4b2170b0c725075d597
treea85ed420b7fa69f1cc0a4552d35e863879f0aedb
parentf8ba6a6b7c0798258db3db5fe12413c8e8e1cb12
- added callbacks parameters to hbugsClient constructor (on_exit,
  on_use_hint)
- hid methods used to handle local http daemon
- added and exposed methods registerToBroker, unregisterFromBroker,
  subscribeAll
- removed useHint, hint are returned on request by "hint" new method
- remeber availableTutors from last List_tutor message and use them to
  show tutors name instead of tutor id in main window
- handle double click on hint name to use an hint
- added wait parameter sendReq method to be able to wait the answer of
  a request
- added support for multiple hints received from broker
- clear old hints on state change
- subscribe to all available tutors on creation
- added subscribeSelected method
helm/hbugs/client/hbugs_client.ml
helm/hbugs/client/hbugs_client.mli