Opened 15 years ago
Closed 15 years ago
#263 closed defect (fixed)
proof-shell-trace-output-regexp in trace output
Reported by: | Makarius | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-4.0 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
proof-shell-trace-output-regexp appears visually in the *trace*
buffer.
For example (in Isabelle):
ML_command {* tracing "foo" *}
Results in
\^AVfoo
Another example with extra term markup, which is displayed properly after the initial garbage:
ML_command {* tracing (Syntax.string_of_term_global @{theory} @{term "x == y"}) *}
Note: See
TracTickets for help on using
tickets.
Works after adding special "V" to invisible parts of
isar-output-font-lock-keywords-1
.