+
+class user_args
+{
+public:
+ /* Save the command line and store the locations of arguments passed
+ to the user defined function. */
+ explicit user_args (const char *line);
+
+ /* Insert the stored user defined arguments into the $arg arguments
+ found in LINE. */
+ std::string insert_args (const char *line) const;
+
+private:
+ /* Disable copy/assignment. (Since the elements of A point inside
+ COMMAND, copying would need to reconstruct the A vector in the
+ new copy.) */
+ user_args (const user_args &) =delete;
+ user_args &operator= (const user_args &) =delete;
+
+ /* It is necessary to store a copy of the command line to ensure
+ that the arguments are not overwritten before they are used. */
+ std::string m_command_line;
+
+ /* The arguments. Each element points inside M_COMMAND_LINE. */
+ std::vector<string_view> m_args;
+};
+
+/* The stack of arguments passed to user defined functions. We need a
+ stack because user-defined functions can call other user-defined
+ functions. */
+static std::vector<std::unique_ptr<user_args>> user_args_stack;
+
+/* An RAII-base class used to push/pop args on the user args
+ stack. */
+struct scoped_user_args_level
+{
+ /* Parse the command line and push the arguments in the user args
+ stack. */
+ explicit scoped_user_args_level (const char *line)