src/Pure/Thy/ml_context.ML

 fun pass_context context f x =
   (case pass (SOME context) f x of
     (y, SOME context') => (y, context')
   | (_, NONE) => error "Lost context in ML");
 
-fun save f x = setmp (get_context ()) f x;
-
-fun change_theory f =
-  set_context (SOME (Context.map_theory f (the_generic_context ())));
+fun save f x = CRITICAL (fn () => setmp (get_context ()) f x);
+
+fun change_theory f = CRITICAL (fn () =>
+  set_context (SOME (Context.map_theory f (the_generic_context ()))));
+
 
 
 (** ML antiquotations **)
 
 (* maintain keywords *)
 
 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 *)
 
 datatype antiq = Inline of string | ProjValue of string * string * string;
 val global_parsers = ref (Symtab.empty:
   (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table);
 
 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
 
 val inline_antiq = add_item Inline;
 val proj_value_antiq = add_item ProjValue;

 
 fun command src =
   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;
 
 
 (* outer syntax *)
 

 local
 
 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);
 
     fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names)
       | expand (Antiquote.Antiq x) names =

               in ((binding, value), names') end);
 
     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;
 
 in