Copying alphabets, deleting symbols from alphabets.

[jurajsic]

Currently, it is not possible to copy alphabets, is there a reason for that? We cannot even delete symbols from alphabets, so if I create an alphabet variable, I cannot change it other than by adding symbols to it.

[Adda0]

Yeah, there is: I never got around to finishing refactoring the alphabets, as we discussed way back, which was supposed to improve working with alphabets in all of these aspects. If we need this now, we can at least add these simple features to alphabets so that they are at least usable for our current use case. What is it that we require currently?

• copying whole alphabets,
• deleting symbols.

Anything else?

[jurajsic]

It's not needed that significantly, I can work around it. If you do it, I would also add clear(), for OnTheFlyAlphabet.

[Adda0]

These are all micro-modifications. I will implement them quickly in the following days.