equal
deleted
inserted
replaced
66 |
66 |
67 val drop_last_char = implode o drop_last o explode; |
67 val drop_last_char = implode o drop_last o explode; |
68 |
68 |
69 in |
69 in |
70 |
70 |
71 fun use_text print verbose txt = |
71 fun use_text (print, err) verbose txt = |
72 let |
72 let |
73 val in_buffer = ref (explode txt); |
73 val in_buffer = ref (explode txt); |
74 val out_buffer = ref ([]: string list); |
74 val out_buffer = ref ([]: string list); |
|
75 fun output () = drop_last_char (implode (rev (! out_buffer))); |
75 |
76 |
76 fun get () = |
77 fun get () = |
77 (case ! in_buffer of |
78 (case ! in_buffer of |
78 [] => "" |
79 [] => "" |
79 | c :: cs => (in_buffer := cs; c)); |
80 | c :: cs => (in_buffer := cs; c)); |
81 |
82 |
82 fun exec () = |
83 fun exec () = |
83 (case ! in_buffer of |
84 (case ! in_buffer of |
84 [] => () |
85 [] => () |
85 | _ => (PolyML.compiler (get, put) (); exec ())); |
86 | _ => (PolyML.compiler (get, put) (); exec ())); |
86 |
|
87 fun show_output () = print (drop_last_char (implode (rev (! out_buffer)))); |
|
88 in |
87 in |
89 exec () handle exn => (show_output (); raise exn); |
88 exec () handle exn => (err (output ()); raise exn); |
90 if verbose then show_output () else () |
89 if verbose then print (output ()) else () |
91 end; |
90 end; |
92 |
91 |
93 end; |
92 end; |
94 |
93 |
95 |
94 |