Limited hilite markup (in Isabelle)

[Makarius]

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.

[David Aspinall]

This turns out to be due to `jit-lock-chunk-size' which defaults to 500 characters. I've raised this to 2000 characters for the Isar output buffers now, but regions with longer matches than that will still defeat it. Of course we could just disable jit-lock for output buffers but that might degrade performance. Better to use another mechanism for long highlighted regions. Or avoid them altogether.