Re: [isabelle] Isabelle2013-2-RC2 available for testing



Am 01.12.2013 00:07, schrieb Yannick Duchêne (Hibou57):
I guess that's because jEdit can't know if the document is still opened, and probably it supposes it still is, and in such a case, a click on the row which is already selected, is probably supposed to result into the document opened twice.
It shouldn't suppose such things, if I click on the documentation I want it to open. Think the problem is that the document is opened when the item is selected not when it's clicked on, if you use the arrow keys to select a documentation, all documentations on the way are opened ;)

Related problem: on OS X for each documentation a new instance of my viewer is started instead of reusing the old instance as customary under OS X, why don't you just use OS X's "open" command which handles all this?

Best Benedikt






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.