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/Syntax/syntax_phases.ML
changeset 71675 55cb4271858b
parent 70784 799437173553
child 73163 624c2b98860a 
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -950,7 +950,7 @@
 fun check_typs ctxt raw_tys =
   let
     val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
-    val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else ();
+    val _ = if Context_Position.reports_enabled ctxt then Output.report sorting_report else ();
   in
     tys
     |> apply_typ_check ctxt
@@ -974,8 +974,8 @@
         else I) ps tys' [];
 
     val _ =
-      if Context_Position.is_visible ctxt then Output.report (sorting_report @ typing_report)
-      else ();
+      if Context_Position.reports_enabled 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;
isabelle