# HG changeset patch # User wenzelm # Date 1395841312 -3600 # Node ID 85911b8a6868c1111294b3aa436cc61d3efa8fb0 # Parent 9bc33476f6aca12f794a67eaa58b07dacd5b6da3 prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature; diff -r 9bc33476f6ac -r 85911b8a6868 src/Doc/antiquote_setup.ML --- 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}); diff -r 9bc33476f6ac -r 85911b8a6868 src/HOL/Tools/SMT/smt_config.ML --- 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 = diff -r 9bc33476f6ac -r 85911b8a6868 src/HOL/Tools/SMT2/smt2_config.ML --- 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 = diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/Isar/generic_target.ML --- 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 diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/Isar/outer_syntax.ML --- 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 ()); diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/Isar/proof_context.ML --- 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; diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/Isar/typedecl.ML --- 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 diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/ML/ml_context.ML --- 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 => ()); diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/PIDE/resources.ML --- 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; diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/Syntax/syntax_phases.ML --- 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; diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/config.ML --- 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; diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/context_position.ML --- 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; diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/skip_proof.ML --- 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 *) diff -r 9bc33476f6ac -r 85911b8a6868 src/Pure/unify.ML --- 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;