1.1 --- a/src/Tools/isac/Interpret/appl.sml	Fri Apr 15 17:07:34 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Sat Apr 16 10:19:45 2011 +0200
     1.3 @@ -343,7 +343,17 @@
     1.4    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  
     1.5      then Notappl ((tac2str (Apply_Method mI))^
     1.6  	   " not for pos "^(pos'2str (p,p_)))
     1.7 -  else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), e_ctxt))
     1.8 +  else let
     1.9 +    val (PblObj{origin = (_, (dI, pI, _), _), probl, ...}) = get_obj I pt p;
    1.10 +    val {where_, ...} = get_pbt pI
    1.11 +    val pres = map (mk_env probl |> subst_atomic) where_
    1.12 +    val ctxt = assoc_thy dI |> ProofContext.init_global 
    1.13 +          |> insert_assumptions pres
    1.14 +    (*TODO.WN110416 here evalprecond according to fun check_preconds'
    1.15 +      and then decide on Notappl/Appl once more.
    1.16 +      Implement after all tests are running, since this changes
    1.17 +      overall system behavior*)
    1.18 +  in Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
    1.19  
    1.20    | applicable_in (p,p_) pt (Check_Postcond pI) =
    1.21    if member op = [Pbl,Met] p_                  

     2.1 --- a/test/Tools/isac/Interpret/appl.sml	Fri Apr 15 17:07:34 2011 +0200
     2.2 +++ b/test/Tools/isac/Interpret/appl.sml	Sat Apr 16 10:19:45 2011 +0200
     2.3 @@ -2,3 +2,46 @@
     2.4     Author: Walther Neuper 110320
     2.5     (c) copyright due to lincense terms.
     2.6  *)
     2.7 +
     2.8 +"-----------------------------------------------------------------";
     2.9 +"table of contents -----------------------------------------------";
    2.10 +"-----------------------------------------------------------------";
    2.11 +"-------------- fun applicable_in..Apply_Method ------------------";
    2.12 +"-----------------------------------------------------------------";
    2.13 +"-----------------------------------------------------------------";
    2.14 +"-----------------------------------------------------------------";
    2.15 +
    2.16 +
    2.17 +"-------------- fun applicable_in..Apply_Method ------------------";
    2.18 +"-------------- fun applicable_in..Apply_Method ------------------";
    2.19 +"-------------- fun applicable_in..Apply_Method ------------------";
    2.20 +val fmz = ["equality (x+1=(2::real))",
    2.21 +	   "solveFor (x::real)","solutions L"];
    2.22 +val (dI',pI',mI') =
    2.23 +  ("Test",["sqroot-test","univariate","equation","test"],
    2.24 +   ["Test","squ-equ-test-subpbl1"]);
    2.25 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    2.26 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    2.27 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    2.28 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    2.29 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    2.30 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    2.31 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    2.32 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    2.33 +
    2.34 +val (PblObj{origin = (_, (dI, pI, _), _), probl, ...}) = get_obj I pt (fst p);
    2.35 +val {where_, ...} = get_pbt pI;
    2.36 +val where_ = [str2term "(lhs e_e) is_poly_in v_v"];(*just for test<>[]*)
    2.37 +val pres = map (mk_env probl |> subst_atomic) where_;
    2.38 +(*val pres = mk_env pbl |> subst_atomic #> where_;*)
    2.39 +if pres = [str2term "lhs (x + 1 = 2) is_poly_in x"] then ()
    2.40 +else error "appl.sml Apply_Method diff.behav.";
    2.41 +
    2.42 +val ctxt = assoc_thy dI |> ProofContext.init_global |> insert_assumptions pres;
    2.43 +(*TODO.WN110416 read pres from ctxt and check*)
    2.44 +
    2.45 +(*========== inhibit exn 110415 ================================================
    2.46 +
    2.47 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    2.48 +show_pt pt;
    2.49 +============ inhibit exn 110415 ==============================================*)

     3.1 --- a/test/Tools/isac/Test_Some.thy	Fri Apr 15 17:07:34 2011 +0200
     3.2 +++ b/test/Tools/isac/Test_Some.thy	Sat Apr 16 10:19:45 2011 +0200
     3.3 @@ -36,8 +36,8 @@
     3.4  
     3.5  
     3.6  *}
     3.7 -
     3.8 -use"../../../test/Tools/isac/Interpret/mstools.sml"
     3.9 +ML {*print_depth 999*}
    3.10 +use"../../../test/Tools/isac/Interpret/appl.sml"
    3.11  
    3.12  end
    3.13  
    3.14 @@ -46,12 +46,12 @@
    3.15  ===== inhibit exn ?===========================================================*)
    3.16  
    3.17  
    3.18 -(*========== inhibit exn 110317 ================================================
    3.19 +(*========== inhibit exn 110415 ================================================
    3.20  
    3.21  "########### testcode inserted vvv ###########################################";
    3.22  "########### testcode inserted ^^^ ###########################################";
    3.23  
    3.24 -============ inhibit exn 110317 ==============================================*)
    3.25 +============ inhibit exn 110415 ==============================================*)
    3.26  
    3.27  
    3.28  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.