101 ((flat o (map (collect_thy "IsacScripts"))) scri_thys) @ |
101 ((flat o (map (collect_thy "IsacScripts"))) scri_thys) @ |
102 ((flat o (map (collect_thy "IsacKnowledge"))) isac_thys) |
102 ((flat o (map (collect_thy "IsacKnowledge"))) isac_thys) |
103 : (theID * thydata) list |
103 : (theID * thydata) list |
104 end; |
104 end; |
105 |
105 |
106 fun show_thes () = (tracing o format_pblIDl o (scan [])) (!thehier); |
106 fun show_thes () = (writeln o format_pblIDl o (scan [])) (!thehier); |
107 |
107 |
108 |
108 |
109 |
109 |
110 (***.create the xml-format for the hierarchy.***) |
110 (***.create the xml-format for the hierarchy.***) |
111 |
111 |
130 |
130 |
131 (*.cut 'theID', the ID of theory elements from tail to head |
131 (*.cut 'theID', the ID of theory elements from tail to head |
132 until insertion into the hierarchy of theory elements 'th' is possible |
132 until insertion into the hierarchy of theory elements 'th' is possible |
133 (the hierarchy requires the parentnode to exist for insertion).*) |
133 (the hierarchy requires the parentnode to exist for insertion).*) |
134 fun cut_theID th ([]:theID) = |
134 fun cut_theID th ([]:theID) = |
135 raise error "could not insert into thy-hierarchy" |
135 error "could not insert into thy-hierarchy" |
136 | cut_theID th theID = |
136 | cut_theID th theID = |
137 if can_insert theID th |
137 if can_insert theID th |
138 then theID else cut_theID th (drop_last theID); |
138 then theID else cut_theID th (drop_last theID); |
139 |
139 |
140 (*.insert empty parents 'Html' into the hierarchy of theory elements 'th' |
140 (*.insert empty parents 'Html' into the hierarchy of theory elements 'th' |
162 (* val (th, (theID, thydata)::ths) = (!thehier, collect_thydata ()); |
162 (* val (th, (theID, thydata)::ths) = (!thehier, collect_thydata ()); |
163 *) |
163 *) |
164 | the_hier th ((theID, thydata)::ths) = |
164 | the_hier th ((theID, thydata)::ths) = |
165 if can_insert theID th |
165 if can_insert theID th |
166 then let val th' = if exist_the theID th |
166 then let val th' = if exist_the theID th |
167 then (tracing ("*** insert: preserved "^strs2str theID); |
167 then (writeln ("*** insert: preserved "^strs2str theID); |
168 th) |
168 th) |
169 else insrt theID thydata theID th |
169 else insrt theID thydata theID th |
170 in the_hier th' ths end |
170 in the_hier th' ths end |
171 else let val th' = fill_parents th theID theID (*..*** insert: not found*) |
171 else let val th' = fill_parents th theID theID (*..*** insert: not found*) |
172 val th' = insrt theID thydata theID th' |
172 val th' = insrt theID thydata theID th' |
259 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^ |
259 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^ |
260 authors2xml i "MATHAUTHORS" mathauthors ^ |
260 authors2xml i "MATHAUTHORS" mathauthors ^ |
261 authors2xml i "COURSEDESIGNS" coursedesign ^ |
261 authors2xml i "COURSEDESIGNS" coursedesign ^ |
262 "</RULESETDATA>\n" |
262 "</RULESETDATA>\n" |
263 | thydata2xml (theID, _) = |
263 | thydata2xml (theID, _) = |
264 raise error ("thydata2xml: not implemented for "^ strs2str' theID); |
264 error ("thydata2xml: not implemented for "^ strs2str' theID); |
265 |
265 |
266 (*.analoguous to 'fun met2file'.*) |
266 (*.analoguous to 'fun met2file'.*) |
267 fun thydata2file (xmldata:path) (pos:pos) (theID:theID) thydata = |
267 fun thydata2file (xmldata:path) (pos:pos) (theID:theID) thydata = |
268 (tracing ("### thes2file: id = " ^ strs2str theID); |
268 (writeln ("### thes2file: id = " ^ strs2str theID); |
269 str2file (xmldata ^ theID2filename theID) |
269 str2file (xmldata ^ theID2filename theID) |
270 (thydata2xml (theID:theID, thydata))); |
270 (thydata2xml (theID:theID, thydata))); |
271 |
271 |
272 (*.analoguous to 'fun node'; here we scan ??????????.*) |
272 (*.analoguous to 'fun node'; here we scan ??????????.*) |
273 (* val (pa, ids, po, wfn, (Ptyp (id,[n],ns))) = |
273 (* val (pa, ids, po, wfn, (Ptyp (id,[n],ns))) = |