Odd unicode abbreviations, notably |>

[makarius]

In isar-symbol-shortcuts there are some odd abbreviations, notably |> which is very common in Isabelle/ML, but its expansion \<triangleright> is very rare.

Anyway, how can the user prevent unwanted expansion? In X-Symbol mode, plain editor undo would revert to the original, but now it just reverst to the ASCII form of the replaced symbol. Of course, editor quote *before* editing works, but is a bit cumbersome.

[da]

From a grep of the sources, |> seems to only be used inside ML code, and there should be different input methods engaged in that context, ideally. Anyway, I have removed it again now.

The behaviour of undo is very odd!

I don't know of a quick way to revert to the ASCII sequence that you typed, but you can use C-\ (control backquote) to enable/disable the tokens input method temporarily. This could do with some hints in the documentation, so I'll leave this open until added.

[da]

Moved to #290.