details on 632d2ecab96f: error (from <NEXT> on new Worksheet)
authorWalther Neuper <neuper@ist.tugraz.at>
Sat, 31 May 2014 15:09:33 +0200
changeset 55415f8d44cb86330
parent 55414 8274d078f94c
child 55416 3a5c99035930
details on 632d2ecab96f: error (from <NEXT> on new Worksheet)

# inform.sml: fetchErrorpatterns causes same behaviour in Test_Isac;
so the hack has been undone, since it doesn't work anymore.
# tackling the error is postponed to removing "! thehier"

Test_Isac works for e_rls and list_rls in fetchErrorpatterns
src/Tools/isac/Interpret/inform.sml
test/Tools/isac/Interpret/mathengine.sml
test/Tools/isac/xmlsrc/thy-hierarchy.sml
     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 +