14.4.69  Patchfiles

The Patchfiles api defines the external interface to the patchfiles package.

The Patchfiles api is implemented by the patchfiles package.

The Patchfiles api source code is src/lib/make-library-glue/patchfiles.api. The above information is manually maintained and may contain errors.

api {
    Patch_Id  = {filename:String, patchname:String};
    Patch  = {lines:List(String ), patch_id:Patch_Id};
    Patchfiles;
    empty : Patchfiles;
    load_patchfile : (String , Patchfiles) -> Patchfiles;
    load_patchfiles : List(String ) -> Patchfiles;
    get_filenames : Patchfiles -> List(String );
    write_patchfiles : Patchfiles -> List(String );
    get_patchfile : Patchfiles -> String -> patchfile::Patchfile;
    get_patch : Patchfiles -> Patch_Id -> Patch;
    apply_patch : Patchfiles -> Patch -> Patchfiles;
    apply_patches : Patchfiles -> List(Patch ) -> Patchfiles;
    append_to_patch : Patchfiles -> Patch -> Patchfiles;
    prepend_to_patch : Patchfiles -> Patch -> Patchfiles;
    map : (Patch -> List(String )) -> Patchfiles -> Patchfiles;
    apply : (Patch -> Void) -> Patchfiles -> Void;
    fold : ((Patch , X) -> X) -> X -> Patchfiles -> X;
    empty_all_patches : Patchfiles -> Patchfiles;};