1.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Oct 06 17:03:44 2016 +0200
1.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Oct 10 18:24:14 2016 +0200
1.3 @@ -118,145 +118,6 @@
1.4 (hierarchy_guh (get_thes ())) ^
1.5 "</NODE>");
1.6
1.7 -(*url to a source external to isac*)
1.8 -fun extref2xml j linktext url =
1.9 - indt j ^ "<EXTREF>\n" ^
1.10 - indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
1.11 - indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
1.12 - indt j ^ "</EXTREF>\n" : xml;
1.13 -
1.14 -(*.for creating a href for a rule within an rls's rule list;
1.15 - the guh points to the thy of definition of the rule, NOT of use in rls.*)
1.16 -fun rule2xml j (thyID:thyID) Erule =
1.17 - error "rule2xml called with 'Erule'"
1.18 - | rule2xml j thyID (Thm (thmDeriv, thm)) =
1.19 - indt j ^ "<RULE>\n" ^
1.20 - indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
1.21 - indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
1.22 - indt (j+i) ^ "<GUH> " ^
1.23 - thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
1.24 - indt j ^ "</RULE>\n" : xml
1.25 - | rule2xml j thyID (Calc (termop, _)) = ""
1.26 -(*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
1.27 - see smltest/../datatypes.sml !
1.28 - indt j ^ "<RULE>\n" ^
1.29 - indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
1.30 - indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
1.31 - termop ^ " </GUH>\n" ^
1.32 - indt j ^ "</RULE>\n"
1.33 -*)
1.34 - | rule2xml j thyID (Cal1 (termop, _)) = ""
1.35 - | rule2xml j thyID (Rls_ rls) =
1.36 - let val rls' = (#id o rep_rls) rls
1.37 - in
1.38 - indt j ^ "<RULE>\n" ^
1.39 - indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
1.40 - indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
1.41 - indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
1.42 - indt j ^ "</RULE>\n"
1.43 - end;
1.44 -
1.45 -fun calcref2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
1.46 - indt j ^ "<CALCREF>\n" ^
1.47 - indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
1.48 - indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge",
1.49 - thyID) scrop ^ " </GUH>\n" ^
1.50 - indt j ^ "</CALCREF>\n" : xml;
1.51 -fun calcrefs2xml _ (_,[]) = "":xml
1.52 - | calcrefs2xml j (thyID, cal::cs) =
1.53 - calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
1.54 -
1.55 -fun rules2xml j thyID [] = ("":xml)
1.56 - | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
1.57 -fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
1.58 - srls, calc, rules, errpatts, scr}) =
1.59 - indt j ^"<RULESET>\n"^
1.60 - indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
1.61 - indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
1.62 - indt (j+i) ^"<RULES>\n" ^
1.63 - rules2xml (j+2*i) thyID rules ^
1.64 - indt (j+i) ^"</RULES>\n" ^
1.65 - indt (j+i) ^"<PRECONDS> " ^
1.66 - terms2xml' (j+2*i) preconds ^
1.67 - indt (j+i) ^"</PRECONDS>\n" ^
1.68 - indt (j+i) ^"<ORDER>\n" ^
1.69 - indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
1.70 -(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
1.71 - indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
1.72 - thyID) ord ^ " </GUH>\n" ^
1.73 -..................................................................*)
1.74 - indt (j+i) ^"</ORDER>\n" ^
1.75 - indt (j+i) ^"<ERLS>\n" ^
1.76 - indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
1.77 - indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
1.78 - indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
1.79 - (id_rls erls) ^ " </GUH>\n" ^
1.80 - indt (j+i) ^"</ERLS>\n" ^
1.81 - indt (j+i) ^"<SRLS>\n" ^
1.82 - indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
1.83 - indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
1.84 - indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
1.85 - (id_rls srls) ^ " </GUH>\n" ^
1.86 - indt (j+i) ^"</SRLS>\n" ^
1.87 - calcrefs2xml (j+i) (thyID, calc) ^
1.88 - scr2xml (j+i) scr ^
1.89 - indt j ^"</RULESET>\n" : xml;
1.90 -
1.91 -fun prepa12xml j (terms, term) =
1.92 - indt j ^"<PREPAT>\n"^
1.93 - indt (j+i) ^"<PRECONDS>\n"^
1.94 - terms2xml (j+2*i) terms ^
1.95 - indt (j+i) ^"</PRECONDS>\n"^
1.96 - indt (j+i) ^"<PATTERN>\n"^
1.97 - term2xml (j+2*i) term ^
1.98 - indt (j+i) ^"</PATTERN>\n"^
1.99 - indt j ^"</PREPAT>\n" : xml;
1.100 -
1.101 -fun prepat2xml j [] = ""
1.102 - | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;
1.103 -
1.104 -fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls)
1.105 - | rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)
1.106 - | rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)
1.107 - | rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
1.108 - indt j ^"<RULESET>\n"^
1.109 - indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
1.110 - indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
1.111 - prepat2xml (j+i) prepat ^
1.112 - indt (j+i) ^"<ORDER> " ^
1.113 - indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
1.114 - indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
1.115 -(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
1.116 - indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
1.117 - thyID) ord ^ " </GUH>\n" ^
1.118 -.................................................................*)
1.119 - indt (j+i) ^"</ORDER>\n" ^
1.120 - indt (j+i) ^"<ERLS> " ^
1.121 - indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
1.122 - indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
1.123 - indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) (id_rls erls) ^ " </GUH>\n" ^
1.124 - indt (j+i) ^"</ERLS>\n" ^
1.125 - calcrefs2xml (j+i) (thyID, calc) ^
1.126 - indt (j+i) ^"<SCRIPT>\n"^
1.127 - scr2xml (j+2*i) scr ^
1.128 - indt (j+i) ^" </SCRIPT>\n"^
1.129 - indt j ^"</RULESET>\n" : xml;
1.130 -
1.131 -(*WN060627 scope of thy's not considered ?!?*)
1.132 -fun thm''2xml j (thm : thm) =
1.133 - indt j ^ "<THEOREM>\n" ^
1.134 - indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
1.135 - term2xml j (Thm.prop_of thm) ^ "\n" ^
1.136 - indt j ^ "</THEOREM>\n" : xml;
1.137 -
1.138 -fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
1.139 - indt j ^ "<CALC>\n" ^
1.140 - indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
1.141 - indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge",
1.142 - thyID) scrop ^ "</GUH>\n" ^
1.143 - indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
1.144 - indt j ^ "</CALC>\n" : xml;
1.145 -
1.146 (* create the xml-files for the thydata in the hierarchy *)
1.147 val i = indentation;
1.148 (* analoguous to 'fun met2xml' *)