src/Pure/ML-Systems/polyml.ML

     fn () => brk (99999, 0), en);
 
 
 (* ML command execution -- 'eval' *)
 
+local
+
+fun drop_last [] = []
+  | drop_last [x] = []
+  | drop_last (x :: xs) = x :: drop_last xs;
+
+val drop_last_char = implode o drop_last o explode;
+
+in
+
 fun use_text print verbose txt =
   let
     val in_buffer = ref (explode txt);
     val out_buffer = ref ([]: string list);
 

     fun exec () =
       (case ! in_buffer of
         [] => ()
       | _ => (PolyML.compiler (get, put) (); exec ()));
 
-    fun show_output () = print (implode (rev (! out_buffer)));
+    fun show_output () = print (drop_last_char (implode (rev (! out_buffer))));
   in
     exec () handle exn => (show_output (); raise exn);
     if verbose then show_output () else ()
   end;
 

 fun exhibit_interrupt f x = f x;
 
 
 
 (** OS related **)
-
-local
-
-fun drop_last [] = []
-  | drop_last [x] = []
-  | drop_last (x :: xs) = x :: drop_last xs;
-
-val drop_last_char = implode o drop_last o explode;
-
-in
-
 
 (* system command execution *)
 
 (*execute Unix command which doesn't take any input from stdin and
   sends its output to stdout*)