# HG changeset patch
# User wenzelm
# Date 1672240388 -3600
# Node ID 3e8340fcaa161b4882fd1be8fc9b2b007c1e0a8e
# Parent  5ffe32b613ae50ad8e83e1f5ee88dab27c218ae2
tuned signature;

diff -r 5ffe32b613ae -r 3e8340fcaa16 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Dec 28 16:02:12 2022 +0100
+++ b/src/Pure/Isar/method.ML	Wed Dec 28 16:13:08 2022 +0100
@@ -667,7 +667,7 @@
       (keyword_positions text);
 
 fun report text_range =
-  if Context_Position.pide_reports ()
+  if Context_Position.reports_enabled0 ()
   then Position.reports (reports_of text_range) else ();
 
 end;
diff -r 5ffe32b613ae -r 3e8340fcaa16 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Dec 28 16:02:12 2022 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Wed Dec 28 16:13:08 2022 +0100
@@ -53,7 +53,7 @@
     val reports_enabled =
       (case Context.get_generic_context () of
         SOME context => Context_Position.reports_enabled_generic context
-      | NONE => Context_Position.pide_reports ());
+      | NONE => Context_Position.reports_enabled0 ());
     fun is_reported pos = reports_enabled andalso Position.is_reported pos;
 
 
diff -r 5ffe32b613ae -r 3e8340fcaa16 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Dec 28 16:02:12 2022 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Dec 28 16:13:08 2022 +0100
@@ -333,7 +333,7 @@
 fun read_file_node file_node master_dir pos delimited src_path =
   let
     val _ =
-      if Context_Position.pide_reports ()
+      if Context_Position.reports_enabled0 ()
       then Position.report pos (Markup.language_path delimited) else ();
 
     fun read_local () =
diff -r 5ffe32b613ae -r 3e8340fcaa16 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Dec 28 16:02:12 2022 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Dec 28 16:13:08 2022 +0100
@@ -118,7 +118,7 @@
         in message name pos_props [XML.blob ss] end;
 
     fun report_message ss =
-      if Context_Position.pide_reports ()
+      if Context_Position.reports_enabled0 ()
       then standard_message [] Markup.reportN ss else ();
 
     val serial_props = Markup.serial_properties o serial;
diff -r 5ffe32b613ae -r 3e8340fcaa16 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Wed Dec 28 16:02:12 2022 +0100
+++ b/src/Pure/context_position.ML	Wed Dec 28 16:13:08 2022 +0100
@@ -17,7 +17,7 @@
   val restore_visible_generic: Context.generic -> Context.generic -> Context.generic
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val restore_visible_global: theory -> theory -> theory
-  val pide_reports: unit -> bool
+  val reports_enabled0: unit -> bool
   val reports_enabled_generic: Context.generic -> bool
   val reports_enabled: Proof.context -> bool
   val reports_enabled_global: theory -> bool
@@ -64,9 +64,8 @@
 
 (* PIDE reports *)
 
-fun pide_reports () = Options.default_bool "pide_reports";
-
-fun reports_enabled_generic context = pide_reports () andalso is_visible_generic context;
+fun reports_enabled0 () = Options.default_bool "pide_reports";
+fun reports_enabled_generic context = reports_enabled0 () andalso is_visible_generic context;
 val reports_enabled = reports_enabled_generic o Context.Proof;
 val reports_enabled_global = reports_enabled_generic o Context.Theory;