"with" command (alternative to the "/" command)

[Philippe Waroquiers]

On Fri, 2019-05-24 at 19:31 +0100, Pedro Alves wrote:
> I'd like to explore other user interfaces for this.  I'm aware
> that you've done a ton of work on the / command, which makes
> it uncomfortable for me to suggest it...  I wish it was
> discussed before that; if it was and I missed it, I'm truly
> sorry.  :-(
No problem, the work done on / was not that huge, and at the end,
if it was the trigger that led to finish the option work, it was time
well spent :).

> > In summary: IMO, there is not a huge set of reasons to
> > have both the "/" and this patch, or at least there are
> > reasonable ways to do what "/" provides, maybe with
> > little additional features such as:
> >   * the optional COMMAND after 
> >       'set some_option [COMMAND]'
> >   * add a systematic way to relaunch the previous command
> >     by starting a line with a '-' option.
> > 
> 
> Right, so today I'm kind of sick with fever so I decided to
> prototype something, instead of working on what I should be
> working on.  :-P.
> 
> So I tried quickly prototyping a "with" command, which is
> just like "set", but sets the setting, runs the command
> and then restores the setting.
Looks nice and good enough to replace the / command
(and a very often 'with print some_option_often_temporary_changed -- COMMAND'
can always be put in a user defined command with a short name).

Thanks for doing this,

Philippe