search

MathHubInfo / Frontend

A new MathHub Narration Frontend written in React.
GNU Affero General Public License v3.0
2 stars 0 forks source link

Isabelle constant names with HTML are not rendered correctly. #129

Open kohlhase opened 3 years ago

kohlhase commented 3 years ago

In https://beta.mathhub.info/library/document/aHR0cHM6Ly9pc2FiZWxsZS5pbi50dW0uZGUvQVZMLVRyZWVzL0FWTDIub21kb2M%3D?modules=https%3A%2F%2Fisabelle.in.tum.de%3FAVL-Trees.AVL2&declarations=https%3A%2F%2Fisabelle.in.tum.de%2F%3FAVL-Trees.AVL2%3FAVL2.raw_sum.tree%5C%3C%5Esub%3E0.sum.Sum_Type.map_raw_sum%7Cconst we see funnily rendered constant names.

Screenshot 2021-03-26 at 15 07 04
tkw1536 commented 3 years ago

This is a problem related to MMT not presenting correctly and very little I can do about it here.

kohlhase commented 3 years ago

To me it seems that you are treating the constant names as strings and not as html, see all the <sub>.

kohlhase commented 3 years ago

or it is excaped once too many.

tkw1536 commented 3 years ago

OK, I will have to investigate in more detail later.