On Fri, Oct 14, 2011 at 11:07 AM, Edward K. Ream <edream...@gmail.com> wrote: > Following up on Kent's prizel. > > We could create a Leo repository now. > > In another post I discussed this possibility:: > > - @file x.leo > - @file y.leo > etc. > > This morning I realized we could have the same thing, just by defining > leo.leo something like this:: > > - Notes > - @file leoNotes.txt > - Core > < same as Code tree in leoPy.leo> > - Plugins > < contents of LeoPlugins.leo> > - Dist > @file leoDist.leo > - Docs > <contents of LeoDocs.leo> > > Or something like this. The point is that we don't need new invention > to create "grand unified Leo base." > > However, there is a real tension between one .leo file and many. > > Pluses of leo.leo: > > - easier global searches. > > Minuses of leo.leo: > > - all files *always* get loaded, so slower startup. > - Less separation, which can be dangerous. > - Less flexibility in loading, but maybe not so important. > > Your comments please. Would a single leo.leo be a good idea?
Sort of a top level Table of Contents with @bookmarks pointing at Leo files? I think that would be great, though persisting the open tabs would add lots of value: from leo.leo -> open tabs for files of interest -> exit Leo -> start Leo -> tabs as before related: I think there's a way to search across Leo files: quicksearch multiple files ... ? What if quicksearch looked at all the @bookmarked files and offered to open the ones with hits? ... methinks way cool. > > Edward > > -- > You received this message because you are subscribed to the Google Groups > "leo-editor" group. > To post to this group, send email to leo-editor@googlegroups.com. > To unsubscribe from this group, send email to > leo-editor+unsubscr...@googlegroups.com. > For more options, visit this group at > http://groups.google.com/group/leo-editor?hl=en. > > -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To post to this group, send email to leo-editor@googlegroups.com. To unsubscribe from this group, send email to leo-editor+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/leo-editor?hl=en.
