# HG changeset patch
# User wenzelm
# Date 926969718 -7200
# Node ID bf421d724db7724d2d244aa33d0180850487fae7
# Parent  f679ddd1ddd8a47544d9cf5cb695233a9c10b903
tuned;

diff -r f679ddd1ddd8 -r bf421d724db7 src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Mon May 17 21:34:45 1999 +0200
+++ b/src/Pure/Thy/browser_info.ML	Mon May 17 21:35:18 1999 +0200
@@ -25,6 +25,7 @@
 structure BrowserInfo: BROWSER_INFO =
 struct
 
+
 (** paths **)
 
 val output_path = Path.variable "ISABELLE_BROWSER_INFO";
@@ -41,6 +42,7 @@
 val pre_index_path = Path.unpack ".session/pre-index";
 
 
+
 (** additional theory data **)
 
 structure BrowserInfoArgs =
@@ -56,9 +58,12 @@
 end;
 
 structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs);
-val setup = [BrowserInfoData.init];
-fun get_info thy = if PureThy.get_name thy = "ProtoPure" then BrowserInfoArgs.empty
-  else BrowserInfoData.get thy;  (** FIXME!? **)
+
+fun get_info thy =
+  if Theory.eq_thy (thy, ProtoPure.thy) then BrowserInfoArgs.empty
+  else BrowserInfoData.get thy;
+
+
 
 (** graphs **)
 
@@ -103,6 +108,7 @@
   filter_out (fn entry' => #ID entry' = ID) gr @ [entry];
 
 
+
 (** global browser info state **)
 
 (* type theory_info *)
@@ -153,11 +159,11 @@
 fun add_index txt = change_browser_info (fn (theories, index, graph, all_graph) =>
   (theories, Buffer.add txt index, graph, all_graph));
 
-(** add entry to graph for current session **)
+(*add entry to graph for current session*)
 fun add_graph_entry e = change_browser_info (fn (theories, index, graph, all_graph) =>
   (theories, index, add_graph_entry' e graph, all_graph));
 
-(** add entry to graph for all sessions **)
+(*add entry to graph for all sessions*)
 fun add_all_graph_entry e = change_browser_info (fn (theories, index, graph, all_graph) =>
   (theories, index, graph, add_graph_entry' e all_graph));
 
@@ -168,6 +174,7 @@
   (source, Buffer.add txt html));
 
 
+
 (** global session state **)
 
 (* session_info *)
@@ -190,6 +197,7 @@
 fun with_context f = f (PureThy.get_name (Context.the_context ()));
 
 
+
 (** HTML output **)
 
 (* maintain index *)
@@ -348,5 +356,10 @@
 fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
 
 
+
+(** theory setup **)
+
+val setup = [BrowserInfoData.init];
+
+
 end;
-