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)