src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml
author Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
Sun, 02 Feb 2014 03:09:40 +0100
changeset 55380 7be2ad0e4acb
parent 55378 3f5c7d9b311a
child 55381 bc6c9dbfb124
permissions -rw-r--r--
ad 967c8a1eb6b1 (7): remove all code concerned with 'mets = Unsynchronized.ref'
neuper@37906
     1
(* export problem-data and method-data to xml
neuper@37906
     2
   author: Walther Neuper
neuper@37906
     3
   (c) isac-team
neuper@37906
     4
neuper@37906
     5
use"xmlsrc/pbl-met-hierarchy.sml";
neuper@37906
     6
use"pbl-met-hierarchy.sml";
neuper@37906
     7
*)
neuper@37906
     8
neuper@37906
     9
fun str2file (fnm:filename) (str:string) =
neuper@37906
    10
    let val file = TextIO.openOut fnm
neuper@37906
    11
    in (TextIO.output (file, str);
neuper@37906
    12
	TextIO.flushOut file;
neuper@37906
    13
	TextIO.closeOut file) end;
neuper@38031
    14
fun pos2filename [] = error "pos2filename called with []"
neuper@37906
    15
  | pos2filename [i] = "_" ^ string_of_int i ^ ".xml"
neuper@37906
    16
  | pos2filename (i::is) = "_" ^ string_of_int i ^ pos2filename is;
neuper@37906
    17
(* pos2filename [1,22,3];
neuper@37906
    18
val it = "_1_22_3.xml" : string
neuper@37906
    19
*)
neuper@38031
    20
fun id2filename [] = error "id2filename called with []"
neuper@37906
    21
  | id2filename [s] = s ^ ".xml"
neuper@37906
    22
  | id2filename (s::ss) = s ^ "_" ^ id2filename ss;
neuper@37906
    23
(* id2filename ["linear","univariate","equation"];
neuper@37906
    24
val it = "linear_univariate_equation.xml" : string
neuper@37906
    25
*)
neuper@37906
    26
neuper@37906
    27
neuper@37906
    28
neuper@37906
    29
(*ad DTD: a NODE contains an ID and zero or more NODEs*)
neuper@37906
    30
(*old version with pos2filename*)
neuper@37906
    31
fun hierarchy pm(*"pbl" | "met"*) h =
neuper@37906
    32
    let val j = indentation
neuper@37906
    33
	fun nd i p (Ptyp (id,_,ns)) = 
neuper@37906
    34
	    let val p' = lev_on p
neuper@37906
    35
	    in (indt i) ^ "<NODE>\n" ^ 
