# HG changeset patch
# User wenzelm
# Date 1301163390 -3600
# Node ID 12875677300b9cacbb3476be4d23b4a8b77120cd
# Parent  a8cbb93711546f9af4d19b68968582e0287b6ab5
tuned;

diff -r a8cbb9371154 -r 12875677300b src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Mar 26 19:16:20 2011 +0100
+++ b/src/Pure/Thy/present.ML	Sat Mar 26 19:16:30 2011 +0100
@@ -228,7 +228,7 @@
 
 val session_info = Unsynchronized.ref (NONE: session_info option);
 
-fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
+fun session_default x f = (case ! session_info of NONE => x | SOME info => f info);
 
 
 
@@ -362,7 +362,7 @@
 
 
 fun finish () =
-  with_session () (fn {name, info, html_prefix, doc_format,
+  session_default () (fn {name, info, html_prefix, doc_format,
     doc_graph, documents, dump_prefix, path, verbose, readme, ...} =>
   let
     val {theories, files, tex_index, html_index, graph} = ! browser_info;
@@ -433,13 +433,13 @@
 
 (* theory elements *)
 
-fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info);
+fun init_theory name = session_default () (fn _ => init_theory_info name empty_theory_info);
 
 fun theory_source name mk_text =
-  with_session () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
+  session_default () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
 
 fun theory_output name s =
-  with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s));
+  session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s));
 
 
 fun parent_link remote_path curr_session thy =
@@ -455,7 +455,7 @@
   in (link, name) end;
 
 fun begin_theory update_time dir files thy =
-    with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
+    session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
   let
     val name = Context.theory_name thy;
     val parents = Theory.parents_of thy;