maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;
1 (* Title: Pure/context_position.ML
4 Context position visibility flag.
7 signature CONTEXT_POSITION =
9 val is_visible: Proof.context -> bool
10 val set_visible: bool -> Proof.context -> Proof.context
11 val restore_visible: Proof.context -> Proof.context -> Proof.context
12 val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
13 val is_visible_proof: Context.generic -> bool
14 val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
15 val report_generic: Context.generic -> Position.T -> Markup.T -> unit
16 val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
17 val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
18 val report: Proof.context -> Position.T -> Markup.T -> unit
19 val reports: Proof.context -> Position.report list -> unit
22 structure Context_Position: CONTEXT_POSITION =
25 val visible = Config.bool (Config.declare "Context_Position.visible" (K (Config.Bool true)));
26 fun is_visible ctxt = Config.get ctxt visible;
27 val set_visible = Config.put visible;
28 val restore_visible = set_visible o is_visible;
30 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
32 fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt
33 | is_visible_proof _ = false;
35 fun if_visible_proof context f x = if is_visible_proof context then f x else ();
37 fun report_generic context pos markup =
38 if Config.get_generic context visible then
39 Output.report (Position.reported_text pos markup "")
42 fun reported_text ctxt pos markup txt =
43 if is_visible ctxt then Position.reported_text pos markup txt else "";
45 fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
46 fun report ctxt pos markup = report_text ctxt pos markup "";
48 fun reports ctxt reps = if is_visible ctxt then Position.reports reps else ();