exec_script : string -> unit
- load "aiLib"; open aiLib; - load "smlExecScripts"; open smlExecScripts; (* output omitted *) > val it = () : unit val dir = HOLDIR ^ "/src/AI/sml_inspection"; (* user can choose *) val scriptin = dir ^ "/script.sml"; val scriptout = dir ^ "/script-out"; (* output omitted *) - writel scriptin ["load \"aiLib\"; open aiLib;", String.concatWith " " ["writel", mlquote scriptout, "[\"hello world!\"]"]]; > val it = (): unit - exec_script scriptin; > val it = (): unit - readl "script-out"; > val it = ["hello world!"]: string list