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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to