
4.7.7 The Preferences structure
Shell.Options.Preferences
val editor: string option
editor are "EmacsServer", "External", and "Custom".
"EmacsServer", MLWorks uses its Emacs-server editor facility to invoke editors.
"External", MLWorks uses the external editor command specified in externalEditorCommand (which is also the value of the External Editor text box on the GUI environment's Preferences > Editor dialog) to invoke editors.
"Custom", MLWorks uses the custom editor specified in customEditorName (which is also the value of the Custom Editor Name text box on the GUI environment's Preferences > Editor dialog) to invoke editors.

Generated with Harlequin WebMaker