aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_RoutedMessageViews.ml
Commit message (Collapse)AuthorAge
* coqide: queries from the query window are routed there (fix #5684)Gravatar Enrico Tassi2018-03-08
We systematically use Wg_MessageView for both the message panel and each Query tab; we register all MessageView in a RoutedMessageViews where the default route (0) is the message panel. Queries from the Query panel pick a non zero route to have their feedback message delivered to their MessageView