1.1 --- a/TODO.md	Sun Apr 18 18:32:57 2021 +0200
     1.2 +++ b/TODO.md	Sun Apr 18 18:39:18 2021 +0200
     1.3 @@ -1,18 +1,16 @@
     1.4 -* switch `isa` repository to Isabelle repository clone (instead of Isabelle2021 release)
     1.5 -  * MW: remove clones of Isabelle2021 and refer to separate Isabelle repos instead;
     1.6 -  * MW: proper build Isabelle/Scala add-ons (presently unused);
     1.7 +* WN: clean up meta-comments for testing:
     1.8 +    - use \<^isac_test>CARTOUCHE for signature and structure body where actually required;
     1.9 +    - remove vacous comments;
    1.10  
    1.11 -* Isabelle/ML brush-up:
    1.12 -  * MW: provide @{isac_test ML} antiquotation, based on system option "isac_test";
    1.13 -  * WN: clean up meta-comments for testing (remove or upgrade to @{isac_test});
    1.14 -  * WN: eliminate "handle _ => ..." , either use @{try} / @{can} antiquotation
    1.15 -    or more basic try/can combinators;
    1.16 +* WN or MW: remove eliminate xcoding-to-test.sh etc. --- option "isac_test" takes over this role
    1.17 +  (already present in $ISABELLE_ISAC_TEST/ROOT)
    1.18  
    1.19 -* systematic test runs, as regular Isabelle build session
    1.20 -  * eliminate xcoding-to-test.sh etc.;
    1.21 -  * proper ROOT for all tests: `Test_Isac_Short`;
    1.22 +* WN: eliminate "handle _ => ..." (essential for PIDE interaction):
    1.23 +    - either use \<^try>CARTOUCHE / \<^can>CARTOUCHE antiquotation
    1.24 +    - or more basic try/can combinators;
    1.25  
    1.26 -* MW: eliminate odd notation term tricks, e.g. "^^^";
    1.27 +* WN: eliminate odd notation term tricks: replace "^^^" e.g. by "\<up>" based on "_ powr _" for type real;
    1.28 +
    1.29  * WN: eliminate numerals_to_free, use existing Isabelle/HOL facilities;
    1.30  
    1.31  * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)