1.1 --- a/src/Tools/isac/Interpret/inform.sml Thu May 08 14:09:02 2014 +0200
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Sat May 31 15:09:33 2014 +0200
1.3 @@ -761,7 +761,7 @@
1.4 case tac of
1.5 Rewrite_Set rlsID => rlsID
1.6 | Rewrite_Set_Inst (_, rlsID) => rlsID
1.7 - | _ => "list_rls" (*WN120806 "e_rls" is appropriate, but raises exn 'get_pbt not found: ?!?*)
1.8 + | _ => "e_rls"
1.9 val (part, thyID) = thy_containing_rls "Isac" rlsID;
1.10 val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]
1.11 in case rls of
2.1 --- a/test/Tools/isac/Interpret/mathengine.sml Thu May 08 14:09:02 2014 +0200
2.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Sat May 31 15:09:33 2014 +0200
2.3 @@ -233,9 +233,15 @@
2.4 val _= upd_tacis cI tacis
2.5 val (tac,_,_) = last_elem tacis;
2.6 (*fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac);
2.7 -**************************************************************************
2.8 -ERROR: app_py: not found: ["IsacKnowledge","Tools","Rulesets","list_rls"]
2.9 -**************************************************************************)
2.10 + fetchErrorpatterns tac
2.11 +ERROR: app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
2.12 +"~~~~~ fun fetchErrorpatterns, args:"; val (tac) = (tac);
2.13 + val rlsID = "e_rls"
2.14 + val (part, thyID) = thy_containing_rls "Build_Thydata" rlsID;
2.15 +if part = "IsacKnowledge" andalso thyID = "KEStore" then ()
2.16 +else error "fetchErrorpatterns .. e_rls changed";
2.17 +(* val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]
2.18 +ERROR app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*)
2.19
2.20 "----------- fun step: Apply_Method without init_form ---";
2.21 "----------- fun step: Apply_Method without init_form ---";
3.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Thu May 08 14:09:02 2014 +0200
3.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Sat May 31 15:09:33 2014 +0200
3.3 @@ -26,6 +26,8 @@
3.4 "--------- (*collect_part: data too large for buffers*) ----------";
3.5 "----------- collect thydata from Test_Build_Thydata.thy ---------";
3.6 "----------- the_hier from Test_Build_Thydata.thy ----------------";
3.7 +"----------- correct theIDs for e_rls ----------------------------";
3.8 +"----------- correct theIDs for list_rls -------------------------";
3.9 "-----------------------------------------------------------------";
3.10 "-----------------------------------------------------------------";
3.11 "-----------------------------------------------------------------";
3.12 @@ -408,3 +410,25 @@
3.13 thenodes p [] [0] thydata2file (thehierTEST)
3.14 \------------------------- outcomment and adjust path -------------------------------/*)
3.15
3.16 +"----------- correct theIDs for e_rls ----------------------------";
3.17 +"----------- correct theIDs for e_rls ----------------------------";
3.18 +"----------- correct theIDs for e_rls ----------------------------";
3.19 +if thy_containing_rls "Build_Thydata" "e_rls" = ("IsacKnowledge", "KEStore") then ()
3.20 +else error "thy_containing_rls e_rls changed";
3.21 +show_thes ();
3.22 +(*shows different assignment for "e_rls"...
3.23 + :
3.24 + ["IsacScripts", "KEStore", "Rulesets", "e_rls"],
3.25 + :*)
3.26 +
3.27 +"----------- correct theIDs for list_rls -------------------------";
3.28 +"----------- correct theIDs for list_rls -------------------------";
3.29 +"----------- correct theIDs for list_rls -------------------------";
3.30 +if thy_containing_rls "Build_Thydata" "list_rls" = ("IsacKnowledge", "Tools") then ()
3.31 +else error "thy_containing_rls list_rls changed";
3.32 +show_thes ();
3.33 +(*shows different assignment for "list_rls"...
3.34 + :
3.35 + ["IsacScripts", "Tools", "Rulesets", "list_rls"],
3.36 + :*)
3.37 +