As people type in the proof <input>s, their text gets prettified to unicode.
The way this happens is ugly. We run the input through Formula.desugar, which does the prettification, and then send a SetFormulaAt update message. As part of the interpretation of this message, we use a helper function reup to find the <input> by its ID and change its value to the prettified text, without moving the caret.
We can't just rely on value :: Text -> Attribute because that would fuck up the caret.
However, Mason has pointed out that on "input" is effectual, so we can perform this entire reup business within an input handler!
As people type in the proof
<input>s, their text gets prettified to unicode.The way this happens is ugly. We run the input through
Formula.desugar, which does the prettification, and then send aSetFormulaAtupdate message. As part of the interpretation of this message, we use a helper functionreupto find the<input>by its ID and change its value to the prettified text, without moving the caret.We can't just rely on
value :: Text -> Attributebecause that would fuck up the caret.However, Mason has pointed out that
on "input"is effectual, so we can perform this entirereupbusiness within an input handler!