equal
deleted
inserted
replaced
74 (** additional theory data **) |
74 (** additional theory data **) |
75 |
75 |
76 structure BrowserInfoData = TheoryDataFun |
76 structure BrowserInfoData = TheoryDataFun |
77 ( |
77 ( |
78 type T = {name: string, session: string list, is_local: bool}; |
78 type T = {name: string, session: string list, is_local: bool}; |
79 val empty = {name = "", session = [], is_local = false}: T; |
79 val empty = {name = Context.PureN, session = [], is_local = false}: T; |
80 val copy = I; |
80 val copy = I; |
81 fun extend _ = empty; |
81 fun extend _ = empty; |
82 fun merge _ _ = empty; |
82 fun merge _ _ = empty; |
83 ); |
83 ); |
84 |
84 |
85 fun get_info thy = |
85 val get_info = BrowserInfoData.get; |
86 if member (op =) [Context.PureN, Context.CPureN] (Context.theory_name thy) |
|
87 then {name = Context.PureN, session = [], is_local = false} |
|
88 else BrowserInfoData.get thy; |
|
89 |
|
90 val session_name = #name o get_info; |
86 val session_name = #name o get_info; |
91 |
87 |
92 |
88 |
93 |
89 |
94 (** graphs **) |
90 (** graphs **) |