more operations;
authorwenzelm
Sat Nov 03 19:31:15 2018 +0100 (6 months ago)
changeset 6922344d68a00917c
parent 69222 8365124a86ae
child 69224 fe9d746b273e
more operations;
src/Pure/General/file.ML
     1.1 --- a/src/Pure/General/file.ML	Thu Nov 01 13:53:29 2018 +0100
     1.2 +++ b/src/Pure/General/file.ML	Sat Nov 03 19:31:15 2018 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4    val standard_path: Path.T -> string
     1.5    val platform_path: Path.T -> string
     1.6    val bash_path: Path.T -> string
     1.7 +  val bash_paths: Path.T list -> string
     1.8    val full_path: Path.T -> Path.T -> Path.T
     1.9    val tmp_path: Path.T -> Path.T
    1.10    val exists: Path.T -> bool
    1.11 @@ -29,6 +30,7 @@
    1.12    val read: Path.T -> string
    1.13    val write: Path.T -> string -> unit
    1.14    val append: Path.T -> string -> unit
    1.15 +  val generate: Path.T -> string -> unit
    1.16    val output: BinIO.outstream -> string -> unit
    1.17    val write_list: Path.T -> string list -> unit
    1.18    val append_list: Path.T -> string list -> unit
    1.19 @@ -45,7 +47,7 @@
    1.20  val platform_path = ML_System.platform_path o standard_path;
    1.21  
    1.22  val bash_path = Bash_Syntax.string o standard_path;
    1.23 -
    1.24 +val bash_paths = Bash_Syntax.strings o map standard_path;
    1.25  
    1.26  (* full_path *)
    1.27  
    1.28 @@ -154,6 +156,7 @@
    1.29  
    1.30  fun write path txt = write_list path [txt];
    1.31  fun append path txt = append_list path [txt];
    1.32 +fun generate path txt = if try read path = SOME txt then () else write path txt;
    1.33  
    1.34  fun write_buffer path buf = open_output (Buffer.output buf) path;
    1.35