+
+/* 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 will mark the current command as not repeating,
+ and will ensure get_saved_command_line returns the previous command,
+ so that the currently executing command can repeat it. */
+
+extern void repeat_previous ();
+
+/* Prevent dont_repeat from working, and return a cleanup that
+ restores the previous state. */