src/Pure/Thy/browser_info.ML

 end;
 
 structure BrowserInfo: BROWSER_INFO =
 struct
 
+
 (** paths **)
 
 val output_path = Path.variable "ISABELLE_BROWSER_INFO";
 
 fun top_path sess_path offset = Path.append (Path.appends (replicate (offset + length sess_path) Path.parent));

 val index_path = Path.basic "index.html";
 
 val session_path = Path.basic ".session";
 val session_entries_path = Path.unpack ".session/entries";
 val pre_index_path = Path.unpack ".session/pre-index";
+
 
 
 (** additional theory data **)
 
 structure BrowserInfoArgs =

   fun merge _ = empty;
   fun print _ _ = ();
 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 **)
 
 type graph_node =
   {name: string, ID: string, dir: string, unfold: bool,

 
 fun add_graph_entry' (entry as {ID, ...}) (gr : graph_node list) =
   filter_out (fn entry' => #ID entry' = ID) gr @ [entry];
 
 
+
 (** global browser info state **)
 
 (* type theory_info *)
 
 type theory_info = {source: Buffer.T, html: Buffer.T};

 
 
 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));
 
 fun add_source name txt = change_theory_info name (fn (source, html) =>
   (Buffer.add txt source, html));
 
 fun add_html name txt = change_theory_info name (fn (source, html) =>
   (source, Buffer.add txt html));
+
 
 
 (** global session state **)
 
 (* session_info *)

 
 val session_info = ref (None: session_info option);
 
 fun with_session x f = (case ! session_info of None => x | Some info => f info);
 fun with_context f = f (PureThy.get_name (Context.the_context ()));
+
 
 
 (** HTML output **)
 
 (* maintain index *)

 
 fun theorem name thm = with_session () (fn _ => with_context add_html (HTML.theorem name thm));
 fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
 
 
+
+(** theory setup **)
+
+val setup = [BrowserInfoData.init];
+
+
 end;
-