1.1 --- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Thu Aug 04 12:48:37 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Thu Aug 04 12:50:19 2022 +0200
1.3 @@ -48,7 +48,7 @@
1.4 \<close>
1.5 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
1.6
1.7 -Example "Diff_App/No.123 a"
1.8 +Example "Diff_App-No.123a"
1.9 Specification:
1.10 Model:
1.11 Given: \<open>Constants r = 7\<close>
1.12 @@ -69,7 +69,7 @@
1.13 \<close>
1.14 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
1.15
1.16 -Example "Diff_App/No.123 a"
1.17 +Example "Diff_App-No.123a"
1.18 Specification:
1.19 Model:
1.20 Given: \<open>Constants _\<close>
1.21 @@ -86,11 +86,11 @@
1.22 subsubsection \<open>Plain Example\<close>
1.23 text \<open>
1.24 This can occur in between text offering to start an interactive Calculation by using
1.25 - "Diff_App/No.123 a" as a link.
1.26 + "Diff_App-No.123a" as a link.
1.27 \<close>
1.28 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
1.29
1.30 -Example "Diff_App/No.123 a"
1.31 +Example "Diff_App-No.123a"
1.32
1.33 (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
1.34
1.35 @@ -102,7 +102,7 @@
1.36 \<close>
1.37 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
1.38
1.39 -Example "Diff_App/No.123 a"
1.40 +Example "Diff_App-No.123a"
1.41 Problem "univariate_calculus/Optimisation"
1.42 Specification:
1.43 Solution:
1.44 @@ -119,7 +119,7 @@
1.45 \<close>
1.46 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
1.47
1.48 -Example "Diff_App/No.123 a"
1.49 +Example "Diff_App-No.123a"
1.50 Problem "univariate_calculus/Optimisation"
1.51 Specification:
1.52 Model:
1.53 @@ -193,7 +193,7 @@
1.54 in the repository.
1.55
1.56 The intermediate steps below will be deleted as soon as all above representations
1.57 - of Example "Diff_App/No.123 a" work out.
1.58 + of Example "Diff_App-No.123a" work out.
1.59 \<close>
1.60
1.61 subsubsection \<open>Complete Specification at once\<close>
2.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Thu Aug 04 12:48:37 2022 +0200
2.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Thu Aug 04 12:50:19 2022 +0200
2.3 @@ -6,7 +6,7 @@
2.4 text \<open>
2.5 Just a test, that this works also in $ISABELLE_ISAC_TEST
2.6 \<close>
2.7 -Example "Diff_App/No.123 a"
2.8 +Example "Diff_App-No.123a"
2.9 Specification:
2.10 Model:
2.11 Given: \<open>Constants [r = 7]\<close>
2.12 @@ -26,15 +26,15 @@
2.13
2.14 text \<open>
2.15 In an electronic textbook there shall be references to examples given, for instance,
2.16 - by \<open>Example "Diff_App/No.123 a"\<close>. Such a reference shall be easily "activated"
2.17 + by \<open>Example "Diff_App-No.123a"\<close>. Such a reference shall be easily "activated"
2.18 to start a Solution at the spot ?and?or? to open a separate window.
2.19
2.20 - Activating the reference \<open>Example "Diff_App/No.123 a"\<close> shall result in a threefold alternative,
2.21 + Activating the reference \<open>Example "Diff_App-No.123a"\<close> shall result in a threefold alternative,
2.22 where (2)=(3) for the parsers:
2.23 (1) the Example presents a "normal problem" with a Specification (preferred by engineers),
2.24 see above subsubsection \<open>Empty Specification\<close>,
2.25 (2) the Example presents a "normal problem" without a Specification (preferred in high-school):
2.26 - |Example "Diff_App/No.123 a"
2.27 + |Example "Diff_App-No.123a"
2.28 | Specification:
2.29 | Solution:
2.30 | ..first formula as given by the specifid Method..
2.31 @@ -62,7 +62,7 @@
2.32 ML \<open> (* # 1: At the first call of \<open>Example\<close> ISAC initialises a calculation *)
2.33 val p = ([], Pos.Pbl);
2.34 val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*)
2.35 -("Diff_App/No.123 a",
2.36 +("Diff_App-No.123a",
2.37 (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too:
2.38 Constants [r = 7] *)
2.39 ( [("#Given", ["Constants [r = 7]"]),
2.40 @@ -77,7 +77,7 @@
2.41 ) Ctree.EmptyPtree;
2.42 val ptp = (pt, p);
2.43 \<close>
2.44 -Example "Diff_App/No.123 a"
2.45 +Example "Diff_App-No.123a"
2.46 Specification:
2.47 Model:
2.48 Given: \<open>Constants [r = 7]\<close>
2.49 @@ -99,7 +99,7 @@
2.50 val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp))
2.51 = Step.specify_do_next ptp;
2.52 \<close>
2.53 -Example "Diff_App/No.123 a"
2.54 +Example "Diff_App-No.123a"
2.55 Specification:
2.56 Model:
2.57 Given: \<open>Constants r = 7\<close>
2.58 @@ -122,7 +122,7 @@
2.59 val ("ok", ([(Tactic.Add_Find "Maximum A", _, _)], _, ptp))
2.60 = Step.specify_do_next ptp;
2.61 \<close>
2.62 -Example "Diff_App/No.123 a"
2.63 +Example "Diff_App-No.123a"
2.64 Specification:
2.65 Model:
2.66 Given: \<open>Constants r = 7\<close>
2.67 @@ -145,7 +145,7 @@
2.68 = Step.specify_do_next ptp;
2.69 \<close>
2.70
2.71 -Example "Diff_App/No.123 a"
2.72 +Example "Diff_App-No.123a"
2.73 Specification:
2.74 Model:
2.75 Given: \<open>Constants r = 7\<close>
2.76 @@ -165,7 +165,7 @@
2.77 \<close>
2.78 ML \<open> (* # 5: Input to \<open>Problem_Ref\<close> might change the \<open>Model\<close> *)
2.79 \<close>
2.80 -Example "Diff_App/No.123 a"
2.81 +Example "Diff_App-No.123a"
2.82 Specification:
2.83 Model:
2.84 Given: \<open>Constants r = 7\<close>
2.85 @@ -188,7 +188,7 @@
2.86 ML \<open> (* # 6: Input to \<open>Method_Ref\<close> changes the \<open>Model\<close> to the respective \<open>Method\<close> *)
2.87 \<close>
2.88 text \<open> --- remove this line and make content Isar input---\
2.89 -Example "Diff_App/No.123 a"
2.90 +Example "Diff_App-No.123a"
2.91 Specification:
2.92 Model: GOON: lookup model of method GOON GOON GOON GOON GOON!
2.93 Given: \<open>Constants r = 7\<close>