1.1 --- a/TODO.md	Fri Aug 05 12:30:16 2022 +0200
     1.2 +++ b/TODO.md	Sat Aug 06 10:45:24 2022 +0200
     1.3 @@ -71,12 +71,21 @@
     1.4  ***** priority of WN items is top down, most urgent/simple on top
     1.5  
     1.6  * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
     1.7 -    - Solve_Step.check ..Rewrite_Inst, Substitute, ..
     1.8      - Error_Pattern.check_for', fill_form
     1.9      - Derive.steps
    1.10      - Fetch_Tacs.specific_from_prog ?
    1.11      - Eval.adhoc_thm, adhoc_thm1_
    1.12      - ? LIST IS NOT COMPLETE
    1.13 +    - Solve_Step.check ..Rewrite_Inst, Substitute, etc: push ctxt through Interpret/*
    1.14 +      a step in a calculation
    1.15 +      initialises ctxt from specified thy            -> pushes ctxt through whole calculation
    1.16 +        val pp = Ctree.par_pblobj pt p;              ->   val ctxt = Ctree.get_loc pt pos |> snd
    1.17 +        val thy' = Ctree.get_obj Ctree.g_domID pt pp;->
    1.18 +        val thy = ThyC.get_theory thy';              ->   val thy = Proof_Context.theory_of ctxt
    1.19 +        val ctxt = Proof_Context.init_global thy;    ->   val thy' = Context.theory_name thy
    1.20 +      cp code to test/*
    1.21 +
    1.22 +* WN: check all Ctree.par_pblobj -- ? better get ctxt = Ctree.get_loc pt pos |> snd ?
    1.23  
    1.24  * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
    1.25    e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
    1.26 @@ -102,6 +111,8 @@
    1.27      - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
    1.28      - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
    1.29  
    1.30 +* WN: rename Pos.* -- Pos.ints, Pos.spec, Pos.empty, Pos.ints_empty
    1.31 +
    1.32  * WN: redesign transition from Specification to Solution: how relate 
    1.33      - Formalise.model with variants (e.g. VSCode_Example)
    1.34        reconsider separation of variants F_I, F_II, see MAWEN paper