1.1 --- a/TODO.md	Sun Aug 21 16:20:48 2022 +0200
     1.2 +++ b/TODO.md	Mon Aug 22 11:26:20 2022 +0200
     1.3 @@ -51,20 +51,15 @@
     1.4      - the trial with <fun is_empty> in Calculation.thy makes the question more precise: 
     1.5        better hack parsers or better work on ML_Syntax?
     1.6  
     1.7 +* ?How accomplish two user-requirements by Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
     1.8 +   (1) start a Calculation with a CAS_Cmd
     1.9 +   (2) start an Example from scratch, i.e. with (Formalize.empty, References.empty)
    1.10 +   Proposals for a solution are in test/../Test_VSCode_Example.thy
    1.11 +   subsubsection ‹Start Example with a CAS_Cmd›
    1.12 +
    1.13  
    1.14  ***** priority of WN items is top down, most urgent/simple on top
    1.15  
    1.16 -* WN: rewriting with ctxt not complete (cause errors hard to indentify later)
    1.17 -    - Solve_Step.check ..Rewrite_Inst, Substitute, etc: push ctxt through Interpret/*
    1.18 -      a step in a calculation
    1.19 -      initialises ctxt from specified thy            -> pushes ctxt through whole calculation
    1.20 -        val pp = Ctree.par_pblobj pt p;              ->   val ctxt = Ctree.get_loc pt pos |> snd
    1.21 -        val thy' = Ctree.get_obj Ctree.g_domID pt pp;->
    1.22 -        val thy = ThyC.get_theory thy';              ->   val thy = Proof_Context.theory_of ctxt
    1.23 -        val ctxt = Proof_Context.init_global thy;    ->   val thy' = Context.theory_name thy
    1.24 -      cp code to test/*
    1.25 -    - Derive.steps: note HACK, new code still outcommented
    1.26 -
    1.27  * WN: eliminate SPARK; as an example replaced by Outer_Syntax.command..problem
    1.28  
    1.29  * WN: Step_Specify.initialisePIDE: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc