# HG changeset patch
# User wenzelm
# Date 1594910305 -7200
# Node ID b9e9ff3a1e1c4630fa45d295d94701697d101f97
# Parent  c386d1b77762c5d3fae2dca60e45ea8c0e1060b9
more thorough extend/merge (for Theory.join_theory);

diff -r c386d1b77762 -r b9e9ff3a1e1c src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Jul 16 16:00:52 2020 +0200
+++ b/src/Pure/Thy/present.ML	Thu Jul 16 16:38:25 2020 +0200
@@ -36,22 +36,32 @@
 
 
 
-(** additional theory data **)
+(** theory data **)
+
+type browser_info = {chapter: string, name: string, bibtex_entries: string list};
+val empty_browser_info: browser_info = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []};
 
 structure Browser_Info = Theory_Data
 (
-  type T = {chapter: string, name: string, bibtex_entries: string list};
-  val empty = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []}: T;
-  fun extend _ = empty;
-  fun merge _ = empty;
+  type T = browser_info
+  val empty = empty_browser_info;
+  val extend = I;
+  val merge = #1;
 );
 
-val _ = Theory.setup
-  (Browser_Info.put {chapter = Context.PureN, name = Context.PureN, bibtex_entries = []});
+fun reset_browser_info thy =
+  if Browser_Info.get thy = empty_browser_info then NONE
+  else SOME (Browser_Info.put empty_browser_info thy);
+
+val _ =
+  Theory.setup
+   (Theory.at_begin reset_browser_info #>
+    Browser_Info.put {chapter = Context.PureN, name = Context.PureN, bibtex_entries = []});
 
 val get_bibtex_entries = #bibtex_entries o Browser_Info.get;
 
 
+
 (** global browser info state **)
 
 (* type theory_info *)