tuned;
authorwenzelm
Sat Mar 26 19:16:30 2011 +0100 (2011-03-26)
changeset 4212612875677300b
parent 42125 a8cbb9371154
child 42127 8223e7f4b0da
tuned;
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/present.ML	Sat Mar 26 19:16:20 2011 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sat Mar 26 19:16:30 2011 +0100
     1.3 @@ -228,7 +228,7 @@
     1.4  
     1.5  val session_info = Unsynchronized.ref (NONE: session_info option);
     1.6  
     1.7 -fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
     1.8 +fun session_default x f = (case ! session_info of NONE => x | SOME info => f info);
     1.9  
    1.10  
    1.11  
    1.12 @@ -362,7 +362,7 @@
    1.13  
    1.14  
    1.15  fun finish () =
    1.16 -  with_session () (fn {name, info, html_prefix, doc_format,
    1.17 +  session_default () (fn {name, info, html_prefix, doc_format,
    1.18      doc_graph, documents, dump_prefix, path, verbose, readme, ...} =>
    1.19    let
    1.20      val {theories, files, tex_index, html_index, graph} = ! browser_info;
    1.21 @@ -433,13 +433,13 @@
    1.22  
    1.23  (* theory elements *)
    1.24  
    1.25 -fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info);
    1.26 +fun init_theory name = session_default () (fn _ => init_theory_info name empty_theory_info);
    1.27  
    1.28  fun theory_source name mk_text =
    1.29 -  with_session () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
    1.30 +  session_default () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
    1.31  
    1.32  fun theory_output name s =
    1.33 -  with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s));
    1.34 +  session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s));
    1.35  
    1.36  
    1.37  fun parent_link remote_path curr_session thy =
    1.38 @@ -455,7 +455,7 @@
    1.39    in (link, name) end;
    1.40  
    1.41  fun begin_theory update_time dir files thy =
    1.42 -    with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
    1.43 +    session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
    1.44    let
    1.45      val name = Context.theory_name thy;
    1.46      val parents = Theory.parents_of thy;