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?

Change History (1)

comment:1 Changed 15 years ago by David Aspinall

Resolution: fixed
Status: newclosed

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.

Note: See TracTickets for help on using tickets.