equal
deleted
inserted
replaced
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 val put_info = BrowserInfoData.put; |
85 val get_info = BrowserInfoData.get; |
86 val get_info = BrowserInfoData.get; |
86 val session_name = #name o get_info; |
87 val session_name = #name o get_info; |
|
88 |
|
89 val _ = Context.>> (Context.map_theory (put_info {name = "", session = [], is_local = false})); |
87 |
90 |
88 |
91 |
89 |
92 |
90 (** graphs **) |
93 (** graphs **) |
91 |
94 |
491 in |
494 in |
492 change_theory_info name prep_html_source; |
495 change_theory_info name prep_html_source; |
493 add_graph_entry (update_time, entry); |
496 add_graph_entry (update_time, entry); |
494 add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name)); |
497 add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name)); |
495 add_tex_index (update_time, Latex.theory_entry name); |
498 add_tex_index (update_time, Latex.theory_entry name); |
496 BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy |
499 put_info {name = sess_name, session = path, is_local = is_some remote_path} thy |
497 end); |
500 end); |
498 |
501 |
499 |
502 |
500 val hooks = ref ([]: (string -> (string * thm list) list -> unit) list); |
503 val hooks = ref ([]: (string -> (string * thm list) list -> unit) list); |
501 fun add_hook f = CRITICAL (fn () => change hooks (cons f)); |
504 fun add_hook f = CRITICAL (fn () => change hooks (cons f)); |