446 | SOME (f, (_, id)) => |
446 | SOME (f, (_, id)) => |
447 let fun eq2 d (i, _, _, _, itm_) = d = (Model.d_in itm_) andalso i <> 0 |
447 let fun eq2 d (i, _, _, _, itm_) = d = (Model.d_in itm_) andalso i <> 0 |
448 in case find_first (eq2 d) ppc of |
448 in case find_first (eq2 d) ppc of |
449 NONE => Add (i, [], true, f,Model.Cor ((d, ts), (id, Model.pbl_ids' d ts))) |
449 NONE => Add (i, [], true, f,Model.Cor ((d, ts), (id, Model.pbl_ids' d ts))) |
450 | SOME (i', _, _, _, itm_) => |
450 | SOME (i', _, _, _, itm_) => |
451 if is_list_dsc d |
451 if LTool.is_list_dsc d |
452 then |
452 then |
453 let |
453 let |
454 val in_itm = Model.ts_in itm_ |
454 val in_itm = Model.ts_in itm_ |
455 val ts' = union op = ts in_itm |
455 val ts' = union op = ts in_itm |
456 val i'' = if in_itm = [] then i else i' |
456 val i'' = if in_itm = [] then i else i' |
1088 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *) |
1088 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *) |
1089 let |
1089 let |
1090 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI |
1090 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI |
1091 val dI = if dI = "" then theory2theory' thy else dI |
1091 val dI = if dI = "" then theory2theory' thy else dI |
1092 val mI = if mI = [] then hd met else mI |
1092 val mI = if mI = [] then hd met else mI |
1093 val hdl = case cas of NONE => pblterm dI pI | SOME t => t |
1093 val hdl = case cas of NONE => LTool.pblterm dI pI | SOME t => t |
1094 val (pt,_) = cappend_problem e_ctree [] (Selem.Uistate, Selem.e_ctxt) ([], (dI, pI, mI)) |
1094 val (pt,_) = cappend_problem e_ctree [] (Selem.Uistate, Selem.e_ctxt) ([], (dI, pI, mI)) |
1095 ([], (dI,pI,mI), hdl) |
1095 ([], (dI,pI,mI), hdl) |
1096 val pt = update_spec pt [] (dI, pI, mI) |
1096 val pt = update_spec pt [] (dI, pI, mI) |
1097 val pits = Generate.init_pbl' ppc |
1097 val pits = Generate.init_pbl' ppc |
1098 val pt = update_pbl pt [] pits |
1098 val pt = update_pbl pt [] pits |
1128 end |
1128 end |
1129 else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI) |
1129 else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI) |
1130 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*) |
1130 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*) |
1131 val dI = theory2theory' (maxthy thy thy') |
1131 val dI = theory2theory' (maxthy thy thy') |
1132 val hdl = case cas of |
1132 val hdl = case cas of |
1133 NONE => pblterm dI pI |
1133 NONE => LTool.pblterm dI pI |
1134 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t |
1134 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t |
1135 val (pt, _) = |
1135 val (pt, _) = |
1136 cappend_problem e_ctree [] (Selem.e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) |
1136 cappend_problem e_ctree [] (Selem.e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) |
1137 val pt = update_ctxt pt [] pctxt |
1137 val pt = update_ctxt pt [] pctxt |
1138 in |
1138 in |
1289 | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) = |
1289 | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) = |
1290 let |
1290 let |
1291 val (dI, pI, _) = get_somespec' spec spec' |
1291 val (dI, pI, _) = get_somespec' spec spec' |
1292 val {cas, ...} = Specify.get_pbt pI |
1292 val {cas, ...} = Specify.get_pbt pI |
1293 in case cas of |
1293 in case cas of |
1294 NONE => Form (pblterm dI pI) |
1294 NONE => Form (LTool.pblterm dI pI) |
1295 | SOME t => Form (subst_atomic (Model.mk_env probl) t) |
1295 | SOME t => Form (subst_atomic (Model.mk_env probl) t) |
1296 end |
1296 end |
1297 |
1297 |
1298 (* pt_extract returns |
1298 (* pt_extract returns |
1299 # the formula at pos |
1299 # the formula at pos |