# HG changeset patch
# User wneuper <Walther.Neuper@jku.at>
# Date 1682776417 -7200
# Node ID 9e987411cfdabe9638a5f2a0a89d3a060dc280e2
# Parent  0710b74705f78bab8af12b8ce53eca4260293db1
add missing I_Model.OLD_to_TEST to sig

diff -r 0710b74705f7 -r 9e987411cfda src/Tools/isac/Specify/i-model.sml
--- a/src/Tools/isac/Specify/i-model.sml	Wed Apr 05 17:46:25 2023 +0200
+++ b/src/Tools/isac/Specify/i-model.sml	Sat Apr 29 15:53:37 2023 +0200
@@ -10,6 +10,7 @@
 
   type T
   type T_TEST
+  val OLD_to_TEST: T -> T_TEST
   val empty: T
   val empty_TEST: T_TEST
   type single
@@ -33,6 +34,7 @@
   val single_to_string_TEST: Proof.context -> single_TEST -> string
   val to_string: Proof.context -> T -> string
   val to_string_TEST: Proof.context -> T_TEST -> string
+  val feedback_OLD_to_TEST: feedback -> feedback_TEST
 
   datatype add_single = Add of single | Err of string
   val init: Model_Pattern.T -> T
diff -r 0710b74705f7 -r 9e987411cfda src/Tools/isac/Specify/p-spec.sml
--- a/src/Tools/isac/Specify/p-spec.sml	Wed Apr 05 17:46:25 2023 +0200
+++ b/src/Tools/isac/Specify/p-spec.sml	Sat Apr 29 15:53:37 2023 +0200
@@ -208,7 +208,7 @@
   | itms2fstr _ (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
   | itms2fstr ctxt (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term ctxt (d $ t))
   | itms2fstr ctxt (itm as (_, _, _, _, I_Model.Par _)) = 
-    raise ERROR ("parsitm (" ^ I_Model.single_to_string ctxt itm ^ "): Par should be internal");
+    raise ERROR ("itms2fstr (" ^ I_Model.single_to_string ctxt itm ^ "): Par should be internal");
 
 fun imodel2fstr iitems = 
   let 
diff -r 0710b74705f7 -r 9e987411cfda test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy
--- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Wed Apr 05 17:46:25 2023 +0200
+++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Sat Apr 29 15:53:37 2023 +0200
@@ -392,8 +392,30 @@
 text \<open>
   # 7: xxxxx:
 \<close> 
-ML \<open> (* # 7: ISAC suggests a next step on request *)
+ML \<open> (* # 7: user inputs value of Method_Ref, which shows the respective Model *)
 \<close>
+
+subsubsection \<open>Specification with Model for the Method_Ref\<close>
+
+text \<open>
+  Observe the (still outcommented) toggles \<Odot>\<Otimes> changed according to the Reference
+\<close>
+Example_TEST "Diff_App-No.123a" (*Specification of the Method_Ref*)
+  Specification:
+    Model:        
+      Given: \<open>Constants [r = 7]\<close> \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>
+        \<open>Extremum (A = 2 * u * v - u \<up> 2)\<close>
+        \<open>SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>
+        \<open>FunctionVariable u\<close> \<open>Domain {0 <..< r}\<close> \<open>ErrorBound (\<epsilon> = 0)\<close> 
+      Where: \<open>0 < r\<close>
+      Find: \<open>Results (A, u, v)\<close>
+      Relate:
+    References:
+      Theory_Ref: "Diff_App"
+  (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"
+  (*\<Otimes>*) Method_Ref: "Optimisation/by_univariate_calculus"
+(*Solution:*)
+
 text \<open> --- remove this line and make content Isar input---\
 ---------- remove this line and make content Isar input---/
 \<close>