Deduplicate artificial labels of Double-DOP binarization.

- Double-DOP binarization uses unique numeric IDs;
  however, given the same siblings and yield function, the same label
  is now re-used, which results in a smaller grammar (about 60% smaller)
  and hence a smaller grammar constant, resulting in faster parsing.
  Since the concatenation of sibling labels and the yield
  function can result in very long labels, these strings are again
  mapped to numeric IDs.
- Web interface:
  - pass parsing parameters (MPD, sampling, &c) properly.
  - cache for web interface evicts items after timeout.
  - enable logging
- Fix doctests which relied on dictionary order.