:Coq Set Printing Width not persistent

[bn-peters]

I would like to globally (or even dynamically) adjust the Printing Width (Set Printing Width 100).

Unfortunately :Coq Set Printing Width 120 doesn't always seem to persist: When I execute the command and then step forward, everything works as expected; but as soon as I step backwards beyond the point where I execute the command, the setting is reset.

In any case, thanks for your work on the plugin!

[whonore]

Thanks for reporting, I agree the current behavior is unintuitive. I believe what's happening is, when you do :Coq Set Printing Width 120, Coq updates that setting for the current state ID. Advancing in the file keeps the same setting, but if you rewind before the point where you set it, you return to the earlier state, which has the old setting. Advancing again creates a new state ID so your setting is lost.

You can see this in this example. Advance to the first Test. Then set the width to 100 and step forward twice to the second Test. Then set it to 110 and step forward to the last Test. If you rewind to the first idtac and step forward again you should see 100 and if you rewind back to the first Test or earlier you should see 78 again.

Goal True.
Proof.
  Test Printing Width. (* 78 *)
  (* :Coq Set Printing Width 100 *)
  idtac.
  Test Printing Width. (* 100 *)
  (* :Coq Set Printing Width 110 *)
  idtac.
  Test Printing Width. (* 110 *)
Qed.

It seems like CoqIDE manages to preserve certain settings upon rewinding, so I'll have to look at how they do that.

As a workaround, any settings you set at the beginning of the file should always be preserved since you can't rewind any earlier, but that doesn't help for changing it dynamically.