Input the file with the name specified by the string. The file will be read in, and the text will be treated as Magma input. Tilde expansion of file names is allowed.
(Interactive load.) Input the file with the name specified by the string. The file will be read in, and the text will be treated as Magma input. Tilde expansion of file names is allowed. In contrast to load, the user has the chance to interact as each line is read in:As the line is read in, it is displayed and the system waits for user response. At this point, the user can skip the line (by moving "down"), edit the line (using the normal editing keys) or execute it (by pressing "enter"). If the line is edited, the new line is executed and the original line is presented again.