src/Pure/Thy/present.ML
changeset 59173 cdcbda56b05b
parent 59058 a78612c67ec0
child 59207 6b030dc97a4f
     1.1 --- a/src/Pure/Thy/present.ML	Mon Dec 22 14:33:53 2014 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Mon Dec 22 14:35:42 2014 +0100
     1.3 @@ -134,9 +134,8 @@
     1.4  
     1.5  (* state *)
     1.6  
     1.7 -val browser_info = Unsynchronized.ref empty_browser_info;
     1.8 -fun change_browser_info f =
     1.9 -  CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
    1.10 +val browser_info = Synchronized.var "browser_info" empty_browser_info;
    1.11 +fun change_browser_info f = Synchronized.change browser_info (map_browser_info f);
    1.12  
    1.13  fun init_theory_info name info =
    1.14    change_browser_info (fn (theories, tex_index, html_index, graph) =>
    1.15 @@ -217,7 +216,7 @@
    1.16  fun init build info info_path doc doc_graph document_output doc_variants doc_files
    1.17      (chapter, name) verbose thys =
    1.18    if not build andalso not info andalso doc = "" then
    1.19 -    (browser_info := empty_browser_info; session_info := NONE)
    1.20 +    (Synchronized.change browser_info (K empty_browser_info); session_info := NONE)
    1.21    else
    1.22      let
    1.23        val doc_output =
    1.24 @@ -239,7 +238,7 @@
    1.25        session_info :=
    1.26          SOME (make_session_info (name, chapter, info_path, info, doc,
    1.27            doc_graph, doc_output, doc_files, documents, verbose, readme));
    1.28 -      browser_info := init_browser_info (chapter, name) thys;
    1.29 +      Synchronized.change browser_info (K (init_browser_info (chapter, name) thys));
    1.30        add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
    1.31      end;
    1.32  
    1.33 @@ -290,7 +289,7 @@
    1.34    with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph,
    1.35      doc_output, doc_files, documents, verbose, readme, ...} =>
    1.36    let
    1.37 -    val {theories, tex_index, html_index, graph} = ! browser_info;
    1.38 +    val {theories, tex_index, html_index, graph} = Synchronized.value browser_info;
    1.39      val thys = Symtab.dest theories;
    1.40  
    1.41      val chapter_prefix = Path.append info_path (Path.basic chapter);
    1.42 @@ -360,7 +359,7 @@
    1.43  
    1.44      val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>);
    1.45    in
    1.46 -    browser_info := empty_browser_info;
    1.47 +    Synchronized.change browser_info (K empty_browser_info);
    1.48      session_info := NONE
    1.49    end);
    1.50