79 manual_reorder = manual_reorder} |
79 manual_reorder = manual_reorder} |
80 |
80 |
81 fun merge_global_limit (NONE, NONE) = NONE |
81 fun merge_global_limit (NONE, NONE) = NONE |
82 | merge_global_limit (NONE, SOME n) = SOME n |
82 | merge_global_limit (NONE, SOME n) = SOME n |
83 | merge_global_limit (SOME n, NONE) = SOME n |
83 | merge_global_limit (SOME n, NONE) = SOME n |
84 | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m)) |
84 | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m)) (* FIXME odd merge *) |
85 |
85 |
86 structure Options = Theory_Data |
86 structure Options = Theory_Data |
87 ( |
87 ( |
88 type T = code_options |
88 type T = code_options |
89 val empty = {ensure_groundness = false, limit_globally = NONE, |
89 val empty = {ensure_groundness = false, limit_globally = NONE, |
94 limited_types = limited_types1, limited_predicates = limited_predicates1, |
94 limited_types = limited_types1, limited_predicates = limited_predicates1, |
95 replacing = replacing1, manual_reorder = manual_reorder1}, |
95 replacing = replacing1, manual_reorder = manual_reorder1}, |
96 {ensure_groundness = ensure_groundness2, limit_globally = limit_globally2, |
96 {ensure_groundness = ensure_groundness2, limit_globally = limit_globally2, |
97 limited_types = limited_types2, limited_predicates = limited_predicates2, |
97 limited_types = limited_types2, limited_predicates = limited_predicates2, |
98 replacing = replacing2, manual_reorder = manual_reorder2}) = |
98 replacing = replacing2, manual_reorder = manual_reorder2}) = |
99 {ensure_groundness = ensure_groundness1 orelse ensure_groundness2, |
99 {ensure_groundness = ensure_groundness1 orelse ensure_groundness2 (* FIXME odd merge *), |
100 limit_globally = merge_global_limit (limit_globally1, limit_globally2), |
100 limit_globally = merge_global_limit (limit_globally1, limit_globally2), |
101 limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2), |
101 limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2), |
102 limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2), |
102 limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2), |
103 manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2), |
103 manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2), |
104 replacing = Library.merge (op =) (replacing1, replacing2)}; |
104 replacing = Library.merge (op =) (replacing1, replacing2)}; |
120 structure System_Config = Generic_Data |
120 structure System_Config = Generic_Data |
121 ( |
121 ( |
122 type T = system_configuration |
122 type T = system_configuration |
123 val empty = {timeout = seconds 10.0, prolog_system = SWI_PROLOG} |
123 val empty = {timeout = seconds 10.0, prolog_system = SWI_PROLOG} |
124 val extend = I; |
124 val extend = I; |
125 fun merge ({timeout = timeout1, prolog_system = prolog_system1}, |
125 fun merge (a, _) = a |
126 {timeout = timeout2, prolog_system = prolog_system2}) = |
|
127 {timeout = timeout1, prolog_system = prolog_system1} |
|
128 ) |
126 ) |
129 |
127 |
130 (* general string functions *) |
128 (* general string functions *) |
131 |
129 |
132 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode; |
130 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode; |