Scripts can terminate execution by setting mp.keep_running = false. Add
an exit() function to wrap setting mp.keep_running and properly expose
this feature. It can be used e.g. by a thumbnail script to spawn workers
with load-script and then let them quit.
It is not added to the mp namespace as mp.exit because that would make
it look like it terminates mpv.
This mirrors the exit() function which already exists in js.
The note in javascript.rst about having to remove key bindings before
exit is not kept because they are actually removed automatically since
bf385e1140 (though it was accurate when the JS backend was developed
before upstreaming it).
I misunderstood CogentRedTester's review in
https://github.com/mpv-player/mpv/pull/10282#discussion_r1428972352 as
referring to the cursor_position in mp.input's arguments instead of the
one received by the closed callback.
The cursor_position passed to input.get doesn't need to be converted to
a number because it was already JSON, while the cursor_position received
by the closed callback is currently a string, and we need to pass JSON
in input-event script messages to keep it as an integer to work around
mpv converting integer script message arguments to string.
This is more noticeable after implementing mp.input.select(): its submit
argument currently receives the selected index as a string, and this
makes Lua error if you use it as an index of a numerical table, e.g.:
submit = function (id)
mp.set_property(property, tracks[tonumber(id)].selected and "no"
or tracks[tonumber(id)].id)
...
end,
This commit avoids having to call tonumber(id).
