src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml
branchisac-update-Isa09-2
changeset 38050 4c52ad406c20
parent 38031 460c24a6a6ba
child 40836 69364e021751
equal deleted inserted replaced
38049:02a1cce684a7 38050:4c52ad406c20
   106 
   106 
   107 fun pbl2term thy (pblRD:pblRD) =
   107 fun pbl2term thy (pblRD:pblRD) =
   108     str2term ("Problem (" ^ 
   108     str2term ("Problem (" ^ 
   109 	      (get_thy o theory2domID) thy ^ "_, " ^
   109 	      (get_thy o theory2domID) thy ^ "_, " ^
   110 	      (strs2str' o rev) pblRD ^ ")");
   110 	      (strs2str' o rev) pblRD ^ ")");
   111 (* term2str (pbl2term Isac.thy ["equations","univariate","normalize"]);
   111 (* term2str (pbl2term (theory "Isac") ["equations","univariate","normalize"]);
   112 val it = "Problem (Isac, [normalize, univariate, equations])" : string
   112 val it = "Problem (Isac, [normalize, univariate, equations])" : string
   113 *)
   113 *)
   114 
   114 
   115 
   115 
   116 (*.format a problem in xml for presentation on the problem browser;
   116 (*.format a problem in xml for presentation on the problem browser;
   211    new version with <KESTOREREF>s -- not used because linking
   211    new version with <KESTOREREF>s -- not used because linking
   212    requires elements (rls, calc, ...) to be reorganized.*)
   212    requires elements (rls, calc, ...) to be reorganized.*)
   213 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
   213 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
   214 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
   214 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
   215 			 crls,erls,nrls,prls,srls,rew_ord'}:met) =
   215 			 crls,erls,nrls,prls,srls,rew_ord'}:met) =
   216     let val thy' = "Isac.thy" (*FIXME.WN0607 get thy from met ?!?*)
   216     let val thy' = "Isac" (*FIXME.WN0607 get thy from met ?!?*)
   217 	val crls' = (#id o rep_rls) crls
   217 	val crls' = (#id o rep_rls) crls
   218 	val erls' = (#id o rep_rls) erls
   218 	val erls' = (#id o rep_rls) erls
   219 	val nrls' = (#id o rep_rls) nrls
   219 	val nrls' = (#id o rep_rls) nrls
   220 	val prls' = (#id o rep_rls) prls
   220 	val prls' = (#id o rep_rls) prls
   221 	val srls' = (#id o rep_rls) srls
   221 	val srls' = (#id o rep_rls) srls