Opened 15 years ago
Closed 15 years ago
#271 closed defect (fixed)
Special characters in Isabelle identifiers missing?
Reported by: | Makarius | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-4.0 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
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.
Change History (2)
comment:1 Changed 15 years ago by
Status: | new → accepted |
---|
comment:2 Changed 15 years ago by
Resolution: | → fixed |
---|---|
Status: | accepted → closed |
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!
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?