--- 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;
-