equal
deleted
inserted
replaced
105 |
105 |
106 (*.format a problem in xml for presentation on the problem browser; |
106 (*.format a problem in xml for presentation on the problem browser; |
107 new version with <KESTOREREF>s -- not used because linking |
107 new version with <KESTOREREF>s -- not used because linking |
108 requires elements (rls, calc, ...) to be reorganized.*) |
108 requires elements (rls, calc, ...) to be reorganized.*) |
109 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*) |
109 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*) |
110 fun pbl2term thy (pblRD:pblRD) = (*WN120405.TODO.txt*) |
110 fun pbl2term thy (pblRD: Specify.pblRD) = (*WN120405.TODO.txt*) |
111 str2term ("Problem (" ^ (get_thy o theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")"); |
111 str2term ("Problem (" ^ (get_thy o theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")"); |
112 (* term2str (pbl2term (Thy_Info.get_theory "Isac") ["equations","univariate","normalize"]); |
112 (* term2str (pbl2term (Thy_Info.get_theory "Isac") ["equations","univariate","normalize"]); |
113 val it = "Problem (Isac, [normalize, univariate, equations])" : string |
113 val it = "Problem (Isac, [normalize, univariate, equations])" : string |
114 *) |
114 *) |
115 val i = indentation; |
115 val i = indentation; |
297 srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc, |
297 srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc, |
298 ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: met |
298 ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: met |
299 |
299 |
300 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *) |
300 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *) |
301 fun update_metpair thy metID errpats = let |
301 fun update_metpair thy metID errpats = let |
302 val ret = (update_metdata (get_met' thy metID) errpats, metID) |
302 val ret = (update_metdata (Specify.get_met' thy metID) errpats, metID) |
303 handle ERROR _ => error ("update_metpair: " ^ (strs2str metID) ^ " must address a method"); |
303 handle ERROR _ => error ("update_metpair: " ^ (strs2str metID) ^ " must address a method"); |
304 in ret end; |
304 in ret end; |