1.1 --- a/TODO.md	Wed Apr 21 10:09:14 2021 +0200
     1.2 +++ b/TODO.md	Wed Apr 21 11:24:46 2021 +0200
     1.3 @@ -15,8 +15,6 @@
     1.4  
     1.5  * MW: more concise "setup KEStore_Elems.add_rlss" etc.;
     1.6  
     1.7 -* MW: eliminate low-level TextIO (not portable);
     1.8 -
     1.9  * MW: check uses of Unsynchronized.ref vs. Synchronized.var;
    1.10  
    1.11  * MW: proper formal name space for rule set, model patterns, methods;
    1.12 @@ -57,3 +55,7 @@
    1.13  
    1.14  * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
    1.15  
    1.16 +* WN: use File.read / File.write instead of low-level TextIO operations (not portable);
    1.17 +* WN: use Path.T (e.g. via Path.explode) for portability;
    1.18 +* WN: refrain from using global /tmp directory
    1.19 +  (e.g. see Isabelle_System.create_tmp_path / with_tmp_file / with_tmp_dir);