1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Wed May 04 14:07:51 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Thu May 05 09:23:32 2011 +0200
     1.3 @@ -1129,27 +1129,26 @@
     1.4  	  Model_Problem,
     1.5  	  Safe,pt)
     1.6    end
     1.7 -  (*ONLY for STARTING modeling phase*)
     1.8 +
     1.9 +    (*ONLY for STARTING modeling phase*)
    1.10    | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
    1.11 -  let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
    1.12 -         *)
    1.13 -    val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) = 
    1.14 -	get_obj I pt p
    1.15 -    val thy' = if dI = e_domID then dI' else dI
    1.16 -    val thy = assoc_thy thy'
    1.17 -    val {ppc,prls,where_,...} = get_pbt pI'
    1.18 -    val pre = check_preconds thy prls where_ pbl
    1.19 -    val pb = foldl and_ (true, map fst pre)
    1.20 -    val ((p,_),_,_,pt) = 
    1.21 -	generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
    1.22 -    val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met) 
    1.23 -		(ppc,(#ppc o get_met) mI') (dI',pI',mI');
    1.24 -  in ((p,Pbl), ((p,p_),Uistate),
    1.25 -      Form' (PpcKF (0,EdUndef,(length p),Nundef,
    1.26 -		    (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
    1.27 -      nxt, Safe, pt) end
    1.28 +      let 
    1.29 +        val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) = get_obj I pt p
    1.30 +        val thy' = if dI = e_domID then dI' else dI
    1.31 +        val thy = assoc_thy thy'
    1.32 +        val {ppc,prls,where_,...} = get_pbt pI'
    1.33 +        val pre = check_preconds thy prls where_ pbl
    1.34 +        val pb = foldl and_ (true, map fst pre)
    1.35 +        val ((p,_),_,_,pt) = generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
    1.36 +        val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met) 
    1.37 +		      (ppc,(#ppc o get_met) mI') (dI',pI',mI');
    1.38 +      in ((p, Pbl), ((p, p_), Uistate), 
    1.39 +          Form' (PpcKF (0, EdUndef, length p, Nundef,
    1.40 +		       (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
    1.41 +          nxt, Safe, pt)
    1.42 +      end
    1.43  
    1.44 -(*. called only if no_met is specified .*)     
    1.45 +    (*. called only if no_met is specified .*)     
    1.46    | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
    1.47    let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
    1.48           *)
    1.49 @@ -1429,20 +1428,19 @@
    1.50      val pbl = init_pbl ppc (* fill in descriptions *)
    1.51      (*----------------if you think, this should be done by the Dialog 
    1.52       in the java front-end, search there for WN060225-modelProblem----*)
    1.53 -    val (pbl, met) = case cas of NONE => (pbl, [])
    1.54 -			    | _ => complete_mod_ (oris, mpc, ppc, probl)
    1.55 +    val (pbl, met) = 
    1.56 +      case cas of NONE => (pbl, [])
    1.57 +			| _ => complete_mod_ (oris, mpc, ppc, probl)
    1.58      (*----------------------------------------------------------------*)
    1.59      val tac_ = Model_Problem' (pI, pbl, met)
    1.60      val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
    1.61    in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
    1.62  
    1.63 -(* val Add_Find ct = tac;
    1.64 -   *)
    1.65    | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
    1.66    | nxt_specif (Add_Find  ct) ptp = nxt_specif_additem "#Find"  ct ptp
    1.67    | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
    1.68  
    1.69 -(*. called only if no_met is specified .*)     
    1.70 +    (*. called only if no_met is specified .*)     
    1.71    | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
    1.72      let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
    1.73  	val opt = refine_ori oris pI