search

dapphub / klab

K framework proof explorer & smart contract specification format
GNU Affero General Public License v3.0
124 stars 36 forks source link

klab fetch shouldn't focus #389

Open asymmetric opened 4 years ago

asymmetric commented 4 years ago

Or at least, it should make it possible not to focus.

The usecase is me trying to debug two proofs, and fetch stealing the focus away from the currently focused one seems unnecessary.

d-xo commented 4 years ago

I quite like fetch focusing, I would for sure keep it as the default.

You can also fetch into a new directory (e.g. cd $(mktemp -d) && klab fetch <URL>), and everything works fine without messing up the focused proof in your current directory.

asymmetric commented 4 years ago

Yeah that's true. I just think it's a behaviour that isn't necessarily part of the semantics of a "fetch".

asymmetric commented 4 years ago

Alternatively, since it asks questions already, it could ask if it should focus and default to yes.

d-xo commented 4 years ago

Alternatively, since it asks questions already, it could ask if it should focus and default to yes.

I would be OK with this :+1: :ok_hand: