# HG changeset patch # User wenzelm # Date 1185212746 -7200 # Node ID e543359fe8b60c61c53e7e23b48f71909ed3e6bb # Parent 977d14aeb4d5367a1a0ffc782fae21ed70009064 marked some CRITICAL sections; diff -r 977d14aeb4d5 -r e543359fe8b6 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Mon Jul 23 19:45:45 2007 +0200 +++ b/src/Pure/General/output.ML Mon Jul 23 19:45:46 2007 +0200 @@ -221,7 +221,7 @@ fun time_accumulator name = let val ti = time_init name in - change time_finish_hooks (cons (fn () => time_finish ti)); + CRITICAL (fn () => change time_finish_hooks (cons (fn () => time_finish ti))); time_add ti end; diff -r 977d14aeb4d5 -r e543359fe8b6 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Mon Jul 23 19:45:45 2007 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Mon Jul 23 19:45:46 2007 +0200 @@ -108,17 +108,17 @@ Symtab.table); val global_markups = ref ([]: (string * ThyOutput.markup) list); -fun change_lexicons f = +fun change_lexicons f = CRITICAL (fn () => let val lexs = f (! global_lexicons) in (case (op inter_string) (pairself Scan.dest_lexicon lexs) of [] => global_lexicons := lexs | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads)) - end; + end); -fun make_markups () = global_markups := - Symtab.fold (fn (name, (_, SOME m)) => cons (name, m) | _ => I) (! global_parsers) []; - -fun change_parsers f = (Library.change global_parsers f; make_markups ()); +fun change_parsers f = CRITICAL (fn () => + (change global_parsers f; + global_markups := + Symtab.fold (fn (name, (_, SOME m)) => cons (name, m) | _ => I) (! global_parsers) [])); in @@ -149,10 +149,10 @@ else warning ("Redefined outer syntax command " ^ quote name); Symtab.update (name, (((comment, kind), (int_only, parse)), markup)) tab); -fun add_parsers parsers = +fun add_parsers parsers = CRITICAL (fn () => (change_parsers (fold add_parser parsers); change_lexicons (apsnd (Scan.extend_lexicon - (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers)))); + (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers))))); end; diff -r 977d14aeb4d5 -r e543359fe8b6 src/Pure/Thy/ml_context.ML --- a/src/Pure/Thy/ml_context.ML Mon Jul 23 19:45:45 2007 +0200 +++ b/src/Pure/Thy/ml_context.ML Mon Jul 23 19:45:46 2007 +0200 @@ -68,10 +68,11 @@ (y, SOME context') => (y, context') | (_, NONE) => error "Lost context in ML"); -fun save f x = setmp (get_context ()) f x; +fun save f x = CRITICAL (fn () => setmp (get_context ()) f x); -fun change_theory f = - set_context (SOME (Context.map_theory f (the_generic_context ()))); +fun change_theory f = CRITICAL (fn () => + set_context (SOME (Context.map_theory f (the_generic_context ())))); + (** ML antiquotations **) @@ -80,8 +81,8 @@ val global_lexicon = ref Scan.empty_lexicon; -fun add_keywords keywords = - change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords)); +fun add_keywords keywords = CRITICAL (fn () => + change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords))); (* maintain commands *) @@ -92,10 +93,11 @@ local -fun add_item kind name scan = change global_parsers (fn tab => - (if not (Symtab.defined tab name) then () - else warning ("Redefined ML antiquotation: " ^ quote name); - Symtab.update (name, scan >> kind) tab)); +fun add_item kind name scan = CRITICAL (fn () => + change global_parsers (fn tab => + (if not (Symtab.defined tab name) then () + else warning ("Redefined ML antiquotation: " ^ quote name); + Symtab.update (name, scan >> kind) tab))); in @@ -115,8 +117,7 @@ let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup (! global_parsers) name of NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) - | SOME scan => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) - (fn () => syntax scan src) ()) + | SOME scan => syntax scan src) end; @@ -137,7 +138,7 @@ val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;"; val isabelle_struct0 = isabelle_struct ""; -fun eval_antiquotes txt = +fun eval_antiquotes txt = CRITICAL (fn () => let val ants = Antiquote.scan_antiquotes (txt, Position.line 1); @@ -158,7 +159,7 @@ val (decls, body) = fold_map expand ants ML_Syntax.reserved |> #1 |> split_list |> pairself implode; - in (isabelle_struct decls, body) end; + in (isabelle_struct decls, body) end); fun eval name verbose txt = Output.ML_errors (use_text name Output.ml_output verbose) txt; diff -r 977d14aeb4d5 -r e543359fe8b6 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon Jul 23 19:45:45 2007 +0200 +++ b/src/Pure/Thy/thy_info.ML Mon Jul 23 19:45:46 2007 +0200 @@ -57,7 +57,7 @@ local val hooks = ref ([]: (action -> string -> unit) list); in - fun add_hook f = hooks := f :: ! hooks; + fun add_hook f = CRITICAL (fn () => change hooks (cons f)); fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks); end; @@ -122,7 +122,7 @@ val database = ref (Graph.empty: thy Graph.T); in fun get_thys () = ! database; - val change_thys = Library.change database; + fun change_thys f = CRITICAL (fn () => Library.change database f); end; @@ -150,7 +150,8 @@ SOME thy => thy | NONE => error (loader_msg "nothing known about theory" [name])); -fun change_thy name f = (get_thy name; change_thys (Graph.map_node name f)); +fun change_thy name f = CRITICAL (fn () => + (get_thy name; change_thys (Graph.map_node name f))); (* access deps *) @@ -229,8 +230,9 @@ fun outdate_thy name = if is_finished name orelse is_outdated name then () - else (change_deps name (Option.map (fn {outdated = _, master, parents, files} => - make_deps true master parents files)); perform Outdate name); + else CRITICAL (fn () => + (change_deps name (Option.map (fn {outdated = _, master, parents, files} => + make_deps true master parents files)); perform Outdate name)); fun check_unfinished name = if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE) @@ -317,9 +319,10 @@ if null missing_files then () else warning (loader_msg "unresolved dependencies of theory" [name] ^ " on file(s): " ^ commas_quote missing_files); - change_deps name - (Option.map (fn {parents, ...} => make_deps false (SOME master) parents files)); - perform Update name + CRITICAL (fn () => + (change_deps name + (Option.map (fn {parents, ...} => make_deps false (SOME master) parents files)); + perform Update name)) end; @@ -420,8 +423,7 @@ else let val succs = thy_graph Graph.all_succs [name] in priority (loader_msg "removing" succs); - List.app (perform Remove) succs; - change_thys (Graph.del_nodes succs) + CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs))) end; @@ -496,7 +498,7 @@ in if not (null nonfinished) then err "non-finished parent theories" nonfinished else if not (null variants) then err "different versions of parent theories" variants - else (change_thys register; perform Update name) + else CRITICAL (fn () => (change_thys register; perform Update name)) end; val _ = register_theory ProtoPure.thy;