no \<^isac_test> guard for test material: thus the Prover IDE does not have to switch the option "isac_test";
1.1 --- a/test/Tools/isac/Test_Isac.thy Mon Apr 19 18:05:01 2021 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Apr 19 19:55:31 2021 +0200
1.3 @@ -96,9 +96,6 @@
1.4
1.5 ML \<open>open ML_System\<close>
1.6 ML \<open>
1.7 -\<^isac_test>\<open>
1.8 - (* these vvv test, if funs are intermediately opened in structure
1.9 - in case of errors here consider ~~/xtest-to-coding.sh *)
1.10 open Kernel;
1.11 open Math_Engine;
1.12 open Test_Code; CalcTreeTEST;
1.13 @@ -143,7 +140,6 @@
1.14 open Rewrite_Ord
1.15 open UnparseC
1.16 \<close>
1.17 -\<close>
1.18 ML_file "BaseDefinitions/libraryC.sml"
1.19
1.20 section \<open>code for copy & paste ===============================================================\<close>
2.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Apr 19 18:05:01 2021 +0200
2.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Apr 19 19:55:31 2021 +0200
2.3 @@ -95,9 +95,6 @@
2.4
2.5 ML \<open>open ML_System\<close>
2.6 ML \<open>
2.7 -\<^isac_test>\<open>
2.8 - (* these vvv test, if funs are intermediately opened in structure
2.9 - in case of errors here consider ~~/xtest-to-coding.sh *)
2.10 open Kernel;
2.11 open Math_Engine;
2.12 open Test_Code; CalcTreeTEST;
2.13 @@ -142,7 +139,6 @@
2.14 open Rewrite_Ord
2.15 open UnparseC
2.16 \<close>
2.17 -\<close>
2.18
2.19 ML \<open>
2.20 "~~~~~ fun xxx , args:"; val () = ();
3.1 --- a/test/Tools/isac/Test_Some.thy Mon Apr 19 18:05:01 2021 +0200
3.2 +++ b/test/Tools/isac/Test_Some.thy Mon Apr 19 19:55:31 2021 +0200
3.3 @@ -4,9 +4,6 @@
3.4
3.5 ML \<open>open ML_System\<close>
3.6 ML \<open>
3.7 -\<^isac_test>\<open>
3.8 - (* these vvv test, if funs are intermediately opened in structure
3.9 - in case of errors here consider ~~/xtest-to-coding.sh *)
3.10 open Kernel;
3.11 open Math_Engine;
3.12 open Test_Code; CalcTreeTEST;
3.13 @@ -51,7 +48,6 @@
3.14 open Rewrite_Ord
3.15 open UnparseC
3.16 \<close>
3.17 -\<close>
3.18 ML_file "BridgeJEdit/parseC.sml"
3.19
3.20 section \<open>code for copy & paste ===============================================================\<close>
4.1 --- a/test/Tools/isac/Test_Some_meld.thy Mon Apr 19 18:05:01 2021 +0200
4.2 +++ b/test/Tools/isac/Test_Some_meld.thy Mon Apr 19 19:55:31 2021 +0200
4.3 @@ -1,9 +1,6 @@
4.4 theory Test_Some_meld imports Isac.Build_Thydata
4.5 begin
4.6 ML \<open>
4.7 -\<^isac_test>\<open>
4.8 - (* these vvv test, if funs are intermediately opened in structure
4.9 - in case of errors here consider ~~/xtest-to-coding.sh *)
4.10 open Kernel;
4.11 open Math_Engine;
4.12 open LItool; arguments_from_model;
4.13 @@ -27,7 +24,6 @@
4.14 open TermC; atomt;
4.15 open Rule; ThmC.string_of_thm;
4.16 \<close>
4.17 -\<close>
4.18 ML_file "BaseDefinitions/libraryC.sml"
4.19
4.20 section \<open>code for copy & paste ===============================================================\<close>