[Texmacs-dev] Applied patches

[Joris van der Hoeven]

Some further news on David's patches:

850, 851, 853, 854: Applied.
  Good idea; maybe that the layout can still be improved.
  Notice that button-widget-2 seems to get useless.
856: Rejected.
  This is an instance where we need contextual translation.
  Initially, I did as you said, but this is incorrect in
  other contexts (I don't remember which). This will be fixed
  as soon as I implement tree-based translations.
859, 860: Postponed.
  As you say yourself, we need a widget for choosing colors.
861: Applied.
862: Applied.

More later.