equal
deleted
inserted
replaced
417 scr = EmptyScr: scr}:met; |
417 scr = EmptyScr: scr}:met; |
418 |
418 |
419 |
419 |
420 (** problem-types stored in format for usage in specify **) |
420 (** problem-types stored in format for usage in specify **) |
421 (*25.8.01 ---- |
421 (*25.8.01 ---- |
422 val pbltypes = ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*) |
422 val pbltypes = Unsynchronized.ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*) |
423 (term * (* description *) |
423 (term * (* description *) |
424 term)) (* id | struct-var *) |
424 term)) (* id | struct-var *) |
425 list) |
425 list) |
426 ) list);*) |
426 ) list);*) |
427 |
427 |
455 |
455 |
456 val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]); |
456 val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]); |
457 val e_Mets = Ptyp ("e_metID",[e_met],[]); |
457 val e_Mets = Ptyp ("e_metID",[e_met],[]); |
458 |
458 |
459 type ptyps = (pbt ptyp) list; |
459 type ptyps = (pbt ptyp) list; |
460 val ptyps = ref ([e_Ptyp]:ptyps); |
460 val ptyps = Unsynchronized.ref ([e_Ptyp]:ptyps); |
461 |
461 |
462 type mets = (met ptyp) list; |
462 type mets = (met ptyp) list; |
463 val mets = ref ([e_Mets]:mets); |
463 val mets = Unsynchronized.ref ([e_Mets]:mets); |
464 |
464 |
465 |
465 |
466 (**+ breadth-first search on hierarchy of problem-types +**) |
466 (**+ breadth-first search on hierarchy of problem-types +**) |
467 |
467 |
468 type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*) |
468 type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*) |