1.1 --- a/TODO.md	Wed Sep 14 11:33:10 2022 +0200
     1.2 +++ b/TODO.md	Thu Sep 15 10:07:12 2022 +0200
     1.3 @@ -60,6 +60,14 @@
     1.4  
     1.5  ***** priority of WN items is top down, most urgent/simple on top
     1.6  
     1.7 +* WN: follow up meeting Makarius 1: new concept of parsing within current ‹ML_structure Context›
     1.8 +      follow up 2: ‹ML_structure Problem› parsed on loading by ‹term Outer_Syntax.command›‹Example›
     1.9 +      follow up 3: ‹ML_structure MethodC› parsed on loading by ‹term Outer_Syntax.command›‹Example›
    1.10 +      follow up 4: cleanup
    1.11 +      follow up 5: distinguish between ctxt used within ‹ML_structure Calc› and ctxt_expl
    1.12 +                   i.e. the ctxt provided by ‹Example› on "the worksheet" used by the student.
    1.13 +
    1.14 +* WN: eliminate KEStore_Elems.get_thes, add_thes 
    1.15  * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
    1.16    See notes in Build_Thydata.thy.
    1.17      https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes 
    1.18 @@ -70,7 +78,9 @@
    1.19    retrieving Thm and Rls from string-identifiers (which do NOT indicate the theory of) --
    1.20    -- get_thes and add_thes are the main reason for (b)
    1.21    So: How can KEStore_Elems.get_thes and KEStore_Elems.add_thes be replaced in current Isabelle?
    1.22 +* WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store›
    1.23  
    1.24 +* WN: Specify/formalise.sml is in BaseDefinitions/ AND Specify/  DELETE ONE VERSION
    1.25  * WN: rename structure KEStore_Elems --> Know_Store
    1.26  * WN: Step_Specify.initialise_PIDE: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc
    1.27        ? which uses initialise_PIDE !?

     2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Sep 14 11:33:10 2022 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Thu Sep 15 10:07:12 2022 +0200
     2.3 @@ -50,18 +50,21 @@
     2.4  \<close>
     2.5  section \<open>Knowledge elements for problems and methods\<close>
     2.6  text \<open>
     2.7 -  Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
     2.8 -  In the front-end Knowledge comprises theories, problems and methods.
     2.9 -  Elements of problems and methods are defined in theories alongside
    2.10 -  the development of respective language elements. 
    2.11 -  However, the structure of methods and problems is independent from theories' 
    2.12 -  deductive structure. Thus respective structures are built in Build_Thydata.thy.
    2.13 +  \<open>ML_structure Problem\<close>, \<open>ML_structure MethodC\<close> and \<open>Example\<close>s are held by "Know_Store".
    2.14  
    2.15 -  Most elements of problems and methods are implemented in "Knowledge/", but some
    2.16 -  of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
    2.17 -  location in the directory structure.
    2.18 +  The structure of \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> is independent from 
    2.19 +  theories' dependency graph. Thus the respective elements are stored as \<open>TermC.as_string\<close>
    2.20 +  and parsed on the fly within the current @{ML_structure Context},
    2.21 +  while being loaded into \<open>ML_structure Calc\<close>.
    2.22  
    2.23 -  get_* retrieves all * of the respective theory PLUS of all ancestor theories.
    2.24 +  Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term typ_a2real\<close> etc)
    2.25 +  are used for "parsing on the fly" until further clarification.
    2.26 +\<open>\<close>
    2.27 +  Most elements of \<open>ML_structure Problem\<close> and \<open>ML_structure MethodC\<close> are implemented in 
    2.28 +  \<open>directory Knowledge/\<close> but some of them are implemented in \<open>directory ProgLang/\<close>already; 
    2.29 +  thus \<open>theory Know_Store\<close> got this location in the directory structure.
    2.30 +
    2.31 +  \<open>term Know_Store.get_*\<close> retrieves all * of the respective theory PLUS of all ancestor theories.
    2.32  \<close> ML \<open>
    2.33  signature KESTORE_ELEMS(*TODO rename to KNOW_STORE*) =
    2.34  sig

     3.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Wed Sep 14 11:33:10 2022 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Sep 15 10:07:12 2022 +0200
     3.3 @@ -28,8 +28,7 @@
     3.4    In contrast, old-style \<^ML>\<open>Thy_Info.get_theory\<close> requires a finished logic image, for
     3.5    example in \<^file>\<open>$ISABELLE_ISAC_TEST/Tools/isac/Test_Some.thy\<close> loaded from session Isac.
     3.6  
     3.7 -  Note on planned improvements (WN): 
     3.8 -  All theories below ML_structure\<open>MathEngine\<close> in the sessiongraph
     3.9 +  All theories below ML_structure\<open>MathEngine\<close> in the theories' dependency graph
    3.10    can be considered as Isac's version of Pure: the respective code handles items
    3.11    declared later between \<^ML>\<open>@{theory Base_Tools}\<close> and \<^ML>\<open>@{theory Isac_Knowledge}\<close>.
    3.12    These items are contained in the  ML_structure\<open>Context\<close> in current Isabelle,