"Setting" menu should we pre-fill string options for all provers

[Matafou]

Currently when setting something via [Coq/Settings/foo] the current value of the foo is not pre-filled.

When an integer is asked to the user (like for the Printing Width) this is ok.

But if a (long) string is asked (I am thinking about the [Coq/Settings/Search Blacklist] option that I just pushed (commit ff9ec2e)) I prefer to have it prefilled with the current value and be able modify it in the minibuffer.

The commit I just made does this (for string options) only for coq by redefining a macro defined in generic/proof-utils.el (namely proof-defstringset-fn).

But if we think this is what all provers want I would rather modify the macro instead of redefining it. What do other prover users think about that?

P.

[cpitclaudel]

Are there really users of other provers at the moment? If so, it would be nice to find contacts in these communities. Otherwise, the implementations for other provers will bit-rot.

[jonleivent]

On 12/09/2015 10:34 AM, Pierre Courtieu wrote:

Currently when setting something via [Coq/Settings/foo] the current value of the foo is not pre-filled.

When an integer is asked to the user (like for the Printing Width) this is ok.

But if a (long) string is asked (I am thinking about the [Coq/Settings/Search Blacklist] option that I just pushed (commit ff9ec2e)) I prefer to have it prefilled with the current value and be able modify it in the minibuffer.

The commit I just made does this (for string options) only for coq by redefining a macro defined in generic/proof-utils.el (namely proof-defstringset-fn).

But if we think this is what all provers want I would rather modify the macro instead of redefining it. What do other prover users think about that?

P.

---

Reply to this email directly or view it on GitHub:
#17

I'm getting these warnings from your latest commit. Are you missing a
variable declaration?

In toplevel form:
coq/coq.el:144:7:Warning: assignment to free variable
`coq-search-blacklist-string-prev'

In coq-set-search-blacklist:
coq/coq.el:1984:11:Warning: reference to free variable
coq-search-blacklist-string-prev' coq/coq.el:1985:11:Warning: assignment to free variable coq-search-blacklist-string-prev'

-- Jonathan

[Matafou]

Argl probably yes, I never compile pg actually. Will fix this.

P.

2015-12-09 22:09 GMT+01:00 Jonathan Leivent notifications@github.com:

On 12/09/2015 10:34 AM, Pierre Courtieu wrote:

Currently when setting something via [Coq/Settings/foo] the current
value of the foo is not pre-filled.

When an integer is asked to the user (like for the Printing Width) this
is ok.

But if a (long) string is asked (I am thinking about the
[Coq/Settings/Search Blacklist] option that I just pushed (commit ff9ec2e))
I prefer to have it prefilled with the current value and be able modify it
in the minibuffer.

The commit I just made does this (for string options) only for coq by
redefining a macro defined in generic/proof-utils.el (namely
proof-defstringset-fn).

But if we think this is what all provers want I would rather modify the
macro instead of redefining it. What do other prover users think about that?

P.

---

Reply to this email directly or view it on GitHub:
#17

I'm getting these warnings from your latest commit. Are you missing a
variable declaration?

In toplevel form:
coq/coq.el:144:7:Warning: assignment to free variable
`coq-search-blacklist-string-prev'

In coq-set-search-blacklist:
coq/coq.el:1984:11:Warning: reference to free variable
coq-search-blacklist-string-prev' coq/coq.el:1985:11:Warning: assignment to free variable coq-search-blacklist-string-prev'

-- Jonathan

—
Reply to this email directly or view it on GitHub
#17 (comment).

[cpitclaudel]

@Matafou Alternatively to compiling, you could use Flycheck; it will pick up this kind of errors :)

[Matafou]

Fixed.
P.

2015-12-10 13:08 GMT+01:00 Clément Pit--Claudel notifications@github.com:

@Matafou https://github.com/Matafou Alternatively to compiling, you
could use Flycheck; it will pick up this kind of errors :)

—
Reply to this email directly or view it on GitHub
#17 (comment).