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

     2.1 --- a/src/Tools/isac/Interpret/solve.sml	Sat Apr 16 10:19:45 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/solve.sml	Mon Apr 18 14:43:26 2011 +0200
     2.3 @@ -226,18 +226,10 @@
     2.4          val thy = assoc_thy thy';
     2.5  	val metID = get_obj g_metID pt ppp;
     2.6          val sc = (#scr o get_met) metID;
     2.7 -        val (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (pp(*!/p/*),Frm); 
     2.8 -     (*val _=tracing("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
     2.9 -  	val _=tracing("### solve Check_postc, is(pt)= "^(istate2str is));
    2.10 -  	val _=tracing("### solve Check_postc, is'= "^
    2.11 -		      (istate2str (E,l,a,scval,scsaf,b)));*)
    2.12 +        val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm); 
    2.13          val ((p,p_),ps,f,pt) = 
    2.14  	    generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
    2.15 -		(ScrState (E,l,a,scval,scsaf,b), ctxt) (pp,Res) pt;
    2.16 -	(*val _=tracing("### solve Check_postc, is(pt')= "^
    2.17 -		      (istate2str (get_istate pt ([3],Res))));
    2.18 -	val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc 
    2.19 -				(ScrState (E,l,a,scval,scsaf,b));*)
    2.20 +		(ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
    2.21         in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
    2.22  	   ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
    2.23  	      ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt)))],ps,(pt,(p,p_))))
    2.24 @@ -370,8 +362,6 @@
    2.25      in if pp = [] then 
    2.26  	   let val is = ScrState (E,l,a,scval,scsaf,b)
    2.27  	       val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
    2.28 -           (*val _= tracing"### nxt_solv2 Apply_Method: stored is =";
    2.29 -               val _= tracing(istate2str is);*)
    2.30  	       val ((p,p_),ps,f,pt) = 
    2.31  		   generate1 thy tac_ (is, ctxt) (pp,Res) pt;
    2.32  	   in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
    2.33 @@ -386,33 +376,11 @@
    2.34          val (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (pp(*!/p/*),Frm)
    2.35          val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
    2.36  	val is = ScrState (E,l,a,scval,scsaf,b)
    2.37 -    (*val _= tracing"### nxt_solv3 Apply_Method: stored is =";
    2.38 -        val _= tracing(istate2str is);*)
    2.39          val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp, Res) pt;
    2.40  	(*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
    2.41         in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p,p_))) end
    2.42      end
    2.43 -(* tracing(istate2str(get_istate pt (p,p_)));
    2.44 -   *)
    2.45  
    2.46 -(*.start interpreter and do one rewrite.*)
    2.47 -(* val (_,Detail_Set'(thy',rls,t)) = (mI,m); val p = (p,p_);
    2.48 -   solve ("",Detail_Set'(thy', rls, t)) p pt;
    2.49 -  | nxt_solv (Detail_Set'(thy', rls, t)) _ (pt, p) = **********
    2.50 ----> Frontend/sml.sml
    2.51 -
    2.52 -  | nxt_solv (End_Detail' t) _ (pt, (p,p_)) = **********
    2.53 -    let val pr as (p',_) = (lev_up p, Res)
    2.54 -	val pp = par_pblobj pt p
    2.55 -	val r = (fst o (get_obj g_result pt)) p' 
    2.56 -	(*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
    2.57 -	val thy' = get_obj g_domID pt pp
    2.58 -	val (srls, is, sc) = from_pblobj' thy' pr pt
    2.59 -	val (tac_,is',_) = next_tac (thy',srls)  (pt,pr) sc is
    2.60 -    in (pr, ((pp,Frm(*???*)),is,tac_), 
    2.61 -	Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
    2.62 -	tac_2tac tac_, Sundef, pt) end
    2.63 -*)
    2.64    | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)
    2.65  
    2.66    | nxt_solv tac_ is (pt, pos as (p,p_)) =