info: default name is "", not "Pure";
authorwenzelm
Mon, 23 Jun 2008 16:01:03 +0200
changeset 27327 efd626efcb04
parent 27326 d3beec370964
child 27328 1f0ac20db386
info: default name is "", not "Pure";
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Jun 23 15:51:38 2008 +0200
+++ b/src/Pure/Thy/present.ML	Mon Jun 23 16:01:03 2008 +0200
@@ -82,9 +82,12 @@
   fun merge _ _ = empty;
 );
 
+val put_info = BrowserInfoData.put;
 val get_info = BrowserInfoData.get;
 val session_name = #name o get_info;
 
+val _ = Context.>> (Context.map_theory (put_info {name = "", session = [], is_local = false}));
+
 
 
 (** graphs **)
@@ -493,7 +496,7 @@
     add_graph_entry (update_time, entry);
     add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
     add_tex_index (update_time, Latex.theory_entry name);
-    BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy
+    put_info {name = sess_name, session = path, is_local = is_some remote_path} thy
   end);