TODO.md
changeset 60270 844610c5c943
parent 60260 6a3b143d4cf4
child 60275 98ee674d18d3
     1.1 --- a/TODO.md	Thu Apr 29 14:13:11 2021 +0200
     1.2 +++ b/TODO.md	Thu Apr 29 17:02:10 2021 +0200
     1.3 @@ -1,8 +1,3 @@
     1.4 -* WN: eliminate "handle _ => ..." (essential for PIDE interaction):
     1.5 -    - either use \<^try>CARTOUCHE / \<^can>CARTOUCHE antiquotation
     1.6 -    - or more basic try/can combinators;
     1.7 -    - or more direct ML of intention;
     1.8 -
     1.9  * reconsider use of Thy_Info.get_theory: only works with batch-build, not within PIDE session;
    1.10    + consider in Build_Thydata:  Thy_Hierarchy.insert_errpatIDs
    1.11    + consider in Biegelinie.thy: KEStore_Elems.add_thes,