Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/proof_context.ML
changeset 55923 4bdae9403baf
parent 55922 710bc66f432c
child 55948 bb21b380f65d 
--- 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
isabelle