| @@ -38,6 +38,7 @@ local opts = { · 37 unmodified lines |
| 38 | case_sensitive = platform ~= 'windows' and true or false, | 38 | case_sensitive = platform ~= 'windows' and true or false, |
| 39 | history_dedup = true, | 39 | history_dedup = true, |
| 40 | font_hw_ratio = 'auto', | 40 | font_hw_ratio = 'auto', |
| | 41 | pause_on_open = false, |
| 41 | } | 42 | } |
| 42 | | 43 | |
| 43 | local styles = { | 44 | local styles = { |
| @@ -89,6 +90,7 @@ local log_buffers = {[id] = {}} · 45 unmodified lines |
| 89 | local key_bindings = {} | 90 | local key_bindings = {} |
| 90 | local dont_bind_up_down = false | 91 | local dont_bind_up_down = false |
| 91 | local global_margins = { t = 0, b = 0 } | 92 | local global_margins = { t = 0, b = 0 } |
| | 93 | local was_playing = true |
| 92 | local input_caller | 94 | local input_caller |
| 93 | | 95 | |
| 94 | local suggestion_buffer = {} | 96 | local suggestion_buffer = {} |
| @@ -1721,12 +1723,21 @@ local function undefine_key_bindings() · 1626 unmodified lines |
| 1721 | key_bindings = {} | 1723 | key_bindings = {} |
| 1722 | end | 1724 | end |
| 1723 | | 1725 | |
| | 1726 | local function pause_playback() |
| | 1727 | was_playing = not mp.get_property_native('pause') |
| | 1728 | |
| | 1729 | if opts.pause_on_open and was_playing then |
| | 1730 | mp.set_property_native('pause', true) |
| | 1731 | end |
| | 1732 | end |
| | 1733 | |
| 1724 | -- Set the REPL visibility ("enable", Esc) | 1734 | -- Set the REPL visibility ("enable", Esc) |
| 1725 | set_active = function (active) | 1735 | set_active = function (active) |
| 1726 | if active == repl_active then return end | 1736 | if active == repl_active then return end |
| 1727 | if active then | 1737 | if active then |
| 1728 | repl_active = true | 1738 | repl_active = true |
| 1729 | insert_mode = false | 1739 | insert_mode = false |
| | 1740 | pause_playback() |
| 1730 | define_key_bindings() | 1741 | define_key_bindings() |
| 1731 | | 1742 | |
| 1732 | if not input_caller then | 1743 | if not input_caller then |
| @@ -1744,6 +1755,10 @@ set_active = function (active) · 11 unmodified lines |
| 1744 | log_buffers[id] = {} | 1755 | log_buffers[id] = {} |
| 1745 | unbind_mouse() | 1756 | unbind_mouse() |
| 1746 | else | 1757 | else |
| | 1758 | if opts.pause_on_open and was_playing then |
| | 1759 | mp.set_property_native('pause', false) |
| | 1760 | end |
| | 1761 | |
| 1747 | repl_active = false | 1762 | repl_active = false |
| 1748 | suggestion_buffer = {} | 1763 | suggestion_buffer = {} |
| 1749 | undefine_key_bindings() | 1764 | undefine_key_bindings() |