neuper@37906
    36
	       (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ 
neuper@37906
    37
	       (indt (i+j)) ^ "<NO> " (*on this level*) ^ 
neuper@37906
    38
	       (string_of_int o last_elem) p' ^ " </NO>\n" ^ 
neuper@37906
    39
	       (indt (i+j)) ^ "<CONTENTREF> " ^ pm ^ pos2filename p' ^ 
neuper@37906
    40
	       " </CONTENTREF>\n" ^
neuper@37906
    41
	       (nds (i+j) (lev_dn p') ns) ^ 
neuper@37906
    42
	       (indt i) ^ "</NODE>\n"
neuper@37906
    43
	    end
neuper@37906
    44
	and nds _ _ [] = ""
neuper@37906
    45
	  | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
neuper@37906
    46
    in nds j [0] h end;
neuper@37906
    47
(*.create a hierarchy with references to the guh's.*)
neuper@37906
    48
fun hierarchy_pbl h =
neuper@37906
    49
    let val j = indentation
neuper@37906
    50
	fun nd i p (Ptyp (id,[n as {guh,...} : pbt],ns)) = 
neuper@37906
    51
	    let val p' = lev_on p
neuper@37906
    52
	    in (indt i) ^ "<NODE>\n" ^ 
neuper@37906
    53
	       (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ 
neuper@37906
    54
	       (indt (i+j)) ^ "<NO> " (*on this level*) ^ 
neuper@37906
    55
	       (string_of_int o last_elem) p' ^ " </NO>\n" ^ 
neuper@37906
    56
	       (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^ 
neuper@37906
    57
	       " </CONTENTREF>\n" ^
neuper@37906
    58
	       (nds (i+j) (lev_dn p') ns) ^ 
neuper@37906
    59
	       (indt i) ^ "</NODE>\n"
neuper@37906
    60
	    end
neuper@37906
    61
	and nds _ _ [] = "" 
neuper@37906
    62
	  | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
neuper@37906
    63
    in nds j [0] h : xml end;
neuper@37906
    64
fun hierarchy_met h =
neuper@37906
    65
    let val j = indentation
neuper@37906
    66
	fun nd i p (Ptyp (id,[n as {guh,...} : met],ns)) = 
neuper@37906
    67
	    let val p' = lev_on p
neuper@37906
    68
	    in (indt i) ^ "<NODE>\n" ^ 
neuper@37906
    69
	       (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ 
neuper@37906
    70
	       (indt (i+j)) ^ "<NO> " (*on this level*) ^ 
neuper@37906
    71
	       (string_of_int o last_elem) p' ^ " </NO>\n" ^ 
neuper@37906
    72
	       (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^ 
neuper@37906
    73
	       " </CONTENTREF>\n" ^
neuper@37906
    74
	       (nds (i+j) (lev_dn p') ns) ^ 
neuper@37906
    75
	       (indt i) ^ "</NODE>\n"
neuper@37906
    76
	    end
neuper@37906
    77
	and nds _ _ [] = ""
neuper@37906
    78
	  | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
neuper@37906
    79
    in nds j [0] h  : xml end;
neuper@38031
    80
(* (writeln o hierarchy_pbl) (!ptyps);
neuper@37906
    81
   *)
neuper@37906
    82
neuper@37906
    83
fun pbl_hierarchy2file (path:path) = 
neuper@37906
    84
    str2file (path ^ "pbl_hierarchy.xml") 
neuper@37906
    85
	     ("<NODE>\n" ^
neuper@37906
    86
	      "  <ID> problem hierarchy </ID>\n" ^
neuper@37906
    87
	      "  <NO> 1 </NO>\n" ^
neuper@37906
    88
	      "  <CONTENTREF> pbl_ROOT </CONTENTREF>\n" ^
s1210629013@55338
    89
	     (hierarchy_pbl (get_ptyps ())) ^
neuper@37906
    90
	     "</NODE>");
neuper@37906
    91
neuper@37906
    92
fun met_hierarchy2file (path:path) = 
neuper@37906
    93
    str2file (path ^ "met_hierarchy.xml") 
neuper@37906
    94
	     ("<NODE>\n" ^
neuper@37906
    95
	      "  <ID> method hierarchy </ID>\n" ^
neuper@37906
    96
	      "  <NO> 1 </NO>\n" ^
neuper@37906
    97
	      "  <CONTENTREF> met_ROOT </CONTENTREF>\n" ^
s1210629013@55372
    98
	     (hierarchy_met (get_mets ())) ^
neuper@37906
    99
	     "</NODE>");
neuper@37906
   100
neuper@37906
   101
neuper@37906
   102
neuper@37906
   103
(**.create the xml-files for the pbls, mets from the hierarchy.**)
neuper@37906
   104
neuper@37906
   105
val i = indentation;
neuper@37906
   106
neuper@42404
   107
fun pbl2term thy (pblRD:pblRD) = (*WN120405.TODO.txt*)
neuper@42404
   108
  str2term ("Problem (" ^ (get_thy o theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
neuper@40836
   109
(* term2str (pbl2term (Thy_Info.get_theory "Isac") ["equations","univariate","normalize"]);
neuper@37906
   110
val it = "Problem (Isac, [normalize, univariate, equations])" : string
neuper@37906
   111
*)
neuper@37906
   112
neuper@37906
   113
neuper@37906
   114
(*.format a problem in xml for presentation on the problem browser;
neuper@37906
   115
   new version with <KESTOREREF>s -- not used because linking
neuper@37906
   116
   requires elements (rls, calc, ...) to be reorganized.*)
neuper@37906
   117
(*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
neuper@37906
   118
fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
neuper@37906
   119
			 thy,where_}:pbt) =
neuper@37906
   120
    let val thy' = theory2theory' thy
neuper@37906
   121
	val prls' = (#id o rep_rls) prls
neuper@37906
   122
    in "<NODECONTENT>\n" ^
neuper@37906
   123
       indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
neuper@37906
   124
       (((id2xml i)(* o rev*)) id) ^ 
neuper@37906
   125
       indt i ^ "<META> </META>\n" ^
neuper@37906
   126
       (*--------------- begin display ------------------------------*)
neuper@37906
   127
       indt i ^ "<HEADLINE>\n" ^
neuper@37926
   128
       (case cas of NONE => term2xml i (pbl2term thy id)
neuper@37926
   129
		  | SOME t => term2xml i t) ^ "\n" ^
neuper@37906
   130
       indt i ^ "</HEADLINE>\n" ^
neuper@37906
   131
       (*--------------- hline --------------------------------------*)
neuper@37906
   132
       pattern2xml i ppc where_ ^
neuper@37906
   133
       (*--------------- hline --------------------------------------*)
neuper@37906
   134
       indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n"
neuper@37906
   135
       (*--------------- end display --------------------------------*)
neuper@37906
   136
       ^
neuper@37906
   137
       indt i ^ "<THEORY>\n" ^ 
neuper@37906
   138
       theref2xml (i+i) thy' "Theorems" "" ^
neuper@37906
   139
       indt i ^ "</THEORY>\n" ^
neuper@37906
   140
       (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
neuper@37906
   141
		  | _ => (indt i) ^ "<METHODS>\n" ^
neuper@37906
   142
			 foldl op^ ("", map (keref2xml (i+i) Met_) met) ^
neuper@37906
   143
			 (indt i) ^ "</METHODS>\n") ^
neuper@37906
   144
       indt i ^ "<EVALPRECOND>\n" ^ 
neuper@37906
   145
       theref2xml (i+i) (snd (thy_containing_rls thy' prls')) "Rulesets" prls'^
neuper@37906
   146
       indt i ^ "</EVALPRECOND>\n" ^
neuper@37906
   147
       authors2xml i "MATHAUTHORS" mathauthors ^
neuper@37906
   148
       authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
neuper@37906
   149
       "</NODECONTENT>" : xml
neuper@37906
   150
    end;
neuper@37906
   151
neuper@37906
   152
(*.format a problem in xml for presentation on the problem browser;
neuper@37906
   153
   old version with 'dead' strings for rls, calc, ....*)
neuper@37906
   154
(* 
neuper@37906
   155
val pblID = ["linear","univariate","equation"];
neuper@37906
   156
val pblID = ["degree_4","polynomial","univariate","equation"];
neuper@37906
   157
val pblID = rev ["tool","find_values"];
neuper@37906
   158
val (id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}:pbt) =
neuper@37906
   159
       (pblID, get_pbt pblID);
neuper@37906
   160
   *)
neuper@37906
   161
fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
neuper@37906
   162
			 thy,where_}:pbt) =
neuper@37906
   163
    "<NODECONTENT>\n" ^
neuper@37906
   164
    indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
neuper@37906
   165
    (((id2xml i)(* o rev*)) id) ^ 
neuper@37906
   166
    indt i ^ "<META> </META>\n" ^
neuper@37906
   167
    (*--------------- begin display ------------------------------*)
neuper@37906
   168
    indt i ^ "<HEADLINE>\n" ^
neuper@37926
   169
    (case cas of NONE => term2xml i (pbl2term thy id)
neuper@37926
   170
	       | SOME t => term2xml i t) ^ "\n" ^
neuper@37906
   171
    indt i ^ "</HEADLINE>\n" ^
neuper@37906
   172
    (*--------------- hline --------------------------------------*)
neuper@37906
   173
    pattern2xml i ppc where_ ^
neuper@37906
   174
    (*--------------- hline --------------------------------------*)
neuper@37906
   175
    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n"
neuper@37906
   176
    (*--------------- end display --------------------------------*)
neuper@37906
   177
    ^
neuper@37906
   178
    indt i ^ "<THEORY>\n" ^ 
neuper@37906
   179
    theref2xml (i+i) (theory2theory' thy) "Theorems" "" ^
neuper@37906
   180
    indt i ^ "</THEORY>\n" ^
neuper@37906
   181
    (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
neuper@37906
   182
	       | _ => (indt i) ^ "<METHODS>\n" ^
neuper@37906
   183
		      foldl op^ ("", map (keref2xml (i+i) Met_) met) ^
neuper@37906
   184
		      (indt i) ^ "</METHODS>\n") ^
neuper@37906
   185
    indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls) 
neuper@37906
   186
				    prls ^ " </EVALPRECOND>\n" ^ 
neuper@37906
   187
    authors2xml i "MATHAUTHORS" mathauthors ^
neuper@37906
   188
    authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
neuper@37906
   189
    "</NODECONTENT>" : xml;
neuper@37906
   190
(* 
neuper@37906
   191
val pblID = ["linear","univariate","equation"];
neuper@37906
   192
val pblID = ["degree_4","polynomial","univariate","equation"];
neuper@38031
   193
writeln (pbl2xml pblID (get_pbt pblID));
neuper@37906
   194
*)
neuper@37906
   195
neuper@37906
   196
(*replace by 'fun calc2xml' as developed for thy in 0607*)
neuper@37906
   197
fun calc2xmlOLD j ((scr_op, (isa_op, _)):calc) =
neuper@37906
   198
    indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";
neuper@37906
   199
fun calcs2xmlOLD j [] = ("":xml) (*TODO replace with 'strs2xml'*)
neuper@37906
   200
  | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
neuper@37906
   201
neuper@37906
   202
(*.format a method in xml for presentation on the method browser;
neuper@37906
   203
   new version with <KESTOREREF>s -- not used because linking
neuper@37906
   204
   requires elements (rls, calc, ...) to be reorganized.*)
neuper@37906
   205
(*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
neuper@37906
   206
fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
neuper@42425
   207
			 crls,erls,errpats,nrls,prls,srls,rew_ord'}:met) =
neuper@38050
   208
    let val thy' = "Isac" (*FIXME.WN0607 get thy from met ?!?*)
neuper@37906
   209
	val crls' = (#id o rep_rls) crls
neuper@37906
   210
	val erls' = (#id o rep_rls) erls
neuper@37906
   211
	val nrls' = (#id o rep_rls) nrls
neuper@37906
   212
	val prls' = (#id o rep_rls) prls
neuper@37906
   213
	val srls' = (#id o rep_rls) srls
neuper@37906
   214
    in "<NODECONTENT>\n" ^
neuper@37906
   215
       indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
neuper@37906
   216
       id2xml i id ^ 
neuper@37906
   217
       indt i ^ "<META> </META>\n" ^
neuper@37906
   218
       scr2xml i scr ^
neuper@37906
   219
       pattern2xml i ppc pre ^
neuper@37906
   220
       indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
neuper@37906
   221
       indt i ^ "<EVALPRECOND>\n" ^ 
neuper@37906
   222
       theref2xml (i+i) (snd (thy_containing_rls thy' prls')) "Rulesets" prls'^
neuper@37906
   223
       indt i ^ "</EVALPRECOND>\n" ^
neuper@37906
   224
       indt i ^ "<EVALCOND>\n"    ^ 
neuper@37906
   225
       theref2xml (i+i) (snd (thy_containing_rls thy' erls')) "Rulesets" erls'^
neuper@37906
   226
       indt i ^ "</EVALCOND>\n" ^
neuper@37906
   227
       indt i ^ "<EVALLISTEXPR>\n"^ 
neuper@37906
   228
       theref2xml (i+i) (snd (thy_containing_rls thy' srls')) "Rulesets" srls'^
neuper@37906
   229
       indt i ^ "</EVALLISTEXPR>\n" ^
neuper@37906
   230
       indt i ^ "<CHECKELEMENTWISE>\n" ^ 
neuper@37906
   231
       theref2xml (i+i) (snd (thy_containing_rls thy' crls')) "Rulesets" crls'^
neuper@37906
   232
       indt i ^ "</CHECKELEMENTWISE>\n" ^
neuper@37906
   233
       indt i ^ "<NORMALFORM>\n"  ^ 
neuper@37906
   234
       theref2xml (i+i) (snd (thy_containing_rls thy' nrls')) "Rulesets" nrls'^
neuper@37906
   235
       indt i ^ "</NORMALFORM>\n" ^
neuper@37906
   236
       indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
neuper@37906
   237
       calcs2xmlOLD i calc ^
neuper@37906
   238
       authors2xml i "MATHAUTHORS" mathauthors ^
neuper@37906
   239
       authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
neuper@37906
   240
       "</NODECONTENT>" : xml
neuper@37906
   241
    end;
neuper@37906
   242
(*.format a method in xml for presentation on the method browser;
neuper@37906
   243
   old version with 'dead' strings for rls, calc, ....*)
neuper@37906
   244
fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
neuper@42425
   245
			 crls,erls,errpats,nrls,prls,srls,rew_ord'}:met) =
neuper@37906
   246
    "<NODECONTENT>\n" ^
neuper@37906
   247
    indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
neuper@37906
   248
    id2xml i id ^ 
neuper@37906
   249
    indt i ^ "<META> </META>\n" ^
neuper@37906
   250
    scr2xml i scr ^
neuper@37906
   251
    pattern2xml i ppc pre ^
neuper@37906
   252
    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
neuper@37906
   253
    indt i ^ "<EVALPRECOND> " ^  (#id o rep_rls) prls ^ " </EVALPRECOND>\n" ^
neuper@37906
   254
    indt i ^ "<EVALCOND> " ^ (#id o rep_rls) erls ^ " </EVALCOND>\n" ^
neuper@37906
   255
    indt i ^ "<EVALLISTEXPR> "^ (#id o rep_rls) srls ^ " </EVALLISTEXPR>\n" ^
neuper@37906
   256
    indt i ^ "<CHECKELEMENTWISE> " ^ (#id o rep_rls) 
neuper@37906
   257
					 crls ^ " </CHECKELEMENTWISE>\n" ^
neuper@37906
   258
    indt i ^ "<NORMALFORM> "  ^ (#id o rep_rls) nrls ^ " </NORMALFORM>\n" ^
neuper@37906
   259
    indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
neuper@37906
   260
    calcs2xmlOLD i calc ^
neuper@37906
   261
    authors2xml i "MATHAUTHORS" mathauthors ^
neuper@37906
   262
    authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
neuper@37906
   263
    "</NODECONTENT>" : xml;
neuper@37906
   264
neuper@38031
   265
(* writeln (met2xml ["Test", "solve_linear"]
neuper@37906
   266
		    (get_met ["Test", "solve_linear"]));
neuper@37906
   267
   *)
neuper@37906
   268
neuper@37906
   269
(**. write pbls from hierarchy to files.**)
neuper@37906
   270
neuper@37906
   271
(*.write the files using an int-key (pos') as filename.*)
neuper@37906
   272
fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
neuper@38031
   273
    (writeln ("### pbl2file: id = " ^ strs2str id);
neuper@37906
   274
    ((str2file (path ^ pos2filename pos)) o (pbl2xml id)) pbl
neuper@37906
   275
    );
neuper@37906
   276
neuper@37906
   277
(*.write the files using the guh as filename.*)
neuper@37906
   278
(*    *)
neuper@37906
   279
fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
neuper@38031
   280
    (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ pos2str pos);
neuper@37906
   281
     ((str2file (path ^ guh2filename guh)) o (pbl2xml id)) pbl
neuper@37906
   282
     );
neuper@37906
   283
    
neuper@37906
   284
(**. write mets from hierarchy to files.**)
neuper@37906
   285
neuper@37906
   286
(*.write the files using an int-key (pos') as filename.*)
neuper@37906
   287
fun met2file (path:path) (pos:pos) (id:metID) met =
neuper@38031
   288
    (writeln ("### met2file: id = " ^ strs2str id);
neuper@37906
   289
     ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
neuper@37906
   290
neuper@37906
   291
(*.write the files using the guh as filename.*)
neuper@37906
   292
fun met2file (path:path) (pos:pos) (id:metID) (met as {guh,...}) =
neuper@38031
   293
    (writeln ("### met2file: id = " ^ strs2str id);
neuper@37906
   294
     ((str2file (path ^ guh2filename guh)) o (met2xml id)) met);
neuper@37906
   295
neuper@37906
   296
neuper@42404
   297
(*.scan the mtree Ptyp and print the nodes using wfn.*)
neuper@37906
   298
fun node (pa:path) ids po wfn (Ptyp (id,[n],ns)) = 
neuper@37906
   299
    let val po' = lev_on po
neuper@42404
   300
    in
neuper@42404
   301
      wfn pa po' (ids@[id]) n; 
neuper@42404
   302
      nodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns
neuper@42404
   303
    end
neuper@37906
   304
and nodes _ _ _ _ [] = ()
neuper@42404
   305
  | nodes pa ids po wfn (n::ns) =
neuper@42404
   306
      (node pa ids po wfn n; nodes pa ids (lev_on po) wfn ns);
neuper@37906
   307
neuper@37906
   308
s1210629013@55338
   309
fun pbls2file (p:path) = nodes p [] [0] pbl2file (get_ptyps ());
s1210629013@55372
   310
fun mets2file (p:path) = nodes p [] [0] met2file (get_mets ());
neuper@37906
   311
(*
neuper@37906
   312
val path = "/home/neuper/proto2/isac/xmldata/"; 
neuper@37906
   313
val path = "/home/neuper/tmp/"; 
neuper@37906
   314
neuper@37906
   315
pbl_hierarchy2file (path ^ "pbl/");
neuper@37906
   316
pbls2file          (path ^ "pbl/");
neuper@37906
   317
neuper@37906
   318
met_hierarchy2file (path ^ "met/");
neuper@37906
   319
mets2file          (path ^ "met/");
neuper@37906
   320
neuper@37906
   321
thy_hierarchy2file (path ^ "thy/");
neuper@37906
   322
thes2file          (path ^ "thy/");
neuper@42452
   323
*)
neuper@42452
   324
neuper@42452
   325
fun update_metdata
neuper@42452
   326
  ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: met)
neuper@42452
   327
    errpats' =
neuper@42452
   328
  {guh = guh, mathauthors = mathauthors, init = init, rew_ord' = rew_ord', erls = erls,
neuper@42452
   329
    srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc,
neuper@42452
   330
    ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: met
neuper@42452
   331
s1210629013@55378
   332
fun update_metpair metID errpats = let
s1210629013@55378
   333
        val ret = (update_metdata (get_met metID) errpats, metID)
s1210629013@55378
   334
          handle ERROR _ => error ("update_metpair: " ^ (strs2str metID) ^ "must address a method");
s1210629013@55378
   335
      in ret end;