# HG changeset patch # User wenzelm # Date 1394045548 -3600 # Node ID 4bdae9403baff1206552410efdd9fea6a3901516 # Parent 710bc66f432c3aad1aa6858c255a68b7fff17d90 tuned; diff -r 710bc66f432c -r 4bdae9403baf src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Wed Mar 05 18:26:35 2014 +0100 +++ b/src/Pure/General/name_space.ML Wed Mar 05 19:52:28 2014 +0100 @@ -205,8 +205,7 @@ (* completion *) fun completion context space (xname, pos) = - if Context_Position.is_visible_generic context andalso Position.is_reported pos - then + if Context_Position.is_reported_generic context pos then let val x = Name.clean xname; val Name_Space {kind = k, internals, ...} = space; @@ -453,7 +452,7 @@ SOME x => let val reports = - if Context_Position.is_visible_generic context andalso Position.is_reported pos + if Context_Position.is_reported_generic context pos then [(pos, markup space name)] else []; in ((name, reports), x) end | NONE => diff -r 710bc66f432c -r 4bdae9403baf src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Mar 05 18:26:35 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Mar 05 19:52:28 2014 +0100 @@ -391,7 +391,7 @@ (Completion.reported_text (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos)))); val reports = - if Context_Position.is_visible ctxt andalso Position.is_reported pos + if Context_Position.is_reported ctxt pos then [(pos, Name_Space.markup class_space name)] else []; in (name, reports) end; @@ -459,7 +459,7 @@ if Lexicon.is_tid c then let val reports = - if Context_Position.is_visible ctxt andalso Position.is_reported pos + if Context_Position.is_reported ctxt pos then [(pos, Markup.tfree)] else []; in (TFree (c, default_sort ctxt (c, ~1)), reports) end else diff -r 710bc66f432c -r 4bdae9403baf src/Pure/context_position.ML --- a/src/Pure/context_position.ML Wed Mar 05 18:26:35 2014 +0100 +++ b/src/Pure/context_position.ML Wed Mar 05 19:52:28 2014 +0100 @@ -15,6 +15,8 @@ val set_visible_global: bool -> theory -> theory val restore_visible: Proof.context -> Proof.context -> Proof.context val restore_visible_global: theory -> theory -> theory + val is_reported_generic: Context.generic -> Position.T -> bool + val is_reported: Proof.context -> Position.T -> bool val report_generic: Context.generic -> Position.T -> Markup.T -> unit val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit @@ -47,13 +49,16 @@ val restore_visible = set_visible o is_visible; val restore_visible_global = set_visible_global o is_visible_global; +fun is_reported_generic context pos = is_visible_generic context andalso Position.is_reported pos; +fun is_reported ctxt pos = is_visible ctxt andalso Position.is_reported pos; + fun report_generic context pos markup = - if is_visible_generic context then + if is_reported_generic context pos then Output.report (Position.reported_text pos markup "") else (); fun reported_text ctxt pos markup txt = - if is_visible ctxt then Position.reported_text pos markup txt else ""; + if is_reported ctxt pos then Position.reported_text pos markup txt else ""; fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt); fun report ctxt pos markup = report_text ctxt pos markup "";