1.1 --- a/src/Tools/isac/calcelems.sml Sat Feb 10 15:12:59 2018 +0100
1.2 +++ b/src/Tools/isac/calcelems.sml Sat Feb 10 16:21:12 2018 +0100
1.3 @@ -1094,7 +1094,7 @@
1.4 let
1.5 val allthys = Theory.ancestors_of (Thy_Info_get_theory "Build_Thydata")
1.6 in
1.7 - drop ((find_index (curry Context.eq_thy (Thy_Info_get_theory "Complex_Main")) allthys), allthys)
1.8 + drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)
1.9 end
1.10 fun knowthys () = (*["Isac", .., "Descript", "Delete"]*)
1.11 let
1.12 @@ -1105,7 +1105,7 @@
1.13 Thy_Info_get_theory "xmlsrc", Thy_Info_get_theory "Frontend"])
1.14 (Theory.ancestors_of (Thy_Info_get_theory "Build_Thydata"))
1.15 in
1.16 - take ((find_index (curry Context.eq_thy (Thy_Info_get_theory "Complex_Main")) allthys),
1.17 + take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
1.18 allthys)
1.19 end
1.20 val isacthys' = isacthys ()
1.21 @@ -1122,7 +1122,7 @@
1.22 Thy_Info_get_theory "xmlsrc", Thy_Info_get_theory "Frontend"])
1.23 (Theory.ancestors_of (Thy_Info_get_theory "Build_Thydata"))
1.24 in
1.25 - take ((find_index (curry Context.eq_thy (Thy_Info_get_theory "Complex_Main")) allthys),
1.26 + take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
1.27 allthys)
1.28 end
1.29 val isacthys' = isacthys ()
2.1 --- a/test/Tools/isac/Interpret/rewtools.sml Sat Feb 10 15:12:59 2018 +0100
2.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Sat Feb 10 16:21:12 2018 +0100
2.3 @@ -13,6 +13,7 @@
2.4 "table of contents --------------------------------------";
2.5 "--------------------------------------------------------";
2.6 "----------- fun thy_containing_rls ---------------------";
2.7 +"----------- apply thy_containing_rls -------------------";
2.8 "----------- fun thy_containing_cal ---------------------";
2.9 "----------- initContext Thy_ Integration-demo ----------";
2.10 "----------- initContext..Thy_, fun context_thm ---------";
2.11 @@ -37,6 +38,39 @@
2.12 "----------- fun thy_containing_rls ---------------------";
2.13 "----------- fun thy_containing_rls ---------------------";
2.14 "----------- fun thy_containing_rls ---------------------";
2.15 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
2.16 +if thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
2.17 +else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
2.18 +;
2.19 +"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie", "norm_Poly");
2.20 + val thy = Thy_Info_get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)
2.21 +val xxx = AList.lookup op= (KEStore_Elems.get_rlss thy) rls';
2.22 +val SOME (thy'', _) = xxx;
2.23 +val SOME ("Poly", _) = xxx;
2.24 +if thy'' = "Poly" then () else error "--- fun thy_containing_rls: changed";
2.25 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" *)
2.26 +if partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"
2.27 +;
2.28 +"~~~~~ fun partID', args:"; val (thy') = (thy');
2.29 +Thy_Info_get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)
2.30 +;
2.31 +"~~~~~ fun partID, args:"; val (thy) = (Thy_Info_get_theory thy');
2.32 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
2.33 +knowthys ()
2.34 +;
2.35 +"~~~~~ fun knowthys, args:"; val () = ();
2.36 + val allthys = filter_out (member Context.eq_thy
2.37 + [(*Thy_Info_get_theory "ProgLang",*) Thy_Info_get_theory "Interpret",
2.38 + Thy_Info_get_theory "xmlsrc", Thy_Info_get_theory "Frontend"])
2.39 + (Theory.ancestors_of (Thy_Info_get_theory "Build_Thydata"));
2.40 +length allthys = 152; (*in Isabelle2015/Isac*)
2.41 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"
2.42 +Thy_Info_get_theory "Complex_Main";*)
2.43 +Thy_Info.get_theory "Complex_Main";;
2.44 +
2.45 +"----------- apply thy_containing_rls -------------------";
2.46 +"----------- apply thy_containing_rls -------------------";
2.47 +"----------- apply thy_containing_rls -------------------";
2.48 if thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
2.49 else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
2.50 ;
3.1 --- a/test/Tools/isac/Test_Isac.thy Sat Feb 10 15:12:59 2018 +0100
3.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Feb 10 16:21:12 2018 +0100
3.3 @@ -40,6 +40,14 @@
3.4 this is status for coding this is status for tests
3.5 \<close>
3.6
3.7 +section \<open>code for copy & paste\<close>
3.8 +text \<open>
3.9 +"~~~~~ fun , args:"; val () = ();
3.10 +"~~~~~ and , args:"; val () = ();
3.11 +
3.12 +"~~~~~ to return val:"; val () = ();
3.13 +
3.14 +\<close>
3.15 section \<open>Run the tests\<close>
3.16 text \<open>
3.17 * say "OK" to the popup asking for theories to be loaded
3.18 @@ -96,7 +104,11 @@
3.19 open Model; (* NONE *)
3.20 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.21 *}
3.22 +(*---------------------- check test file by testfile -------------------------------------------
3.23 + ---------------------- check test file by testfile -------------------------------------------*)
3.24 +
3.25 ML {*
3.26 +"~~~~~ fun xxx, args:"; val () = ();
3.27 *} ML {*
3.28 *} ML {*
3.29 *}
3.30 @@ -128,8 +140,8 @@
3.31 ML_file "ProgLang/scrtools.sml"
3.32 ML_file "ProgLang/tools.sml"
3.33 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
3.34 + ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
3.35 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
3.36 - ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
3.37 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
3.38 ML_file "Minisubpbl/000-comments.sml"
3.39 ML_file "Minisubpbl/100-init-rootpbl.sml"
3.40 @@ -143,8 +155,9 @@
3.41 ML_file "Minisubpbl/600-postcond.sml"
3.42 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
3.43 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
3.44 -(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
3.45 ML_file "Interpret/mstools.sml"
3.46 +
3.47 +
3.48 ML_file "Interpret/ctree.sml" (*!...!see(25)*)
3.49 ML_file "Interpret/ptyps.sml" (* requires setup from ptyps.thy *)
3.50 ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
3.51 @@ -156,6 +169,14 @@
3.52 ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
3.53 ML_file "Interpret/rewtools.sml"
3.54 ML_file "Interpret/script.sml"
3.55 +
3.56 +ML {*
3.57 +"~~~~~ fun xxx, args:"; val () = ();
3.58 +*} ML {*
3.59 +*} ML {*
3.60 +*}
3.61 +
3.62 +(*---------------------- check test file by testfile -------------------------------------------
3.63 ML_file "Interpret/solve.sml"
3.64 ML_file "Interpret/inform.sml"
3.65 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
3.66 @@ -219,11 +240,11 @@
3.67 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
3.68 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
3.69 ML {*"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";*}
3.70 + ---------------------- check test file by testfile -------------------------------------------*)
3.71
3.72 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
3.73 ML {*"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";*}
3.74 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
3.75 - ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
3.76
3.77 section {* history of tests *}
3.78 text {*