Special characters in Isabelle identifiers missing?

[Makarius]

In prover output, the special characters ? and ' seem to be missing. For example:

lemma "A --> A" ..

In the response there is only "A" not "?A", as could be expected with show_question_marks := false.

Same effect for typ 'a --- only a named "a" is displayed.

Copy/paste works -- the characters show up in the source as expected.

[David Aspinall]

Hmm, odd. Must be caused by the regexps in isar-syntax.el. Those regexps matching identifiers are pretty hairy with nesting for identifier formats, do they need to be that complicated or could we just match anything inside the delimiters?

[David Aspinall]

OK, I've looked a bit more closely: this was actually an intentional/experimental change as these characters are arguably spurious when you can see in colour. So the display regexps may simply hide them now we use invisible characters in the presentation in GNU Emacs/PG4, rather than hacking the buffer contents.

Question marks can be disabled by the Isabelle printing option but not quotes.

Anyway, I have reverted to the old behaviour now for consistency and least surprise!