1.1 --- a/TODO.md	Wed Jul 20 11:11:31 2022 +0200
     1.2 +++ b/TODO.md	Wed Jul 20 11:48:38 2022 +0200
     1.3 @@ -1,3 +1,10 @@
     1.4 +* MW: make Outer_Syntax.command \<^command_keyword>\<open>problem\<close> a model for ..\<open>Example\<close>
     1.5 +  An ML syntax error should be indicated in place (in the string after \<^keyword>\<open>Given\<close> etc)
     1.6 +  and not on the definition as a whole. 
     1.7 +    This however is not the case despite there is no ISAC code involved.
     1.8 +    Reproducible e.g. at https://hg.risc.uni-linz.ac.at/wneuper/isa/file/9c2e1efe5cde/src/Tools/isac/Knowledge/Biegelinie.thy#l108
     1.9 +    The respective improvement would be the model for WN continuing ..\<open>Example\<close>. 
    1.10 +
    1.11  * MW: check uses of Unsynchronized.ref vs. Synchronized.var;
    1.12  
    1.13  * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)