1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri Apr 08 15:16:08 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Mon Apr 11 12:56:57 2011 +0200
     1.3 @@ -802,9 +802,9 @@
     1.4              end
     1.5        end
     1.6    | appl_add ctxt sel oris ppc pbt str =
     1.7 -      case parse (ProofContext.theory_of ctxt) str of
     1.8 +      case parseNEW ctxt str of
     1.9            NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
    1.10 -        | SOME t => case is_known ctxt sel oris (term_of t) of
    1.11 +        | SOME t => case is_known ctxt sel oris t of
    1.12              ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
    1.13                ("", itm) => Add itm
    1.14                | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
    1.15 @@ -1015,7 +1015,8 @@
    1.16        val cpI = if pI = e_pblID then pI' else pI;
    1.17        val cmI = if mI = e_metID then mI' else mI;
    1.18        val {ppc,pre,prls,...} = get_met cmI;
    1.19 -    in case appl_add (thy2ctxt thy) sel oris met ppc ct of
    1.20 +      val ctxt = get_ctxt pt (p,Met);
    1.21 +    in case appl_add ctxt sel oris met ppc ct of
    1.22        Add itm (*..union old input *) =>
    1.23  	let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
    1.24                 *)
    1.25 @@ -1048,7 +1049,7 @@
    1.26      end
    1.27  (* val (p,_) = p;
    1.28     *)
    1.29 -| specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt = 
    1.30 +| specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt = 
    1.31      let
    1.32        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    1.33  		  probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.34 @@ -1056,7 +1057,8 @@
    1.35        val cpI = if pI = e_pblID then pI' else pI;
    1.36        val cmI = if mI = e_metID then mI' else mI;
    1.37        val {ppc,where_,prls,...} = get_pbt cpI;
    1.38 -    in case appl_add (thy2ctxt thy) sel oris pbl ppc ct of
    1.39 +      val ctxt = get_ctxt pt pos;
    1.40 +    in case appl_add ctxt sel oris pbl ppc ct of
    1.41        Add itm (*..union old input *) =>
    1.42        (* val Add itm = appl_add thy sel oris pbl ppc ct;
    1.43           *)
    1.44 @@ -1109,9 +1111,9 @@
    1.45  fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)= 
    1.46    let          (* either """"""""""""""" all empty or complete *)
    1.47      val thy = assoc_thy dI';
    1.48 -    val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
    1.49 -	       else pI' |> #ppc o get_pbt |> prep_ori fmz thy |> #1;
    1.50 -    val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
    1.51 +    val (oris, ctxt) = if dI' = e_domID orelse pI' = e_pblID then ([], e_ctxt)
    1.52 +	       else pI' |> #ppc o get_pbt |> prep_ori fmz thy;
    1.53 +    val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
    1.54  				 (oris,(dI',pI',mI'),e_term);
    1.55      val {ppc,prls,where_,...} = get_pbt pI'
    1.56      (*val pbl = init_pbl ppc;  WN.9.03: done in Model/Refine_Problem
    1.57 @@ -1288,7 +1290,8 @@
    1.58  		  probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
    1.59        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.60        val cpI = if pI = e_pblID then pI' else pI;
    1.61 -    in case appl_add (thy2ctxt thy) sel oris pbl ((#ppc o get_pbt) cpI) ct of
    1.62 +      val ctxt = get_ctxt pt (p, Pbl);
    1.63 +    in case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
    1.64  	   Add itm (*..union old input *) =>
    1.65  (* val Add itm = appl_add thy sel oris pbl ppc ct;
    1.66     *)
    1.67 @@ -1321,7 +1324,8 @@
    1.68  		  probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.69        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.70        val cmI = if mI = e_metID then mI' else mI;
    1.71 -    in case appl_add (thy2ctxt thy) sel oris met ((#ppc o get_met) cmI) ct of
    1.72 +      val ctxt = get_ctxt pt (p,Met);
    1.73 +    in case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
    1.74        Add itm (*..union old input *) =>
    1.75  	let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
    1.76                 *)
    1.77 @@ -1573,20 +1577,20 @@
    1.78    | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = 
    1.79      let           (* both """"""""""""""""""""""""" either empty or complete *)
    1.80  	val thy = assoc_thy dI
    1.81 -	val (pI, pors, mI) = 
    1.82 +	val (pI, (pors, pctxt), mI) = 
    1.83  	    if mI = ["no_met"] 
    1.84 -	    then let val pors = get_pbt pI |> #ppc |> prep_ori fmz thy |> #1;
    1.85 +	    then let val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
    1.86  		     val pI' = refine_ori' pors pI;
    1.87 -		 in (pI', pors(*refinement over models with diff.precond only*),
    1.88 +		 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
    1.89  		     (hd o #met o get_pbt) pI') end
    1.90 -	    else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
    1.91 +	    else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
    1.92  	val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
    1.93  	val dI = theory2theory' (maxthy thy thy');
    1.94  	val hdl = case cas of
    1.95  		      NONE => pblterm dI pI
    1.96  		    | SOME t => subst_atomic ((vars_of_pbl_' ppc) 
    1.97  						  ~~~ vals_of_oris pors) t;
    1.98 -        val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
    1.99 +        val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
   1.100  				      (pors, (dI, pI, mI), hdl)
   1.101      in ((pt, ([], Pbl)), 
   1.102          fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate