equal
deleted
inserted
replaced
95 Note: For the purpose of user-guidance the format of requested input should be indicated! |
95 Note: For the purpose of user-guidance the format of requested input should be indicated! |
96 - proposal for how to indicate requested input: in VSCode_Example.thy subsubsection \<open>Empty Specification> |
96 - proposal for how to indicate requested input: in VSCode_Example.thy subsubsection \<open>Empty Specification> |
97 - this proposal presumable involves hacking of parsers -- is there a better way? |
97 - this proposal presumable involves hacking of parsers -- is there a better way? |
98 - implementation and tests have solution for (a) above as a prerequisite. |
98 - implementation and tests have solution for (a) above as a prerequisite. |
99 |
99 |
100 * WN: rename in Formalise: type spec = Model_Def.form_spec; |
|
101 type refs = Model_Def.form_refs; |
|
102 * WN: as soon as parsing in Outer_Syntax.command..‹Example› works, implement in Calculation |
100 * WN: as soon as parsing in Outer_Syntax.command..‹Example› works, implement in Calculation |
103 - init_ctree, update_status, check_input |
101 - init_ctree, update_status, check_input |
104 |
102 |
105 |
103 |