Reformat commands when solving holes

[mikeshulman]

Currently when solving a hole in ProofGeneral, the inserted term is pretty-printed. But it would be better to reformat the entire command it appears in, since replacing a ? by a longer term could cause different linebreaking and indentation, particularly when the inserted term is part of the case tree.

This will probably require recording some information about the scope of each command in the history, so it can be reformatted in that scope. It will also require some thought regarding how to maintain, or re-create, any other hole overlays currently existing in that command.

[mikeshulman]

Achieved by #98. Scopes are retained by adding an "instant" property to the overlays that ProofGeneral already puts on each command, while hole overlays are just deleted and re-created.