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
