equal
deleted
inserted
replaced
208 Date.fmt ".%Y%m%d_%H%M%S__" (Date.fromTimeLocal (Time.now ())) ^ |
208 Date.fmt ".%Y%m%d_%H%M%S__" (Date.fromTimeLocal (Time.now ())) ^ |
209 serial_string () |
209 serial_string () |
210 |
210 |
211 fun encode_feature (name, weight) = |
211 fun encode_feature (name, weight) = |
212 encode_str name ^ |
212 encode_str name ^ |
213 (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight) |
213 (if Real.== (weight, 1.0) then "" else "=" ^ smart_string_of_real weight) |
214 |
214 |
215 val encode_features = map encode_feature #> space_implode " " |
215 val encode_features = map encode_feature #> space_implode " " |
216 |
216 |
217 fun str_of_learn (name, parents, feats, deps) = |
217 fun str_of_learn (name, parents, feats, deps) = |
218 "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ |
218 "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ |
328 |
328 |
329 val empty_state = {access_G = Graph.empty, dirty = SOME []} |
329 val empty_state = {access_G = Graph.empty, dirty = SOME []} |
330 |
330 |
331 local |
331 local |
332 |
332 |
333 val version = "*** MaSh version 20130113a ***" |
333 val version = "*** MaSh version 20130207a ***" |
334 |
334 |
335 exception Too_New of unit |
335 exception Too_New of unit |
336 |
336 |
337 fun extract_node line = |
337 fun extract_node line = |
338 case space_explode ":" line of |
338 case space_explode ":" line of |