questions about parsing in Outer_Syntax.command?Example?
authorwneuper <Walther.Neuper@jku.at>
Tue, 26 Jul 2022 22:11:41 +0200
changeset 60492a4f173bee704
parent 60491 045784ce9f33
child 60493 ba7b7a24bc3f
questions about parsing in Outer_Syntax.command?Example?
TODO.md
     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 +