src/Pure/Thy/thy_output.ML
changeset 23942 079e99db59d7
parent 23935 2a4e42ec9a54
child 24680 0d355aa59e67
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Jul 23 19:45:48 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Jul 23 19:45:49 2007 +0200
     1.3 @@ -63,14 +63,14 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val add_commands = Library.change global_commands o fold (add_item "command");
     1.8 -val add_options = Library.change global_options o fold (add_item "option");
     1.9 +fun add_commands xs = CRITICAL (fn () => change global_commands (fold (add_item "command") xs));
    1.10 +fun add_options xs = CRITICAL (fn () => change global_options (fold (add_item "option") xs));
    1.11  
    1.12  fun command src =
    1.13    let val ((name, _), pos) = Args.dest_src src in
    1.14      (case Symtab.lookup (! global_commands) name of
    1.15        NONE => error ("Unknown text antiquotation command: " ^ quote name ^ Position.str_of pos)
    1.16 -    | SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
    1.17 +    | SOME f => f src)
    1.18    end;
    1.19  
    1.20  fun option (name, s) f () =