I'm not seeing this when using @nosent from a new Leo file, so it's probably nothing ...
This is really cool. It furthers the 'Domain Specific Editor' notion of customizing a Leo file to match development requirements of a framework. With the new @nosent, one Leo file can be downloaded and when saved, create the required external files defined by @nosent nodes. In the spirit of http://devassistant.org/ On Fri, Feb 6, 2015 at 3:12 PM, Kent Tenney <[email protected]> wrote: > I'm seeing this with current trunk > > create node > @nosent /tmp/txt > > rclick 'Refresh from disk' > body is empty > > create node > @edit /tmp/txt > rclick 'Refresh from disk' > body is loaded > > change @edit above to @nosent > make changes to /tmp/txt outside Leo > rclick 'Refresh from disk' > outside changes are reflected in body > > On Fri, Feb 6, 2015 at 2:56 PM, Edward K. Ream <[email protected]> wrote: >> >> On Fri, Feb 6, 2015 at 11:15 AM, Matt Wilkie <[email protected]> wrote: >>> >>> >>> Question: what happens to undo history when a @nosent file is changed >>> externally changed and reloaded? >> >> >> Nothing, until now: refresh-from-disk did not support @nosent. >> >> As of rev 86ff908, refresh-from-disk supports @nosent and also shows the >> "Recovered Nodes" tree indicating what nodes were changed. >> >> The refresh-from-disk command has never altered the undo history, which >> surely is wrong. However, nobody has noticed this until now. What should >> happen is that refresh-from-disk should be undoable. I've put it on the >> list. >> >> Edward >> >> -- >> You received this message because you are subscribed to the Google Groups >> "leo-editor" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To post to this group, send email to [email protected]. >> Visit this group at http://groups.google.com/group/leo-editor. >> For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/leo-editor. For more options, visit https://groups.google.com/d/optout.
