Opened 15 years ago
Closed 15 years ago
#267 closed defect (fixed)
Isabelle sendback markup dysfunctional
Reported by: | Makarius | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-4.0 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
The "sendback" markup in Isabelle no longer works.
For example:
ML_command {* writeln (Markup.markup Markup.sendback "oops") *}
produces literal
\^AWoops\^AX
What happened to pbp?
Note: See
TracTickets for help on using
tickets.
Fixed now: the "send back" feature has been restored based on font lock markup with a non-nil @code{sendback} property. This is more general than before and should work with multiple commands on a line. It could also be easily extended to use hidden commands (i.e. text in buffer is different to command sent).
The rest of PBP is not enabled: output markup has been radically simplified in PG 4 so this can be redesigned.