+
+/* Command line saving and repetition.
+ Each input line executed is saved to possibly be repeated either
+ when the user types an empty line, or be repeated by a command
+ that wants to repeat the previously executed command. The below
+ functions control command repetition. */
+
+/* Commands call dont_repeat if they do not want to be repeated by null
+ lines or by repeat_previous (). */
+
+extern void dont_repeat ();
+
+/* Commands call repeat_previous if they want to repeat the previous
+ command. Such commands that repeat the previous command must
+ indicate to not repeat themselves, to avoid recursive repeat.
+ repeat_previous marks the current command as not repeating, and
+ ensures get_saved_command_line returns the previous command, so
+ that the currently executing command can repeat it. If there's no
+ previous command, throws an error. Otherwise, returns the result
+ of get_saved_command_line, which now points at the command to
+ repeat. */
+
+extern const char *repeat_previous ();
+
+/* Prevent dont_repeat from working, and return a cleanup that
+ restores the previous state. */