129 wfn (*= pbl2file*) |
129 wfn (*= pbl2file*) |
130 "~~~~~ fun pbl2file, args:"; val ((path:filepath), (pos:pos), (id: Method.id), (pbl as {guh,...})) = |
130 "~~~~~ fun pbl2file, args:"; val ((path:filepath), (pos:pos), (id: Method.id), (pbl as {guh,...})) = |
131 (pa, po', (ids@[id]), n); |
131 (pa, po', (ids@[id]), n); |
132 strs2str id = "[\"e_pblID\"]"; (*true*) |
132 strs2str id = "[\"e_pblID\"]"; (*true*) |
133 pos2str pos = "[1]"; (*true*) |
133 pos2str pos = "[1]"; (*true*) |
134 path ^ guh2filename guh = "/tmp/pbl/pbl_empty.xml"; (*true*) |
134 path ^ Thy_Present.guh2filename guh = "/tmp/pbl/pbl_empty.xml"; (*true*) |
135 "~~~~~ fun pbl2xml, args:"; val (id: Problem.id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) = |
135 "~~~~~ fun pbl2xml, args:"; val (id: Problem.id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) = |
136 (id, pbl); |
136 (id, pbl); |
137 "~~~~~ fun pbl2term, args:"; val (thy, (pblRD:pblRD)) = (thy, id); |
137 "~~~~~ fun pbl2term, args:"; val (thy, (pblRD:pblRD)) = (thy, id); |
138 if ("Problem (" ^ Context.theory_name thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")") = |
138 if ("Problem (" ^ Context.theory_name thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")") = |
139 "Problem (Pure', [empty_probl_id])" |
139 "Problem (Pure', [empty_probl_id])" |