equal
deleted
inserted
replaced
50 (** additional theory data **) |
50 (** additional theory data **) |
51 |
51 |
52 structure Browser_Info = Theory_Data |
52 structure Browser_Info = Theory_Data |
53 ( |
53 ( |
54 type T = {chapter: string, name: string}; |
54 type T = {chapter: string, name: string}; |
55 val empty = {chapter = Context.PureN, name = Context.PureN}: T; |
55 val empty = {chapter = "Unsorted", name = "Unknown"}: T; |
56 fun extend _ = empty; |
56 fun extend _ = empty; |
57 fun merge _ = empty; |
57 fun merge _ = empty; |
58 ); |
58 ); |
|
59 |
|
60 val _ = Context.>> (Context.map_theory |
|
61 (Browser_Info.put {chapter = Context.PureN, name = Context.PureN})); |
59 |
62 |
60 val session_name = #name o Browser_Info.get; |
63 val session_name = #name o Browser_Info.get; |
61 val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get; |
64 val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get; |
62 |
65 |
63 |
66 |