marked some CRITICAL sections;
authorwenzelm
Mon Jul 23 20:47:56 2007 +0200 (2007-07-23)
changeset 239442ea068548a83
parent 23943 1b5f77bc146a
child 23945 622641164de8
marked some CRITICAL sections;
src/Pure/Thy/present.ML
src/Pure/Thy/thy_load.ML
src/Pure/context.ML
     1.1 --- a/src/Pure/Thy/present.ML	Mon Jul 23 20:47:55 2007 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Mon Jul 23 20:47:56 2007 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4  (* state *)
     1.5  
     1.6  val browser_info = ref empty_browser_info;
     1.7 -fun change_browser_info f = browser_info := map_browser_info f (! browser_info);
     1.8 +fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
     1.9  
    1.10  val suppress_tex_source = ref false;
    1.11  fun no_document f x = Library.setmp suppress_tex_source true f x;
    1.12 @@ -290,7 +290,7 @@
    1.13  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    1.14  
    1.15  fun init build info doc doc_graph doc_versions path name doc_prefix2
    1.16 -    (remote_path, first_time) verbose thys =
    1.17 +    (remote_path, first_time) verbose thys = CRITICAL (fn () =>
    1.18    if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
    1.19      (browser_info := empty_browser_info; session_info := NONE)
    1.20    else
    1.21 @@ -327,7 +327,7 @@
    1.22        info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
    1.23        browser_info := init_browser_info remote_path path thys;
    1.24        add_html_index index_text
    1.25 -    end;
    1.26 +    end);
    1.27  
    1.28  
    1.29  (* isatool wrappers *)
    1.30 @@ -371,8 +371,9 @@
    1.31    write_tex (Buffer.add Latex.tex_trailer tex_index) doc_indexN path;
    1.32  
    1.33  
    1.34 -fun finish () = with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
    1.35 -    documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
    1.36 +fun finish () = CRITICAL (fn () =>
    1.37 +    with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
    1.38 +      documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
    1.39    let
    1.40      val {theories, files, tex_index, html_index, graph} = ! browser_info;
    1.41      val thys = Symtab.dest theories;
    1.42 @@ -429,7 +430,7 @@
    1.43  
    1.44      browser_info := empty_browser_info;
    1.45      session_info := NONE
    1.46 -  end);
    1.47 +  end));
    1.48  
    1.49  
    1.50  (* theory elements *)
    1.51 @@ -503,7 +504,7 @@
    1.52  
    1.53  
    1.54  val hooks = ref ([]: (string -> (string * thm list) list -> unit) list);
    1.55 -fun add_hook f = hooks := (f :: ! hooks);
    1.56 +fun add_hook f = CRITICAL (fn () => change hooks (cons f));
    1.57  
    1.58  fun results k xs =
    1.59   (List.app (fn f => (try (fn () => f k xs) (); ())) (! hooks);
     2.1 --- a/src/Pure/Thy/thy_load.ML	Mon Jul 23 20:47:55 2007 +0200
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Jul 23 20:47:56 2007 +0200
     2.3 @@ -46,16 +46,25 @@
     2.4  
     2.5  (* maintain load path *)
     2.6  
     2.7 -val load_path = ref [Path.current];
     2.8 +local val load_path = ref [Path.current] in
     2.9  
    2.10  fun show_path () = map Path.implode (! load_path);
    2.11 -fun del_path s = change load_path (remove (op =) (Path.explode s));
    2.12 -fun add_path s = (del_path s; change load_path (cons (Path.explode s)));
    2.13 -fun path_add s = (del_path s; change load_path (fn path => path @ [Path.explode s]));
    2.14 +
    2.15 +fun del_path s = CRITICAL (fn () => change load_path (remove (op =) (Path.explode s)));
    2.16 +fun add_path s = CRITICAL (fn () => (del_path s; change load_path (cons (Path.explode s))));
    2.17 +fun path_add s =
    2.18 +  CRITICAL (fn () => (del_path s; change load_path (fn path => path @ [Path.explode s])));
    2.19  fun reset_path () = load_path := [Path.current];
    2.20 -fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
    2.21 +
    2.22 +fun with_paths ss f x =
    2.23 +  CRITICAL (fn () => Library.setmp load_path (! load_path @ map Path.explode ss) f x);
    2.24  fun with_path s f x = with_paths [s] f x;
    2.25  
    2.26 +fun search_path dir path =
    2.27 +  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
    2.28 +
    2.29 +end;
    2.30 +
    2.31  
    2.32  (* file formats *)
    2.33  
    2.34 @@ -66,10 +75,7 @@
    2.35  
    2.36  (* check files *)
    2.37  
    2.38 -fun search_path dir path =
    2.39 -  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
    2.40 -
    2.41 -fun check_ext exts dir src_path =
    2.42 +fun check_ext exts paths dir src_path =
    2.43    let
    2.44      val path = Path.expand src_path;
    2.45      val _ = Path.is_current path andalso error "Bad file specification";
    2.46 @@ -78,16 +84,19 @@
    2.47        let val ext_path = Path.expand (Path.ext ext rel_path)
    2.48        in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
    2.49      fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
    2.50 -  in get_first try_prfx (search_path dir path) end;
    2.51 +  in get_first try_prfx paths end;
    2.52  
    2.53 -val check_file = check_ext [];
    2.54 -val check_ml = check_ext ml_exts;
    2.55 +fun check_file dir path = check_ext [] (search_path dir path) dir path;
    2.56 +fun check_ml dir path = check_ext ml_exts (search_path dir path) dir path;
    2.57  
    2.58  fun check_thy dir name ml =
    2.59 -  let val thy_file = thy_path name in
    2.60 -    (case check_file dir thy_file of
    2.61 +  let
    2.62 +    val thy_file = thy_path name;
    2.63 +    val paths = search_path dir thy_file;
    2.64 +  in
    2.65 +    (case check_ext [] paths dir thy_file of
    2.66        NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
    2.67 -        " in " ^ commas_quote (map Path.implode (search_path dir thy_file)))
    2.68 +        " in " ^ commas_quote (map Path.implode paths))
    2.69      | SOME thy_id => (thy_id, if ml then check_file dir (ml_path name) else NONE))
    2.70    end;
    2.71  
     3.1 --- a/src/Pure/context.ML	Mon Jul 23 20:47:55 2007 +0200
     3.2 +++ b/src/Pure/context.ML	Mon Jul 23 20:47:56 2007 +0200
     3.3 @@ -126,7 +126,7 @@
     3.4    let
     3.5      val k = serial ();
     3.6      val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
     3.7 -    val _ = change kinds (Datatab.update (k, kind));
     3.8 +    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
     3.9    in k end;
    3.10  
    3.11  val copy_data = Datatab.map' invoke_copy;
    3.12 @@ -449,7 +449,7 @@
    3.13  fun declare init =
    3.14    let
    3.15      val k = serial ();
    3.16 -    val _ = change kinds (Datatab.update (k, init));
    3.17 +    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
    3.18    in k end;
    3.19  
    3.20  fun get k dest prf =
    3.21 @@ -494,8 +494,8 @@
    3.22  local
    3.23    val setup_fn = ref (I: theory -> theory);
    3.24  in
    3.25 -  fun add_setup f = setup_fn := (! setup_fn #> f);
    3.26 -  fun setup () = let val f = ! setup_fn in setup_fn := I; f end;
    3.27 +  fun add_setup f = CRITICAL (fn () => setup_fn := (! setup_fn #> f));
    3.28 +  fun setup () = CRITICAL (fn () => let val f = ! setup_fn in setup_fn := I; f end);
    3.29  end;
    3.30  
    3.31  end;