Custom Query (361 matches)

When printing text with "hilite" markup the outcome appears to depend on the complexity of the body.

For example:

lemmas rules = sym refl trans sym refl trans sym refl trans sym refl trans sym refl trans

ML_command {* Pretty.writeln (Pretty.markup Markup.hilite
  [ProofContext.pretty_fact @{context} ("foo", @{thms rules(1-10)})]) *}

This works, but printing rules(1-11) produces funny \^A0...\^A1, although the body is still printed correctly, with markup.

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?

There is an odd link on http://proofgeneral.inf.ed.ac.uk/devel --- the hyperlink of "Visit the PG trac" points to the home page instead of http://proofgeneral.inf.ed.ac.uk/trac