Hey Colomban,
[...]
0001-Per-document-real-time-symbols-setting.patch: Adds a per-document setting for real-time updates and a menu item in the Document menu. There is still a FIXME in it, feel free to give ideas :)
This looks like a good idea.
For the fixme, It shouldn't apply per document settings here, they are not in the prefs so they won't have changed. Just leave it out.
0002-Tell-the-user-if-real-time-reparsing-is-slow-and-let.patch: This one adds the check for the updating duration and asks the user. It is WIP, and I'm not really convinced by the dialog, as you can read in a TODO. Apart that, it seems to work pretty OK.
Havn't had time to look at this, but as I said its a last resort.
Both misses docs, up to come when they are ready.
So, I'm soliciting your impressions, opinions, remarks, etc. Also, is this whole thing important enough to break string freeze less than a week before release? (read: to have some strings untranslated)
I'm not Nick, but I would suggest leaving it until after release, thats not far away, and then as soon as it is committed Nick will have built a new version :)
Cheers Lex