1.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sun Apr 18 16:30:11 2021 +0200
1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Apr 18 18:30:31 2021 +0200
1.3 @@ -5,8 +5,8 @@
1.4 Isac's tests are organised parallel to sources:
1.5 $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
1.6 plus
1.7 - $ISABELLE_ISAC_TEST/ADDTESTS
1.8 - $ISABELLE_ISAC_TEST/Minisubpbl: the Lucas-Interpreter's core functionality
1.9 + $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS
1.10 + $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
1.11
1.12 Note, that only the first error in a file is shown here.
1.13 *)
1.14 @@ -61,31 +61,31 @@
1.15 and find out, which ML_file or *.thy causes an error (might be ONLY one).
1.16 Also backup files (#* ) recognised by jEdit cause this trouble *)
1.17 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
1.18 - "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"
1.19 -(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Ctxt"
1.20 -(**)"$ISABELLE_ISAC_TEST/ADDTESTS/test-depend/Build_Test"
1.21 -(**)"$ISABELLE_ISAC_TEST/ADDTESTS/All_Ctxt"
1.22 -(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Test_Units"
1.23 -(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T1_Basics"
1.24 -(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T2_Rewriting"
1.25 -(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T3_MathEngine"
1.26 -(**)"$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/BuildC_Test"
1.27 -(**)"$ISABELLE_ISAC_TEST/ADDTESTS/session-get_theory/Foo"
1.28 + "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"
1.29 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
1.30 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
1.31 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
1.32 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
1.33 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
1.34 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
1.35 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
1.36 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
1.37 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
1.38 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
1.39 ADDTESTS/------------------------------------------- see end of tests *)
1.40 (*/--- these work directly from Pure, but create problems here ..
1.41 - "~~/test/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
1.42 - "~~/test/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
1.43 - "~~/test/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
1.44 - "~~/test/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
1.45 - "~~/test/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
1.46 + "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
1.47 + "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
1.48 + "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
1.49 + "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
1.50 + "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
1.51 \--- .. these work independently, but create problems here *)
1.52 -(**)"~~/test/Pure/Isar/Test_Parsers"
1.53 -(**)"~~/test/HOL/Tools/Sledgehammer/Try_Sledgehammer"
1.54 +(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"
1.55 +(**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"
1.56 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
1.57 - "$ISABELLE_ISAC_TEST/Specify/refine" (* setup for refine.sml *)
1.58 - "$ISABELLE_ISAC_TEST/ProgLang/calculate" (* setup for evaluate.sml *)
1.59 - "$ISABELLE_ISAC_TEST/Knowledge/integrate" (* setup for integrate.sml*)
1.60 + "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
1.61 + "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
1.62 + "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
1.63 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
1.64 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*)
1.65 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) Test_Isac_Short*)
1.66 @@ -175,10 +175,10 @@
1.67 ---------------------- check test file by testfile -------------------------------------------*)
1.68 section \<open>trials with Isabelle's functions\<close>
1.69 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.70 - ML_file "~~/test/Pure/General/alist.ML"
1.71 - ML_file "~~/test/Pure/General/basics.ML"
1.72 - ML_file "~~/test/Pure/General/scan.ML"
1.73 - ML_file "~~/test/Pure/PIDE/xml.ML"
1.74 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
1.75 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
1.76 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
1.77 + ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
1.78 ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.79
1.80 section \<open>test ML Code of isac\<close>
1.81 @@ -330,8 +330,8 @@
1.82
1.83 section \<open>further tests additional to src/.. files\<close>
1.84 ML_file "BridgeLibisabelle/use-cases.sml"
1.85 - ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/mini-test.sml"
1.86 - ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/protocol.sml"
1.87 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
1.88 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
1.89
1.90 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.91 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>