# HG changeset patch
# User wneuper <Walther.Neuper@jku.at>
# Date 1654006882 -7200
# Node ID 9488084c3441c51beeeca68b5502c524ac1444a6
# Parent  edeeb202911a258c8fc8e31b1cef610a835484da
cleanup

diff -r edeeb202911a -r 9488084c3441 TODO.md
--- a/TODO.md	Tue May 31 11:00:15 2022 +0200
+++ b/TODO.md	Tue May 31 16:21:22 2022 +0200
@@ -69,4 +69,5 @@
 * WN: for calculation by use of Makarius' "problem" as boilerplate clarify:
     - How inspect Token lists, e.g. from ML_Lex.read OR ML_Lex.read_source ?
     - Why the ERROR in Demo_Example.thy at: \<open>problem pbl_bieg : "Biegelinien" = ..\<close> ?
+    - 
 
diff -r edeeb202911a -r 9488084c3441 src/Tools/isac/BridgeJEdit/Calculation.thy
--- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Tue May 31 11:00:15 2022 +0200
+++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Tue May 31 16:21:22 2022 +0200
@@ -18,9 +18,10 @@
 ML_file "preliminary.sml"
 
 section \<open>new code for Outer_Syntax Example  ...\<close>
-text \<open> UPDATE:
-1.  The code re-uses Makarius' \<open>Outer_Syntax.command..problem ..\<close> to a maximal extent.
-2. GOON
+text \<open> 
+  stepwise development to be inspected from
+  https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080
+  onwards.
 \<close>
 
 ML \<open>
@@ -63,9 +64,7 @@
 
 in end;
 \<close> ML \<open>
-Input.pos_of: Input.source -> Position.T
 \<close> ML \<open>
-Position.none
 \<close> ML \<open>
 \<close> 
 
diff -r edeeb202911a -r 9488084c3441 src/Tools/isac/BridgeJEdit/Demo_Example.thy
--- a/src/Tools/isac/BridgeJEdit/Demo_Example.thy	Tue May 31 11:00:15 2022 +0200
+++ b/src/Tools/isac/BridgeJEdit/Demo_Example.thy	Tue May 31 16:21:22 2022 +0200
@@ -69,20 +69,12 @@
 section \<open>Stepwise Development\<close>
 
 subsection \<open>Specification Phase\<close>
-text \<open> UPDATE:
-1. The \<open>Example\<close> below is a minimal adaptation of \<open>problem pbl_bieg : "Biegelinien" ..\<close>
-  in Knowledge/Biegelinie.thy.
-2. GOON
+text \<open> 
+  stepwise development to be inspected from
+  https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080
+  onwards.
 \<close>
 
-(*
-vvvvvvv why raises \<open>Example\<close> exception Option raised (line 82 of "General/basics.ML")? Although 
-        * code (Outer_Syntax.command..Example..) and 
-        * application (Example pbl_bieg : "Biegelinien".) are exact copies from Makarius?
-        * Although the application below with \<open>problem\<close> works?
-        * Although \<open>ExampleSPARK\<close> is disambiguated in Calculation_OLD.thy ?!?
-        HOW CAN SUCH AN ERROR BE INVESTIGATED ? debugger ? .. ?         
-Example problem*)
 Example pbl_bieg : "Biegelinien" =
   Method: "IntegrierenUndKonstanteBestimmen2"
   Given: "Traegerlaenge l_l" "Streckenlast q_q"
diff -r edeeb202911a -r 9488084c3441 test/Tools/isac/Interpret/lucas-interpreter.sml
--- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Tue May 31 11:00:15 2022 +0200
+++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Tue May 31 16:21:22 2022 +0200
@@ -259,7 +259,7 @@
     "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
 (*this is new since ThmC.numerals_to_Free.-----\\*)
     "Calculate PLUS"]
-  then () else error "specific_from_prog ([1], Res) 1 CHANGED";  (*GOON*)
+  then () else error "specific_from_prog ([1], Res) 1 CHANGED";
 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
 
 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [