1.1 --- a/TODO.md	Thu Jul 28 11:30:53 2022 +0200
     1.2 +++ b/TODO.md	Thu Jul 28 11:43:27 2022 +0200
     1.3 @@ -94,8 +94,8 @@
     1.4  * WN: ?How represent items, which have not yet been input?
     1.5     Note: For the purpose of user-guidance the format of requested input should be indicated!
     1.6      - proposal for how to indicate requested input: in VSCode_Example.thy subsubsection \<open>Empty Specification>
     1.7 -    - this proposal presumable involves hacking of parsers -- is there a better way?
     1.8 -    - implementation and tests have solution for (a) above as a prerequisite.
     1.9 +    - the trial with <fun is_empty> in Calculation.thy makes the question more precise: 
    1.10 +      better hack parsers or better work on ML_Syntax?
    1.11  
    1.12  * WN: as soon as parsing in Outer_Syntax.command..‹Example› works, implement in Calculation
    1.13    - init_ctree, update_status, check_input