[isabelle-dev] Remaining uses of Proof General?

Lars Noschinski noschinl at in.tum.de
Sat Jun 28 08:01:36 CEST 2014

On 27.06.2014 23:47, Makarius wrote:
> Just a side remark: in the repository version we are talking about,
> and thus the coming release, ML in auxiliary files works smoothly and
> often better than the ML blocks, because the file gets its own ML mode.
For ML files, I occasionally had the problem that hovering would not
work. It usually recovered after some time. I haven't been able to pin
it down to a certain situation yet. The file in question has around
400-500 lines. I /think/, this refers to d3d91422f4 (haven't worked
enough with later revisions yet).

It might be coincidence, but I haven't encountered this behaviour with
ML blocks yet.

  -- Lars

More information about the isabelle-dev mailing list