open_file


Description:

public async void open_file (File file, int? line_number = null)

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

Parameters:

file

The file to open

line_number

Optional line number to navigate to (overrides saved position)