When opening Leo I get the following in the terminal:
chris@technatica:~/leo-editor$ python3 ./launchLeo.py --dock
setting leoID from os.getenv('USER'): 'chris'
Leo 6.0-devel, dock branch, build 96296149a5
2019-05-23 06:53:33 -0500
Duplicate dock name: 'outline'
Duplicate dock name: 'body'
Duplicate dock name: 'tabs'
Duplicate dock name: 'outline'
Duplicate dock name: 'body'
Duplicate dock name: 'tabs'
I had three files open when I closed the previous session.
Would it not then make sense to give each dock a unique name? And would
this not then lend itself to presenting a list of all currently open docks?
Then the user could select the dock desired and have it present itself back
in its last known position.
I will need to use it a little more in a multi-file session to see if more
ideas come up.
The docks are not restricted to the main UI for placement on a screen. They
do follow the main UI though when it comes to maximize/minimize which
limits the usefulness. The docks also do not show up in my desktop
environment's window manager. Is it possible to truly cut them loose and
give the docks their own independent ability to maximize/minimize? I think
this would also allow them to utilize all of the window manager's features
like "Kepp Above", "Keep Below", "Move" etc.
If it isn't possible to cut them loose, would it not be helpful to be able
to minimize a dock and have a mechanism by which it could be "maximized"
back to its original position before minimizing?
Again, I will need more time fiddling to come up with more ideas.
Chris
--
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 https://groups.google.com/group/leo-editor.
To view this discussion on the web visit
https://groups.google.com/d/msgid/leo-editor/3f067552-fbfa-4f9f-8c51-e17f55af0154%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
