equal
deleted
inserted
replaced
66 structure Solvers = Generic_Data |
66 structure Solvers = Generic_Data |
67 ( |
67 ( |
68 type T = (solver_info * string list) Symtab.table * string option |
68 type T = (solver_info * string list) Symtab.table * string option |
69 val empty = (Symtab.empty, NONE) |
69 val empty = (Symtab.empty, NONE) |
70 val extend = I |
70 val extend = I |
71 fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s (* FIXME merge options!? *)) |
71 fun merge ((ss1, s1), (ss2, s2)) = |
|
72 (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2)) |
72 ) |
73 ) |
73 |
74 |
74 fun set_solver_options (name, options) = |
75 fun set_solver_options (name, options) = |
75 let val opts = String.tokens (Symbol.is_ascii_blank o str) options |
76 let val opts = String.tokens (Symbol.is_ascii_blank o str) options |
76 in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end |
77 in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end |