[isabelle-dev] Remaining uses of Proof General?

[Lars Noschinski]

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