equal
deleted
inserted
replaced
76 val name = "Pure/browser_info"; |
76 val name = "Pure/browser_info"; |
77 type T = {name: string, session: string list, is_local: bool}; |
77 type T = {name: string, session: string list, is_local: bool}; |
78 |
78 |
79 val empty = {name = "Pure", session = [], is_local = false}; |
79 val empty = {name = "Pure", session = [], is_local = false}; |
80 val copy = I; |
80 val copy = I; |
|
81 val finish = I; |
81 fun prep_ext _ = {name = "", session = [], is_local = false}; |
82 fun prep_ext _ = {name = "", session = [], is_local = false}; |
82 fun merge _ = empty; |
83 fun merge _ = empty; |
83 fun print _ _ = (); |
84 fun print _ _ = (); |
84 end; |
85 end; |
85 |
86 |