1.1 --- a/src/Tools/isac/Interpret/ptyps.sml	Sat Jan 25 21:06:58 2014 +0100
     1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml	Sun Jan 26 01:37:36 2014 +0100
     1.3 @@ -353,10 +353,10 @@
     1.4            if k0 = k'' then app_py' ks ps else app_py' k' ps';
     1.5    in app_py' k p end;
     1.6  
     1.7 -fun extract_py (Ptyp (_, [py], _)) = py
     1.8 -  | extract_py _ = error ("extract_py: Ptyp has wrong format.");
     1.9 -
    1.10 -fun get_py p = app_py p extract_py;
    1.11 +fun get_py p = let
    1.12 +        fun extract_py (Ptyp (_, [py], _)) = py
    1.13 +          | extract_py _ = error ("extract_py: Ptyp has wrong format.");
    1.14 +      in app_py p extract_py end;
    1.15  
    1.16  (*> ptyps:= 
    1.17  [Ptyp ("1",[("ptyp 1",([],[]))],
    1.18 @@ -463,7 +463,7 @@
    1.19  
    1.20  (*.the pblID has the leaf-element as first; better readability achieved;.*)
    1.21  fun store_pbt (pbt as {guh,...}, pblID) = 
    1.22 -    (if (!check_guhs_unique) then check_pblguh_unique guh (get_ptyps ()) else ();
    1.23 +    (if (!check_guhs_unique) then check_pblguh_unique guh (! ptyps) else ();
    1.24       ptyps:= insrt pblID pbt (rev pblID) (! ptyps));
    1.25  
    1.26  (*.the metID has the root-element as first; compare 'fun store_pbt'.*)

     2.1 --- a/src/Tools/isac/KEStore.thy	Sat Jan 25 21:06:58 2014 +0100
     2.2 +++ b/src/Tools/isac/KEStore.thy	Sun Jan 26 01:37:36 2014 +0100
     2.3 @@ -69,7 +69,7 @@
     2.4      );
     2.5    fun get_ptyps thy = Data.get thy;
     2.6    fun store_pbts pbts = let
     2.7 -          fun store_pbts' (pbt, pblID) = ((*map writeln pblID;*) rev pblID |> insrt pblID pbt)
     2.8 +          fun store_pbts' (pbt, pblID) = rev pblID |> insrt pblID pbt;
     2.9          in fold store_pbts' pbts |> Data.map end;
    2.10  
    2.11    (*etc*)
    2.12 @@ -111,7 +111,8 @@
    2.13  
    2.14  fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
    2.15  
    2.16 -fun get_ptyps () = ! ptyps (*KEStore_Elems.get_ptyps @{theory}*);
    2.17 +fun get_ptyps () = ! ptyps (*Thy_Info.get_theory "Isac" |> KEStore_Elems.get_ptyps*);
    2.18 +val store_pbts = KEStore_Elems.store_pbts;
    2.19  *}
    2.20  setup {* KEStore_Elems.add_rlss 
    2.21    [("e_rls", (Context.theory_name @{theory}, e_rls)), 

     3.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sat Jan 25 21:06:58 2014 +0100
     3.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sun Jan 26 01:37:36 2014 +0100
     3.3 @@ -292,7 +292,7 @@
     3.4          specification of this equation type.*}
     3.5          
     3.6  ML {*
     3.7 -  match_pbl fmz (get_pbt 
     3.8 +  match_pbl fmz (get_pbt
     3.9      ["abcFormula","degree_2","polynomial","univariate","equation"]);
    3.10  *}
    3.11  
    3.12 @@ -892,6 +892,10 @@
    3.13     (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
    3.14     (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
    3.15  *}
    3.16 +setup {* store_pbts
    3.17 +  [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, []),
    3.18 +    prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
    3.19 +      (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])] *}
    3.20  
    3.21  text{*\noindent For the suddenly created node we have to define the input
    3.22         and output parameters. We already prepared their definition in
    3.23 @@ -906,8 +910,17 @@
    3.24      ],
    3.25      append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
    3.26      [["SignalProcessing","Z_Transform","Inverse"]]));
    3.27 -
    3.28 -  show_ptyps();
    3.29 +*}
    3.30 +setup {* store_pbts
    3.31 +  [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
    3.32 +      (["Inverse", "Z_Transform", "SignalProcessing"],
    3.33 +        [("#Given", ["filterExpression X_eq"]),
    3.34 +          ("#Find", ["stepResponse n_eq"])],
    3.35 +        append_rls "e_rls" e_rls [(*for preds in where_*)],
    3.36 +        NONE,
    3.37 +        [["SignalProcessing","Z_Transform","Inverse"]])] *}
    3.38 +ML {*
    3.39 +  show_ptyps ();
    3.40    get_pbt ["Inverse","Z_Transform","SignalProcessing"];
    3.41  *}
    3.42  

     4.1 --- a/test/Tools/isac/Interpret/ptyps.sml	Sat Jan 25 21:06:58 2014 +0100
     4.2 +++ b/test/Tools/isac/Interpret/ptyps.sml	Sun Jan 26 01:37:36 2014 +0100
     4.3 @@ -142,7 +142,7 @@
     4.4  
     4.5  i.e. there is no common fun for pbls and mets ?!?*)
     4.6  
     4.7 -coll_pblguhs (!ptyps);
     4.8 +coll_pblguhs (get_ptyps ());
     4.9  sort string_ord (coll_pblguhs (get_ptyps ()));
    4.10  show_pblguhs ();
    4.11  sort_pblguhs ();

     5.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml	Sat Jan 25 21:06:58 2014 +0100
     5.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml	Sun Jan 26 01:37:36 2014 +0100
     5.3 @@ -65,6 +65,16 @@
     5.4  			  eval_is_rootequation_in "")],
     5.5    [("Test","methode")]));
     5.6  
     5.7 +store_pbts
     5.8 +  [prep_pbt (*Test.thy*) (theory "Isac")
     5.9 +      (["root'","univariate","equation","test"],
    5.10 +        [("#Given" ,["equality e_e","solveFor v_v"]),
    5.11 +          ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),
    5.12 +          ("#Find"  ,["solutions v_i_"])],
    5.13 +        append_rls e_rls [Calc ("Test.is'_rootequation'_in", eval_is_rootequation_in "")],
    5.14 +        [("Test","methode")])]
    5.15 +  thy;
    5.16 +
    5.17  match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["root'","univariate","equation","test"]); 
    5.18  
    5.19  
    5.20 @@ -80,6 +90,15 @@
    5.21    append_rls e_rls [Calc ("Tools.matches",eval_matches "#matches_")],
    5.22    []));
    5.23  
    5.24 +store_pbts
    5.25 +  [prep_pbt (theory "Isac")
    5.26 +      (["approximate","univariate","equation","test"],
    5.27 +        [("#Given", ["equality e_e","solveFor v_v","errorBound err_"]),
    5.28 +          ("#Where", ["matches (?a = ?b) e_e"]),
    5.29 +          ("#Find", ["solutions v_i_"])],
    5.30 +        append_rls e_rls [Calc ("Tools.matches",eval_matches "#matches_")], [])]
    5.31 +  thy;
    5.32 +
    5.33  methods:= overwritel (!methods,
    5.34  [
    5.35   prep_met

     6.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml	Sat Jan 25 21:06:58 2014 +0100
     6.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml	Sun Jan 26 01:37:36 2014 +0100
     6.3 @@ -31,6 +31,17 @@
     6.4     ("#Find"  ,["realTestFind f_"])
     6.5    ],
     6.6    e_rls, NONE, []));
     6.7 +
     6.8 +store_pbts
     6.9 +  [prep_pbt Test.thy "pbl_testss" [] e_pblID
    6.10 +      (["tests"], []:(string * string list) list, e_rls, NONE, []),
    6.11 +    prep_pbt Test.thy "pbl_testss_term" [] e_pblID
    6.12 +      (["met_testterm","tests"],
    6.13 +        [("#Given" ,["realTestGiven g_"]),
    6.14 +          ("#Find"  ,["realTestFind f_"])],
    6.15 +        e_rls, NONE, [])]
    6.16 +  thy;
    6.17 +
    6.18  store_met
    6.19   (prep_met Test.thy "met_test_simp" [] e_metID
    6.20   (*test for simplification*)
    6.21 @@ -98,6 +109,13 @@
    6.22     ("#Find"  ,["boolTestFind v_i_"])
    6.23    ],
    6.24    e_rls, NONE, []));
    6.25 +store_pbts
    6.26 +  [prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
    6.27 +      (["met_testeq","tests"],
    6.28 +        [("#Given" ,["boolTestGiven e_e"]),
    6.29 +          ("#Find"  ,["boolTestFind v_i_"])],
    6.30 +        e_rls, NONE, [])]
    6.31 +  thy;
    6.32  
    6.33  store_met
    6.34   (prep_met Test.thy "met_test_eq1" [] e_metID

     7.1 --- a/test/Tools/isac/Test_Isac.thy	Sat Jan 25 21:06:58 2014 +0100
     7.2 +++ b/test/Tools/isac/Test_Isac.thy	Sun Jan 26 01:37:36 2014 +0100
     7.3 @@ -50,6 +50,15 @@
     7.4    ML_file          "calcelems.sml"
     7.5    ML_file          "kestore.sml"
     7.6    ML_file "ProgLang/termC.sml"
     7.7 +
     7.8 +  setup {* store_pbts
     7.9 +    [prep_pbt @{theory "Test"} "pbl_ttest" [] e_pblID (["test"], [], e_rls, NONE, []),
    7.10 +      prep_pbt @{theory "Test"} "pbl_ttest_calc" [] e_pblID
    7.11 +        (["calculate","test"],
    7.12 +          [("#Given" ,["realTestGiven t_t"]),
    7.13 +            ("#Find"  ,["realTestFind s_s"])],
    7.14 +          e_rls, NONE, [["Test","test_calculate"]])] *}
    7.15 +
    7.16    ML_file "ProgLang/calculate.sml"
    7.17    ML_file "ProgLang/rewrite.sml"
    7.18    ML_file "ProgLang/listC.sml"