1.1 --- a/TODO.md Tue Jul 26 22:01:40 2022 +0200
1.2 +++ b/TODO.md Tue Jul 26 22:11:41 2022 +0200
1.3 @@ -3,12 +3,16 @@
1.4 and not on the definition as a whole.
1.5 - in MathEngBasic/problem "Outer_Syntax.command \<^command_keyword>\<open>problem\<close>" there are writeln
1.6 and comments with testdata from "problem pbl_bieg : "Biegelinien"" in Biegelinie.thy
1.7 - - in BridgeJEdit/Calculation.thy are remainings of time-consuming investigations
1.8 - in MathEngBasic/problem there is guesswork ("TODO") how to reorganise "fun prep_input_PIDE"
1.9 such that errors in "Given" etc are indicated WITHIN the term.
1.10
1.11 * ?MW?: In Outer_Syntax.command \<^command_keyword>\<open>Example\<close> is there a quick fix
1.12 for successfully replacing hacked Problem.parse_cas by parse_references_input?
1.13 + (a) In addition to replacing Problem.parse_cas: How implement the optional parser:
1.14 + - Example "Diff_App/No.123 a" + NONE
1.15 + - Example "Diff_App/No.123 a" + SOME (probl_id, model_input, refs_input)
1.16 + i.e. we expect ISAC to present an empty template "Problem..Solution", but as a whole, to the user;
1.17 + see VSCode_Example.thy subsubsection \<open>Specification step by step\<close>
1.18 How get Token.src for testing purposes?
1.19 How can Scan.* be traced?
1.20 (Tracing should help understanding Problem.parse_cas, Problem.parse_model_input which involve Scan.*)
1.21 @@ -87,3 +91,10 @@
1.22 - !?! I_Model of MethodC (fairly free sequence, dependent on Formalise.model)
1.23 - !?! formal arguments of program (fixed sequence)
1.24
1.25 +* WN: ?How represent items, which have not yet been input?
1.26 + Note: For the purpose of user-guidance the format of requested input should be indicated!
1.27 + - proposal for how to indicate requested input: in VSCode_Example.thy subsubsection \<open>Empty Specification>
1.28 + - this proposal presumable involves hacking of parsers -- is there a better way?
1.29 + - implementation and tests have solution for (a) above as a prerequisite.
1.30 +
1.31 +