# HG changeset patch
# User wenzelm
# Date 1541269875 -3600
# Node ID 44d68a00917c1e6fa0d465dbfe93b02550f885d3
# Parent  8365124a86ae6b108b70a11766a86bd5d16a0548
more operations;

diff -r 8365124a86ae -r 44d68a00917c src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Thu Nov 01 13:53:29 2018 +0100
+++ b/src/Pure/General/file.ML	Sat Nov 03 19:31:15 2018 +0100
@@ -9,6 +9,7 @@
   val standard_path: Path.T -> string
   val platform_path: Path.T -> string
   val bash_path: Path.T -> string
+  val bash_paths: Path.T list -> string
   val full_path: Path.T -> Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
   val exists: Path.T -> bool
@@ -29,6 +30,7 @@
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
+  val generate: Path.T -> string -> unit
   val output: BinIO.outstream -> string -> unit
   val write_list: Path.T -> string list -> unit
   val append_list: Path.T -> string list -> unit
@@ -45,7 +47,7 @@
 val platform_path = ML_System.platform_path o standard_path;
 
 val bash_path = Bash_Syntax.string o standard_path;
-
+val bash_paths = Bash_Syntax.strings o map standard_path;
 
 (* full_path *)
 
@@ -154,6 +156,7 @@
 
 fun write path txt = write_list path [txt];
 fun append path txt = append_list path [txt];
+fun generate path txt = if try read path = SOME txt then () else write path txt;
 
 fun write_buffer path buf = open_output (Buffer.output buf) path;