1.1 --- a/TODO.md	Tue May 31 11:00:15 2022 +0200
     1.2 +++ b/TODO.md	Tue May 31 16:21:22 2022 +0200
     1.3 @@ -69,4 +69,5 @@
     1.4  * WN: for calculation by use of Makarius' "problem" as boilerplate clarify:
     1.5      - How inspect Token lists, e.g. from ML_Lex.read OR ML_Lex.read_source ?
     1.6      - Why the ERROR in Demo_Example.thy at: \<open>problem pbl_bieg : "Biegelinien" = ..\<close> ?
     1.7 +    - 
     1.8  

     2.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Tue May 31 11:00:15 2022 +0200
     2.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Tue May 31 16:21:22 2022 +0200
     2.3 @@ -18,9 +18,10 @@
     2.4  ML_file "preliminary.sml"
     2.5  
     2.6  section \<open>new code for Outer_Syntax Example  ...\<close>
     2.7 -text \<open> UPDATE:
     2.8 -1.  The code re-uses Makarius' \<open>Outer_Syntax.command..problem ..\<close> to a maximal extent.
     2.9 -2. GOON
    2.10 +text \<open> 
    2.11 +  stepwise development to be inspected from
    2.12 +  https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080
    2.13 +  onwards.
    2.14  \<close>
    2.15  
    2.16  ML \<open>
    2.17 @@ -63,9 +64,7 @@
    2.18  
    2.19  in end;
    2.20  \<close> ML \<open>
    2.21 -Input.pos_of: Input.source -> Position.T
    2.22  \<close> ML \<open>
    2.23 -Position.none
    2.24  \<close> ML \<open>
    2.25  \<close> 
    2.26  

     3.1 --- a/src/Tools/isac/BridgeJEdit/Demo_Example.thy	Tue May 31 11:00:15 2022 +0200
     3.2 +++ b/src/Tools/isac/BridgeJEdit/Demo_Example.thy	Tue May 31 16:21:22 2022 +0200
     3.3 @@ -69,20 +69,12 @@
     3.4  section \<open>Stepwise Development\<close>
     3.5  
     3.6  subsection \<open>Specification Phase\<close>
     3.7 -text \<open> UPDATE:
     3.8 -1. The \<open>Example\<close> below is a minimal adaptation of \<open>problem pbl_bieg : "Biegelinien" ..\<close>
     3.9 -  in Knowledge/Biegelinie.thy.
    3.10 -2. GOON
    3.11 +text \<open> 
    3.12 +  stepwise development to be inspected from
    3.13 +  https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080
    3.14 +  onwards.
    3.15  \<close>
    3.16  
    3.17 -(*
    3.18 -vvvvvvv why raises \<open>Example\<close> exception Option raised (line 82 of "General/basics.ML")? Although 
    3.19 -        * code (Outer_Syntax.command..Example..) and 
    3.20 -        * application (Example pbl_bieg : "Biegelinien".) are exact copies from Makarius?
    3.21 -        * Although the application below with \<open>problem\<close> works?
    3.22 -        * Although \<open>ExampleSPARK\<close> is disambiguated in Calculation_OLD.thy ?!?
    3.23 -        HOW CAN SUCH AN ERROR BE INVESTIGATED ? debugger ? .. ?         
    3.24 -Example problem*)
    3.25  Example pbl_bieg : "Biegelinien" =
    3.26    Method: "IntegrierenUndKonstanteBestimmen2"
    3.27    Given: "Traegerlaenge l_l" "Streckenlast q_q"

     4.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Tue May 31 11:00:15 2022 +0200
     4.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Tue May 31 16:21:22 2022 +0200
     4.3 @@ -259,7 +259,7 @@
     4.4      "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
     4.5  (*this is new since ThmC.numerals_to_Free.-----\\*)
     4.6      "Calculate PLUS"]
     4.7 -  then () else error "specific_from_prog ([1], Res) 1 CHANGED";  (*GOON*)
     4.8 +  then () else error "specific_from_prog ([1], Res) 1 CHANGED";
     4.9  (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
    4.10  
    4.11  (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [