1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri May 25 09:58:20 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri May 25 16:30:15 2012 +0200
     1.3 @@ -1841,46 +1841,42 @@
     1.4  	(by application of another tac to the preceding formula !)
     1.5     pos is assumed to come from the frontend, ie. generated by moveDown.*)
     1.6  (*cannot be in ctree.sml, because ModSpec has to be calculated*)
     1.7 -fun pt_extract (pt,([],Res)) =
     1.8 -(* val (pt,([],Res)) = ptp;
     1.9 -   *)
    1.10 +fun pt_extract (pt,([],Res)) = (* WN120512: --returns--> Check_Postcondition WRONGLY
    1.11 +                                  see --- build fun is_exactly_equal*)
    1.12      (* ML_TODO 110417 get assumptions from ctxt !? *)
    1.13 -    let val (f, asm) = get_obj g_result pt []
    1.14 -    in (Form f, NONE, asm) end
    1.15 -(* val p = [3,2];
    1.16 -   *)
    1.17 +      let val (f, asm) = get_obj g_result pt []
    1.18 +      in (Form f, NONE, asm) end
    1.19    | pt_extract (pt,(p,Res)) =
    1.20 -(* val (pt,(p,Res)) = ptp;
    1.21 -   *)
    1.22 -    let val (f, asm) = get_obj g_result pt p
    1.23 -	val tac = if last_onlev pt p
    1.24 -		  then if is_pblobj' pt (lev_up p)
    1.25 -		       then let val (PblObj{spec=(_,pI,_),...}) = 
    1.26 -				    get_obj I pt (lev_up p)
    1.27 -			    in if pI = e_pblID then NONE 
    1.28 -			       else SOME (Check_Postcond pI) end
    1.29 -		       else SOME End_Trans (*WN0502 TODO for other branches*)
    1.30 -		  else let val p' = lev_on p
    1.31 -		       in if is_pblobj' pt p'
    1.32 -			  then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
    1.33 -				       get_obj I pt p'
    1.34 -			       in SOME (Subproblem (dI, pI)) end
    1.35 -			  else if f = get_obj g_form pt p'
    1.36 -			  then SOME (get_obj g_tac pt p')
    1.37 -			  (*because this Frm          ~~~is not on worksheet*)
    1.38 -			  else SOME (Take (term2str (get_obj g_form pt p')))
    1.39 -		       end
    1.40 -    in (Form f, tac, asm) end
    1.41 -	
    1.42 +      let
    1.43 +        val (f, asm) = get_obj g_result pt p
    1.44 +        val tac =
    1.45 +          if last_onlev pt p
    1.46 +          then
    1.47 +            if is_pblobj' pt (lev_up p)
    1.48 +            then
    1.49 +              let
    1.50 +                val (PblObj{spec=(_,pI,_),...}) = get_obj I pt (lev_up p)
    1.51 +              in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
    1.52 +		        else SOME End_Trans (*WN0502 TODO for other branches*)
    1.53 +		      else
    1.54 +		        let val p' = lev_on p
    1.55 +		        in
    1.56 +		          if is_pblobj' pt p'
    1.57 +		          then
    1.58 +		            let val (PblObj{origin = (_,(dI,pI,_),_),...}) = get_obj I pt p'
    1.59 +		            in SOME (Subproblem (dI, pI)) end
    1.60 +		          else
    1.61 +		            if f = get_obj g_form pt p'
    1.62 +		            then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
    1.63 +		            else SOME (Take (term2str (get_obj g_form pt p')))
    1.64 +		        end
    1.65 +      in (Form f, tac, asm) end
    1.66    | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
    1.67 -(* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
    1.68 -   val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
    1.69 -   *)
    1.70 -    let val ppobj = get_obj I pt p
    1.71 -	val f = if is_pblobj ppobj then pt_model ppobj p_
    1.72 -		else get_obj pt_form pt p
    1.73 -	val tac = g_tac ppobj
    1.74 -    in (f, SOME tac, []) end;
    1.75 +      let
    1.76 +        val ppobj = get_obj I pt p
    1.77 +        val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
    1.78 +        val tac = g_tac ppobj
    1.79 +      in (f, SOME tac, []) end;
    1.80  
    1.81  
    1.82  (**. get the formula from a ctree-node: