# HG changeset patch
# User wenzelm
# Date 1003602074 -7200
# Node ID 651650b717e10e05e42fadcafa071365e8c4ed65
# Parent  a528a716a31233d3f976fc29444c9e4a43ddb12f
conditional: bool -> (unit -> unit) -> unit;
std_error: string -> unit;

diff -r a528a716a312 -r 651650b717e1 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Oct 20 20:20:41 2001 +0200
+++ b/src/Pure/library.ML	Sat Oct 20 20:21:14 2001 +0200
@@ -71,6 +71,7 @@
   val toggle: bool ref -> bool
   val change: 'a ref -> ('a -> 'a) -> unit
   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+  val conditional: bool -> (unit -> unit) -> unit
 
   (*lists*)
   exception LIST of string
@@ -154,6 +155,7 @@
   val cat_lines: string list -> string
   val space_explode: string -> string -> string list
   val std_output: string -> unit
+  val std_error: string -> unit
   val prefix_lines: string -> string -> string
   val split_lines: string -> string list
   val untabify: string list -> string list
@@ -425,6 +427,11 @@
   end;
 
 
+(* conditional execution *)
+
+fun conditional b f = if b then f () else ();
+
+
 
 (** lists **)
 
@@ -1145,8 +1152,8 @@
 val cd = OS.FileSys.chDir;
 val pwd = OS.FileSys.getDir;
 
-fun std_output s =
-  (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
 
 fun prefix_lines prfx txt =
   txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;