equal
deleted
inserted
replaced
311 |
311 |
312 val empty_state = {access_G = Graph.empty, dirty = SOME []} |
312 val empty_state = {access_G = Graph.empty, dirty = SOME []} |
313 |
313 |
314 local |
314 local |
315 |
315 |
316 val version = "*** MaSh version 20130111a ***" |
316 val version = "*** MaSh version 20130112a ***" |
317 |
317 |
318 exception Too_New of unit |
318 exception Too_New of unit |
319 |
319 |
320 fun extract_node line = |
320 fun extract_node line = |
321 case space_explode ":" line of |
321 case space_explode ":" line of |