workspaces_prefs.php

<?hh

function workspace_prefs_to_db_rows(workspace_t $workspace, array<string, mixed> $prefs): array<db_workspaces_prefs_row_t> {
	$pref_rows = [];

	foreach ($prefs as $pref_name => $pref_value){
		$new_pref = shape(
			'workspace_id' => $workspace['id'],
			'pref_name'    => $pref_name,
			'pref_value'   => json_encode($pref_value),
		);

		$pref_rows[] = $new_pref;
	}

	return $pref_rows;
}