You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The issue is that currently, we tried to support both blocks of invariants and individual invariants. When we modified the semantic model (e.g., via quick fix), the context return for invariants is individual invariants, hence the described problem. There are two possible fixes for this.
Drop the support for blocks of invariants
Distinguish between block invariants and individual invariants, i.e., using different EMF types and using the translation to normal invariants during serialisation.
When converting plain text to Rodin keyboard symbols using the contextual helper, it puts "invariant" keyword at the end of the preceding line
![image](https://user-images.githubusercontent.com/1729886/228796523-cafbc6ec-1226-489a-a0c2-c5b696bc2493.png)
![image](https://user-images.githubusercontent.com/1729886/228796683-9be39ae3-9f74-484e-b107-fca683a6406d.png)
The text was updated successfully, but these errors were encountered: