prefer Context_Position where a context is available;
prefer explicit Context_Position.is_visible -- avoid redundant message composition;
tuned signature;

--- a/src/Doc/antiquote_setup.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -192,17 +192,17 @@
 
 fun no_check _ _ = true;
 
-fun check_command (name, pos) =
+fun check_command ctxt (name, pos) =
   is_some (Keyword.command_keyword name) andalso
     let
       val markup =
         Outer_Syntax.scan Position.none name
         |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
         |> map (snd o fst);
-      val _ = List.app (Position.report pos) markup;
+      val _ = Context_Position.reports ctxt (map (pair pos) markup);
     in true end;
 
-fun check_tool (name, pos) =
+fun check_tool ctxt (name, pos) =
   let
     fun tool dir =
       let val path = Path.append dir (Path.basic name)
@@ -210,7 +210,7 @@
   in
     (case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of
       NONE => false
-    | SOME path => (Position.report pos (Markup.path (Path.implode path)); true))
+    | SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true))
   end;
 
 val arg = enclose "{" "}" o clean_string;
@@ -255,7 +255,7 @@
 val _ =
   Theory.setup
    (entity_antiqs no_check "" @{binding syntax} #>
-    entity_antiqs (K check_command) "isacommand" @{binding command} #>
+    entity_antiqs check_command "isacommand" @{binding command} #>
     entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #>
     entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #>
     entity_antiqs (can o Method.check_name) "" @{binding method} #>
@@ -269,7 +269,7 @@
     entity_antiqs no_check "isatt" @{binding system_option} #>
     entity_antiqs no_check "" @{binding inference} #>
     entity_antiqs no_check "isatt" @{binding executable} #>
-    entity_antiqs (K check_tool) "isatool" @{binding tool} #>
+    entity_antiqs check_tool "isatool" @{binding tool} #>
     entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
     entity_antiqs (K (is_action o #1)) "isatt" @{binding action});
 

--- a/src/HOL/Tools/SMT/smt_config.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -101,8 +101,9 @@
   filter (is_available ctxt) (all_solvers_of ctxt)
 
 fun warn_solver (Context.Proof ctxt) name =
-      Context_Position.if_visible ctxt
+      if Context_Position.is_visible ctxt then
         warning ("The SMT solver " ^ quote name ^ " is not installed.")
+      else ()
   | warn_solver _ _ = ();
 
 fun select_solver name context =

--- a/src/HOL/Tools/SMT2/smt2_config.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_config.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -99,8 +99,9 @@
   filter (is_available ctxt) (all_solvers_of ctxt)
 
 fun warn_solver (Context.Proof ctxt) name =
-      Context_Position.if_visible ctxt
+      if Context_Position.is_visible ctxt then
         warning ("The SMT solver " ^ quote name ^ " is not installed.")
+      else ()
   | warn_solver _ _ = ();
 
 fun select_solver name context =

--- a/src/Pure/Isar/generic_target.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/Isar/generic_target.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -57,12 +57,13 @@
 fun check_mixfix ctxt (b, extra_tfrees) mx =
   if null extra_tfrees then mx
   else
-    (Context_Position.if_visible ctxt warning
-      ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
-        commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
-        (if mx = NoSyn then ""
-         else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)));
-      NoSyn);
+   (if Context_Position.is_visible ctxt then
+      warning
+        ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
+          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
+          (if mx = NoSyn then ""
+           else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
+    else (); NoSyn);
 
 fun check_mixfix_global (b, no_params) mx =
   if no_params orelse mx = NoSyn then mx

--- a/src/Pure/Isar/outer_syntax.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -143,7 +143,8 @@
 
 fun add_command (name, kind) cmd = CRITICAL (fn () =>
   let
-    val thy = ML_Context.the_global_context ();
+    val context = ML_Context.the_generic_context ();
+    val thy = Context.theory_of context;
     val Command {pos, ...} = cmd;
     val _ =
       (case try (Thy_Header.the_keyword thy) name of
@@ -155,7 +156,7 @@
           if Context.theory_name thy = Context.PureN
           then Keyword.define (name, SOME kind)
           else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
-    val _ = Position.report pos (command_markup true (name, cmd));
+    val _ = Context_Position.report_generic context pos (command_markup true (name, cmd));
 
     fun redefining () =
       "Redefining outer syntax command " ^ quote name ^ Position.here (Position.thread_data ());

--- a/src/Pure/Isar/proof_context.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -718,7 +718,7 @@
 fun check_tfree ctxt v =
   let
     val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v];
-    val _ = Context_Position.if_visible ctxt Output.report sorting_report;
+    val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else ();
   in a end;
 
 end;

--- a/src/Pure/Isar/typedecl.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/Isar/typedecl.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -102,11 +102,12 @@
     val rhs = Proof_Context.read_typ_syntax (ctxt |> Proof_Context.set_defsort []) raw_rhs;
     val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
     val _ =
-      if null ignored then ()
-      else Context_Position.if_visible ctxt warning
-        ("Ignoring sort constraints in type variables(s): " ^
-          commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
-          "\nin type abbreviation " ^ Binding.print b);
+      if not (null ignored) andalso Context_Position.is_visible ctxt then
+        warning
+          ("Ignoring sort constraints in type variables(s): " ^
+            commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
+            "\nin type abbreviation " ^ Binding.print b)
+      else ();
   in rhs end;
 
 in

--- a/src/Pure/ML/ml_context.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -149,9 +149,8 @@
     val _ =
       (case Option.map Context.proof_of env_ctxt of
         SOME ctxt =>
-          if Config.get ctxt source_trace then
-            Context_Position.if_visible ctxt
-              tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
+          if Config.get ctxt source_trace andalso Context_Position.is_visible ctxt
+          then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
           else ()
       | NONE => ());
 

--- a/src/Pure/PIDE/resources.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -211,9 +211,10 @@
           val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
         in
           if strict then error msg
-          else
-            Context_Position.if_visible ctxt Output.report
+          else if Context_Position.is_visible ctxt then
+            Output.report
               (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
+          else ()
         end;
   in path end;
 

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -417,8 +417,9 @@
             report_result ctxt pos []
               [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
           else if checked_len = 1 then
-            (if not (null ambig_msgs) andalso ambiguity_warning then
-              Context_Position.if_visible ctxt warning
+            (if not (null ambig_msgs) andalso ambiguity_warning andalso
+                Context_Position.is_visible ctxt then
+              warning
                 (cat_lines (ambig_msgs @
                   ["Fortunately, only one parse tree is well-formed and type-correct,\n\
                    \but you may still want to disambiguate your grammar or your input."]))
@@ -927,7 +928,7 @@
 fun check_typs ctxt raw_tys =
   let
     val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
-    val _ = Context_Position.if_visible ctxt Output.report sorting_report;
+    val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else ();
   in
     tys
     |> apply_typ_check ctxt
@@ -951,7 +952,9 @@
         else I) ps tys' []
       |> implode;
 
-    val _ = Context_Position.if_visible ctxt Output.report (sorting_report ^ typing_report);
+    val _ =
+      if Context_Position.is_visible ctxt then Output.report (sorting_report ^ typing_report)
+      else ();
   in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
 
 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;

--- a/src/Pure/config.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/config.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -131,8 +131,9 @@
               print_value (get_value (Context.Theory (Context.theory_of context'))) <>
                 print_value (get_value context')
             then
-              (Context_Position.if_visible ctxt warning
-                ("Ignoring local change of global option " ^ quote name); context)
+             (if Context_Position.is_visible ctxt then
+                warning ("Ignoring local change of global option " ^ quote name)
+              else (); context)
             else context'
           end
       | map_value f context = update_value f context;

--- a/src/Pure/context_position.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/context_position.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -9,8 +9,6 @@
   val is_visible_generic: Context.generic -> bool
   val is_visible: Proof.context -> bool
   val is_visible_global: theory -> bool
-  val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
-  val if_visible_global: theory -> ('a -> unit) -> 'a -> unit
   val set_visible: bool -> Proof.context -> Proof.context
   val set_visible_global: bool -> theory -> theory
   val restore_visible: Proof.context -> Proof.context -> Proof.context
@@ -40,9 +38,6 @@
 val is_visible = is_visible_generic o Context.Proof;
 val is_visible_global = is_visible_generic o Context.Theory;
 
-fun if_visible ctxt f x = if is_visible ctxt then f x else ();
-fun if_visible_global thy f x = if is_visible_global thy then f x else ();
-
 val set_visible = Context.proof_map o Data.put o SOME;
 val set_visible_global = Context.theory_map o Data.put o SOME;
 

--- a/src/Pure/skip_proof.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/skip_proof.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -18,8 +18,9 @@
 (* report *)
 
 fun report ctxt =
-  Context_Position.if_visible ctxt Output.report
-    (Markup.markup Markup.bad "Skipped proof");
+  if Context_Position.is_visible ctxt then
+    Output.report (Markup.markup Markup.bad "Skipped proof")
+  else ();
 
 
 (* oracle setup *)

--- a/src/Pure/unify.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/Pure/unify.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -607,8 +607,8 @@
             [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq)
           | dp :: frigid' =>
               if tdepth > search_bound then
-                (Context_Position.if_visible_global thy warning "Unification bound exceeded";
-                 Seq.pull reseq)
+                (if Context_Position.is_visible_global thy
+                 then warning "Unification bound exceeded" else (); Seq.pull reseq)
               else
                (if tdepth > trace_bound then
                   print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
@@ -617,7 +617,8 @@
                     (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq))))
         end
         handle CANTUNIFY =>
-         (if tdepth > trace_bound then Context_Position.if_visible_global thy tracing "Failure node"
+         (if tdepth > trace_bound andalso Context_Position.is_visible_global thy
+          then tracing "Failure node"
           else (); Seq.pull reseq));
     val dps = map (fn (t, u) => ([], t, u)) tus;
   in add_unify 1 ((env, dps), Seq.empty) end;