113 val it = "Problem (Isac, [normalise, univariate, equations])" : string |
113 val it = "Problem (Isac, [normalise, univariate, equations])" : string |
114 *) |
114 *) |
115 val i = indentation; |
115 val i = indentation; |
116 |
116 |
117 (* new version with <KESTOREREF>s -- not used *) |
117 (* new version with <KESTOREREF>s -- not used *) |
118 fun pbl2xml (id:(*pblRD*)Spec.pblID) ({guh,mathauthors,init,cas,met,ppc,prls, |
118 fun pbl2xml (id:(*pblRD*)Problem.id) ({guh,mathauthors,init,cas,met,ppc,prls, |
119 thy,where_}:Problem.T) = |
119 thy,where_}:Problem.T) = |
120 let val thy' = Context.theory_name thy |
120 let val thy' = Context.theory_name thy |
121 val prls' = (#id o Rule_Set.rep) prls |
121 val prls' = (#id o Rule_Set.rep) prls |
122 in "<NODECONTENT>\n" ^ |
122 in "<NODECONTENT>\n" ^ |
123 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
123 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
147 authors2xml i "MATHAUTHORS" mathauthors ^ |
147 authors2xml i "MATHAUTHORS" mathauthors ^ |
148 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
148 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
149 "</NODECONTENT>" : Celem.xml |
149 "</NODECONTENT>" : Celem.xml |
150 end; |
150 end; |
151 (* old version with 'dead' strings for rls, calc, ....* *) |
151 (* old version with 'dead' strings for rls, calc, ....* *) |
152 fun pbl2xml (id:(*pblRD*)Spec.pblID) ({guh,mathauthors,init,cas,met,ppc,prls, |
152 fun pbl2xml (id:(*pblRD*)Problem.id) ({guh,mathauthors,init,cas,met,ppc,prls, |
153 thy,where_}:Problem.T) = |
153 thy,where_}:Problem.T) = |
154 "<NODECONTENT>\n" ^ |
154 "<NODECONTENT>\n" ^ |
155 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
155 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
156 (((id2xml i)(* o rev*)) id) ^ |
156 (((id2xml i)(* o rev*)) id) ^ |
157 indt i ^ "<META> </META>\n" ^ |
157 indt i ^ "<META> </META>\n" ^ |
179 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
179 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
180 "</NODECONTENT>" : Celem.xml; |
180 "</NODECONTENT>" : Celem.xml; |
181 |
181 |
182 |
182 |
183 (**. write pbls from hierarchy to files.**) |
183 (**. write pbls from hierarchy to files.**) |
184 fun pbl2file (path: Celem.filepath) (pos: Pos.pos) (id:Spec.metID) (pbl as {guh,...}) = |
184 fun pbl2file (path: Celem.filepath) (pos: Pos.pos) (id:Method.id) (pbl as {guh,...}) = |
185 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Pos.pos2str pos); |
185 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Pos.pos2str pos); |
186 ((str2file (path ^ Rtools.guh2filename guh)) o (pbl2xml id)) pbl |
186 ((str2file (path ^ Rtools.guh2filename guh)) o (pbl2xml id)) pbl |
187 ); |
187 ); |
188 |
188 |
189 (**. write mets from hierarchy to files.**) |
189 (**. write mets from hierarchy to files.**) |
190 (*.format a method in xml for presentation on the method browser; |
190 (*.format a method in xml for presentation on the method browser; |
191 new version with <KESTOREREF>s -- not used because linking |
191 new version with <KESTOREREF>s -- not used because linking |
192 requires elements (rls, calc, ...) to be reorganized.*) |
192 requires elements (rls, calc, ...) to be reorganized.*) |
193 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*) |
193 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*) |
194 fun met2xml (id: Spec.metID) ({guh,mathauthors,init,ppc,pre,scr,calc, |
194 fun met2xml (id: Method.id) ({guh,mathauthors,init,ppc,pre,scr,calc, |
195 crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) = |
195 crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) = |
196 let val thy' = "Isac_Knowledge" (*FIXME.WN0607 get thy from met ?!?*) |
196 let val thy' = "Isac_Knowledge" (*FIXME.WN0607 get thy from met ?!?*) |
197 val crls' = (#id o Rule_Set.rep) crls |
197 val crls' = (#id o Rule_Set.rep) crls |
198 val erls' = (#id o Rule_Set.rep) erls |
198 val erls' = (#id o Rule_Set.rep) erls |
199 val nrls' = (#id o Rule_Set.rep) nrls |
199 val nrls' = (#id o Rule_Set.rep) nrls |
227 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
227 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^ |
228 "</NODECONTENT>" : Celem.xml |
228 "</NODECONTENT>" : Celem.xml |
229 end; |
229 end; |
230 (*.format a method in xml for presentation on the method browser; |
230 (*.format a method in xml for presentation on the method browser; |
231 old version with 'dead' strings for rls, calc, ....*) |
231 old version with 'dead' strings for rls, calc, ....*) |
232 fun met2xml (id: Spec.metID) ({guh,mathauthors,init,ppc,pre,scr,calc, |
232 fun met2xml (id: Method.id) ({guh,mathauthors,init,ppc,pre,scr,calc, |
233 crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) = |
233 crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) = |
234 "<NODECONTENT>\n" ^ |
234 "<NODECONTENT>\n" ^ |
235 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
235 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^ |
236 id2xml i id ^ |
236 id2xml i id ^ |
237 indt i ^ "<META> </META>\n" ^ |
237 indt i ^ "<META> </META>\n" ^ |
252 (* writeln (met2xml ["Test", "solve_linear"] |
252 (* writeln (met2xml ["Test", "solve_linear"] |
253 (get_met ["Test", "solve_linear"])); |
253 (get_met ["Test", "solve_linear"])); |
254 *) |
254 *) |
255 |
255 |
256 (*.write the files using an int-key (pos') as filename.*) |
256 (*.write the files using an int-key (pos') as filename.*) |
257 fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Spec.metID) met = |
257 fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Method.id) met = |
258 (writeln ("### met2file: id = " ^ strs2str id); |
258 (writeln ("### met2file: id = " ^ strs2str id); |
259 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met); |
259 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met); |
260 |
260 |
261 (*.write the files using the guh as filename.*) |
261 (*.write the files using the guh as filename.*) |
262 fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Spec.metID) (met as {guh,...}) = |
262 fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Method.id) (met as {guh,...}) = |
263 (writeln ("### met2file: id = " ^ strs2str id); |
263 (writeln ("### met2file: id = " ^ strs2str id); |
264 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met); |
264 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met); |
265 |
265 |
266 (*.scan the mtree Ptyp and print the nodes using wfn.*) |
266 (*.scan the mtree Ptyp and print the nodes using wfn.*) |
267 fun node (pa: Celem.filepath) ids po wfn (Store.Node (id,[n],ns)) = |
267 fun node (pa: Celem.filepath) ids po wfn (Store.Node (id,[n],ns)) = |