Unicode translator does not add space between identifier ending with non-letter and operator starting with letter

Description

When trying to load the third refinement of
git@github.com:heinzware/EventBPacman-Plugin.git ( https://github.com/heinzware/EventBPacman-Plugin/tree/master/eventb) Pacman_Machine_3.bum
ProB2 raises the following exception:

Environment

None

Status

Assignee

dgelessus

Reporter

Michael Leuschel

Priority

Major
Configure