The Patchfile api defines the external interface to the patchfile package.
The Patchfile api is implemented by the patchfile package.
The Patchfile api source code is src/lib/make-library-glue/patchfile.api. The above information is manually maintained and may contain errors.
api {
Patch = {lines:List(String ), patchname:String};
Patch_Id = {filename:String, patchname:String};
Patch' = {lines:List(String ), patch_id:Patch_Id};
Patchfile;
get_patch_names : Patchfile -> List(String );
get_patch : (Patchfile , String) -> Patch;
print_patchfile : Patchfile -> Void;
read_patchfile : String -> Patchfile;
write_patchfile : Patchfile -> String;
write_patchfile' : Patchfile -> List(Patch ) -> String;
patch_count : Patchfile -> Int;
text_count : Patchfile -> Int;
get_only_patch : Patchfile -> List(String );
set_only_patch : Patchfile -> List(String ) -> Patchfile;
apply_patch : Patchfile -> Patch -> Patchfile;
apply_patches : Patchfile -> List(Patch ) -> Patchfile;
append_to_patch : (Patchfile , String , List(String )) -> Patchfile;
prepend_to_patch : (Patchfile , String , List(String )) -> Patchfile;
empty_all_patches : Patchfile -> Patchfile;
make_patch_beginline : {patchname:String} -> String;
make_patch_endline : {patchname:String} -> String;
map : (Patch' -> List(String )) -> Patchfile -> Patchfile;
apply : (Patch' -> Void) -> Patchfile -> Void;
fold : ((Patch' , X) -> X) -> X -> Patchfile -> X;};