1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Sat Oct 09 16:20:02 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Sun Oct 10 14:15:43 2010 +0200
     1.3 @@ -1568,12 +1568,10 @@
     1.4  
     1.5  
     1.6  
     1.7 -(*.create a calc-tree with oris via an cas.refined pbl.*)
     1.8 -fun nxt_specify_init_calc (([],(dI,pI,mI)): fmz) =
     1.9 -(* val ([],(dI,pI,mI)) = (fmz, sp);
    1.10 -   *)
    1.11 -    if pI <> [] then (*comes from pbl-browser*)
    1.12 -	let val {cas,met,ppc,thy,...} = get_pbt pI
    1.13 +(* create a calc-tree with oris via an cas.refined pbl *)
    1.14 +fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
    1.15 +    if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
    1.16 +	let val {cas, met, ppc, thy, ...} = get_pbt pI
    1.17  	    val dI = if dI = "" then theory2theory' thy else dI
    1.18  	    val thy = assoc_thy dI
    1.19  	    val mI = if mI = [] then hd met else mI
    1.20 @@ -1583,8 +1581,8 @@
    1.21  	    val pt = update_spec pt [] (dI,pI,mI)
    1.22  	    val pits = init_pbl' ppc
    1.23  	    val pt = update_pbl pt [] pits
    1.24 -	in ((pt,([],Pbl)), []): calcstate end
    1.25 -    else if mI <> [] then (*comes from met-browser*)
    1.26 +	in ((pt, ([] ,Pbl)), []) : calcstate end
    1.27 +    else if mI <> [] then (* from met-browser *)
    1.28  	let val {ppc,...} = get_met mI
    1.29  	    val dI = if dI = "" then "Isac" else dI
    1.30  	    val thy = assoc_thy dI
    1.31 @@ -1593,13 +1591,11 @@
    1.32  	    val pt = update_spec pt [] (dI,pI,mI)
    1.33  	    val mits = init_pbl' ppc
    1.34  	    val pt = update_met pt [] mits
    1.35 -	in ((pt,([],Met)), []) end
    1.36 -    else (*completely new example*)
    1.37 +	in ((pt, ([], Met)), []) : calcstate end
    1.38 +    else (* new example, pepare for interactive modeling *)
    1.39  	let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec)
    1.40  					 ([], e_spec, e_term)
    1.41 -	in ((pt,([],Pbl)), []) end
    1.42 -(* val (fmz, (dI,pI,mI)) = (fmz, sp);
    1.43 -   *)
    1.44 +	in ((pt,([],Pbl)), []) : calcstate end
    1.45    | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = 
    1.46      let           (* both """"""""""""""""""""""""" either empty or complete *)
    1.47  	val thy = assoc_thy dI
    1.48 @@ -1617,8 +1613,10 @@
    1.49  		    | SOME t => subst_atomic ((vars_of_pbl_' ppc) 
    1.50  						  ~~~ vals_of_oris pors) t
    1.51          val (pt, _) = cappend_problem e_ptree [] e_istate (fmz, (dI, pI, mI))
    1.52 -				 (pors, (dI, pI, mI), hdl)
    1.53 -  in ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) end;
    1.54 +				      (pors, (dI, pI, mI), hdl)
    1.55 +    in ((pt, ([], Pbl)), 
    1.56 +        fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
    1.57 +    end;
    1.58  
    1.59  
    1.60