Function addFile

src/lib/editorManager.js:2222–2233

* Adds a file to the manager's file list and updates the UI. * @param {File} file - The file to be added.

(file)

	 * @param {File} file - The file to be added.
	 */
	function addFile(file) {
		if (manager.files.includes(file)) return;
		const insertAt = file.pinned
			? getPinnedInsertIndex()
			: manager.files.length;
		manager.files.splice(insertAt, 0, file);
		syncOpenFileList();
		if (!manager.activeFile) {
			$header.text = file.name;
		}
		toggleProblemButton();
	}

	function getPinnedInsertIndex(skipFile = null) {
		return manager.files.reduce((count, file) => {