93 let |
93 let |
94 val i = indentation |
94 val i = indentation |
95 val j = indentation |
95 val j = indentation |
96 fun node i p theID (Ptyp (id, _, ns)) = |
96 fun node i p theID (Ptyp (id, _, ns)) = |
97 let |
97 let |
98 val p' = lev_on p |
98 val p' = Ctree.lev_on p |
99 val theID' = theID @ [id] |
99 val theID' = theID @ [id] |
100 in |
100 in |
101 (indt i) ^ "<NODE>\n" ^ |
101 (indt i) ^ "<NODE>\n" ^ |
102 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ |
102 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ |
103 (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^ |
103 (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^ |
104 (indt (i+j)) ^ "<CONTENTREF> " ^ theID2guh theID' ^ " </CONTENTREF>\n" ^ |
104 (indt (i+j)) ^ "<CONTENTREF> " ^ theID2guh theID' ^ " </CONTENTREF>\n" ^ |
105 (nodes (i+j) (lev_dn p') theID' ns) ^ |
105 (nodes (i+j) (Ctree.lev_dn p') theID' ns) ^ |
106 (indt i) ^ "</NODE>\n" |
106 (indt i) ^ "</NODE>\n" |
107 end |
107 end |
108 and nodes _ _ _ [] = "" |
108 and nodes _ _ _ [] = "" |
109 | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (lev_on p) theID ns); |
109 | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Ctree.lev_on p) theID ns); |
110 in nodes j [0] [] h end; |
110 in nodes j [0] [] h end; |
111 |
111 |
112 fun thy_hierarchy2file (path:path) = |
112 fun thy_hierarchy2file (path:path) = |
113 str2file (path ^ "thy_hierarchy.xml") |
113 str2file (path ^ "thy_hierarchy.xml") |
114 ("<NODE>\n" ^ |
114 ("<NODE>\n" ^ |
163 "</RULESETDATA>\n" |
163 "</RULESETDATA>\n" |
164 | thydata2xml (theID, _) = |
164 | thydata2xml (theID, _) = |
165 error ("thydata2xml: not implemented for "^ strs2str' theID); |
165 error ("thydata2xml: not implemented for "^ strs2str' theID); |
166 |
166 |
167 (* analoguous to 'fun met2file' *) |
167 (* analoguous to 'fun met2file' *) |
168 fun thydata2file (path : path) (pos : pos) (theID : theID) thydata = |
168 fun thydata2file (path : path) (pos : Ctree.pos) (theID : theID) thydata = |
169 (writeln ("### thes2file: id = " ^ strs2str theID); |
169 (writeln ("### thes2file: id = " ^ strs2str theID); |
170 str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata))); |
170 str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata))); |
171 |
171 |
172 (* analoguous to 'fun node' *) |
172 (* analoguous to 'fun node' *) |
173 fun thenode (pa : path) ids po wfn (Ptyp (id, [n], ns)) = |
173 fun thenode (pa : path) ids po wfn (Ptyp (id, [n], ns)) = |
174 let val po' = lev_on po |
174 let val po' = Ctree.lev_on po |
175 in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns end |
175 in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Ctree.lev_dn po') wfn ns end |
176 and thenodes _ _ _ _ [] = () |
176 and thenodes _ _ _ _ [] = () |
177 | thenodes pa ids po wfn (n::ns) = |
177 | thenodes pa ids po wfn (n::ns) = |
178 (thenode pa ids po wfn n; thenodes pa ids (lev_on po) wfn ns); |
178 (thenode pa ids po wfn n; thenodes pa ids (Ctree.lev_on po) wfn ns); |
179 |
179 |
180 (* analoguous to 'fun mets2file' *) |
180 (* analoguous to 'fun mets2file' *) |
181 fun thes2file (p : path) = thenodes p [] [0] thydata2file (get_thes ()); |
181 fun thes2file (p : path) = thenodes p [] [0] thydata2file (get_thes ()); |
182 |
182 |
183 |
183 |