open_file


Description:

public async void open_file (File file, int line_number = -1)

Open/switch to a file, optionally navigate to a specific line.

Parameters:

file

The file to open

line_number

Line to navigate to (0-based); use -1 to restore saved cursor/scroll