# HG changeset patch
# User wneuper <Walther.Neuper@jku.at>
# Date 1659610219 -7200
# Node ID 851c82618f2e3627a843569dc9aa511c948dd5cc
# Parent  2e0b7ca391dc4e7218e772400f7ea8ff3c850dd0
cleanup Example.id

diff -r 2e0b7ca391dc -r 851c82618f2e src/Tools/isac/BridgeJEdit/VSCode_Example.thy
--- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy	Thu Aug 04 12:48:37 2022 +0200
+++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy	Thu Aug 04 12:50:19 2022 +0200
@@ -48,7 +48,7 @@
 \<close>
 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
 
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Specification:
     Model:
       Given: \<open>Constants r = 7\<close>
@@ -69,7 +69,7 @@
 \<close>
 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
 
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Specification:
     Model:
       Given: \<open>Constants _\<close>
@@ -86,11 +86,11 @@
 subsubsection \<open>Plain Example\<close>
 text \<open>
   This can occur in between text offering to start an interactive Calculation by using
-  "Diff_App/No.123 a" as a link.
+  "Diff_App-No.123a" as a link.
 \<close>
 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
 
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
 
        (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
 
@@ -102,7 +102,7 @@
 \<close>
 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
 
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Problem "univariate_calculus/Optimisation"
     Specification:
     Solution:
@@ -119,7 +119,7 @@
 \<close>
 text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
 
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Problem "univariate_calculus/Optimisation"
     Specification:
       Model:
@@ -193,7 +193,7 @@
   in the repository.
 
   The intermediate steps below will be deleted as soon as all above representations 
-  of Example "Diff_App/No.123 a" work out.
+  of Example "Diff_App-No.123a" work out.
 \<close>
 
 subsubsection \<open>Complete Specification at once\<close>
diff -r 2e0b7ca391dc -r 851c82618f2e test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy
--- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Thu Aug 04 12:48:37 2022 +0200
+++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Thu Aug 04 12:50:19 2022 +0200
@@ -6,7 +6,7 @@
 text \<open>
   Just a test, that this works also in $ISABELLE_ISAC_TEST
 \<close>
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Specification:
     Model:
       Given: \<open>Constants [r = 7]\<close>
@@ -26,15 +26,15 @@
 
 text \<open>
   In an electronic textbook there shall be references to examples given, for instance,
-  by \<open>Example "Diff_App/No.123 a"\<close>. Such a reference shall be easily "activated" 
+  by \<open>Example "Diff_App-No.123a"\<close>. Such a reference shall be easily "activated" 
   to start a Solution at the spot ?and?or? to open a separate window.
 
-  Activating the reference \<open>Example "Diff_App/No.123 a"\<close> shall result in a threefold alternative,
+  Activating the reference \<open>Example "Diff_App-No.123a"\<close> shall result in a threefold alternative,
   where (2)=(3) for the parsers:
   (1) the Example presents a "normal problem" with a Specification (preferred by engineers),
     see above subsubsection \<open>Empty Specification\<close>,
   (2) the Example presents a "normal problem" without a Specification (preferred in high-school):
-    |Example "Diff_App/No.123 a"
+    |Example "Diff_App-No.123a"
     |  Specification:
     |  Solution:
     |    ..first formula as given by the specifid Method..
@@ -62,7 +62,7 @@
 ML \<open> (* # 1: At the first call of \<open>Example\<close> ISAC initialises a calculation *)
 val p = ([], Pos.Pbl);
 val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*)
-("Diff_App/No.123 a", 
+("Diff_App-No.123a", 
     (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too:
                  Constants [r = 7] *)
   ( [("#Given", ["Constants [r = 7]"]),
@@ -77,7 +77,7 @@
 ) Ctree.EmptyPtree;
 val ptp = (pt, p);
 \<close>
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Specification:
     Model:
       Given: \<open>Constants [r = 7]\<close>
@@ -99,7 +99,7 @@
 val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp))
   = Step.specify_do_next ptp;
 \<close>
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Specification:
     Model:
       Given: \<open>Constants r = 7\<close>
@@ -122,7 +122,7 @@
 val ("ok", ([(Tactic.Add_Find "Maximum A", _, _)], _, ptp))
   = Step.specify_do_next ptp;
 \<close>
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Specification:
     Model:
       Given: \<open>Constants r = 7\<close>
@@ -145,7 +145,7 @@
   = Step.specify_do_next ptp;
 \<close>
 
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Specification:
     Model:
       Given: \<open>Constants r = 7\<close>
@@ -165,7 +165,7 @@
 \<close> 
 ML \<open> (* # 5: Input to \<open>Problem_Ref\<close> might change the \<open>Model\<close> *)
 \<close>
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Specification:
     Model:
       Given: \<open>Constants r = 7\<close>
@@ -188,7 +188,7 @@
 ML \<open> (* # 6: Input to \<open>Method_Ref\<close> changes the \<open>Model\<close> to the respective \<open>Method\<close> *)
 \<close>
 text \<open> --- remove this line and make content Isar input---\
-Example "Diff_App/No.123 a"
+Example "Diff_App-No.123a"
   Specification:
     Model:                                          GOON: lookup model of method GOON GOON GOON GOON GOON!
       Given: \<open>Constants r = 7\<close>