On Mac, some of the symbols do not display properly in the symbols panel (see attachment)
(This is reported by Michael Butler via private communication).
Hi Laurent,
The Brave Sans Mono font is loaded by the Event-B UI plug-in. If the Symbols view is activated before the Event-B UI plug-in, the font will not be available. In fact, once the Event-B UI is activated, close the Symbols view and reopen it again will help to display the symbols correctly.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
On Windows, the same problem occurs, however, resizing the view (which force a refresh) and the correct font is used.
I debug the problem and it is the case that the Event-B UI plug-in is started before the Symbols View (as it is a dependency). However, the loadFont() method in EventBUIPlugin load the font asynchronously, i.e., using display.asyncExec(...). Changing this to display.syncExec(....) fixes the problem on Mac for me.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Dear Son, it is on purpose that the font loading is done asynchronously. Making it synchronous would break again the UI tests by introducing deadlocks.
I think you should rather postpone the display of the symbols after the font has been loaded asynchronously.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Dear Son, I have a developed a fix for this issue.
It is available in branch bug-763 of my fork of RodinCore (git://git.code.sf.net/u/lvoisin/rodincore).
Could you please review it and check that it works on Mac OS Sierra and the other platforms (I have only tested it on my computer which is El Capitan)?
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Dear Laurent,
Thank you very much. The changes look reasonable to me. We have checked Mac OS Sierra, Window 32bit and Ubuntu 64bit and the problem is gone.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
The symbols that are not properly displayed correspond to those that are taken in the private subset of Unicode (Event-B specific).
On my machine, these symbols are properly displayed. I suppose that it is because I have the Event-B font installed globally on my Mac.
Normally the Event-B font is locally installed by the Rodin platform if it is not yet available. It seems that the symbol table does not use it, then.
Hi Laurent,
The Brave Sans Mono font is loaded by the Event-B UI plug-in. If the Symbols view is activated before the Event-B UI plug-in, the font will not be available. In fact, once the Event-B UI is activated, close the Symbols view and reopen it again will help to display the symbols correctly.
Some more information related to the problem:
I debug the problem and it is the case that the Event-B UI plug-in is started before the Symbols View (as it is a dependency). However, the loadFont() method in EventBUIPlugin load the font asynchronously, i.e., using display.asyncExec(...). Changing this to display.syncExec(....) fixes the problem on Mac for me.
Dear Son, it is on purpose that the font loading is done asynchronously. Making it synchronous would break again the UI tests by introducing deadlocks.
I think you should rather postpone the display of the symbols after the font has been loaded asynchronously.
Dear Son, I have a developed a fix for this issue.
It is available in branch bug-763 of my fork of RodinCore (git://git.code.sf.net/u/lvoisin/rodincore).
Could you please review it and check that it works on Mac OS Sierra and the other platforms (I have only tested it on my computer which is El Capitan)?
Dear Laurent,
Thank you very much. The changes look reasonable to me. We have checked Mac OS Sierra, Window 32bit and Ubuntu 64bit and the problem is gone.
Bug fixed in [8e82cb]
Related
Commit: [8e82cb]