# HG changeset patch
# User wenzelm
# Date 1585928110 -7200
# Node ID 55cb4271858b798502ff6298bd6e13e9b5472949
# Parent  48ff625687f53c03bd399c2d1970ce8c172351a1
less redundant markup reports;

diff -r 48ff625687f5 -r 55cb4271858b etc/options
--- a/etc/options	Fri Apr 03 13:51:56 2020 +0200
+++ b/etc/options	Fri Apr 03 17:35:10 2020 +0200
@@ -123,9 +123,6 @@
 option system_heaps : bool = false
   -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
 
-option pide_build : bool = false
-  -- "build session heaps via PIDE"
-
 
 section "ML System"
 
@@ -151,6 +148,15 @@
   -- "ML process command prefix (process policy)"
 
 
+section "PIDE Build"
+
+option pide_build : bool = false
+  -- "build session heaps via PIDE"
+
+option pide_reports : bool = true
+  -- "report PIDE markup"
+
+
 section "Editor Session"
 
 public option editor_load_delay : real = 0.5
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/Isar/method.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -659,7 +659,9 @@
     maps (fn p => map (pair p) (Markup.keyword3 :: Completion.suppress_abbrevs ""))
       (keyword_positions text);
 
-val report = Position.reports o reports_of;
+fun report text_range =
+  if Context_Position.pide_reports ()
+  then Position.reports (reports_of text_range) else ();
 
 end;
 
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -792,7 +792,7 @@
 fun check_tfree ctxt v =
   let
     val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v];
-    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 a end;
 
 end;
@@ -1103,7 +1103,7 @@
   let
     val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt;
     val mx' = Mixfix.reset_pos mx;
-    val _ = add_syntax [(x, T, if Context_Position.is_visible ctxt then mx else mx')] ctxt';
+    val _ = add_syntax [(x, T, if Context_Position.reports_enabled ctxt then mx else mx')] ctxt';
   in mx' end;
 
 fun prep_var prep_typ internal (b, raw_T, mx) ctxt =
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/Isar/token.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -760,7 +760,7 @@
     val old_reports = maps reports_of_value src;
     val args1 = map init_assignable (args_of_src src);
     fun reported_text () =
-      if Context_Position.is_visible_generic context then
+      if Context_Position.reports_enabled_generic context then
         let val new_reports = maps (reports_of_value o closure) args1 in
           if old_reports <> new_reports then
             map (fn (p, m) => Position.reported_text p m "") new_reports
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -50,11 +50,11 @@
 
 fun report_parse_tree redirect depth name_space parse_tree =
   let
-    val is_visible =
+    val reports_enabled =
       (case Context.get_generic_context () of
-        SOME context => Context_Position.is_visible_generic context
-      | NONE => true);
-    fun is_reported pos = is_visible andalso Position.is_reported pos;
+        SOME context => Context_Position.reports_enabled_generic context
+      | NONE => Context_Position.pide_reports ());
+    fun is_reported pos = reports_enabled andalso Position.is_reported pos;
 
 
     (* syntax reports *)
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -58,7 +58,9 @@
 
 fun read_file_node file_node master_dir pos src_path =
   let
-    val _ = Position.report pos Markup.language_path;
+    val _ =
+      if Context_Position.pide_reports ()
+      then Position.report pos Markup.language_path else ();
     val _ =
       (case try Url.explode file_node of
         NONE => ()
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/ROOT.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -96,6 +96,8 @@
 ML_file "General/change_table.ML";
 ML_file "General/graph.ML";
 
+ML_file "System/options.ML";
+
 
 subsection "Fundamental structures";
 
@@ -103,7 +105,6 @@
 ML_file "term.ML";
 ML_file "context.ML";
 ML_file "context_position.ML";
-ML_file "System/options.ML";
 ML_file "config.ML";
 ML_file "soft_type_system.ML";
 
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/Syntax/syntax_phases.ML
--- 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;
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -152,13 +152,15 @@
             | _ => props);
         in message name props' (XML.blob ss) end;
 
+    fun report_message ss =
+      if Context_Position.pide_reports ()
+      then standard_message [] Markup.reportN ss else ();
+
     val serial_props = Markup.serial_properties o serial;
 
     val message_context =
-      Unsynchronized.setmp Private_Output.status_fn
-        (standard_message [] Markup.statusN) #>
-      Unsynchronized.setmp Private_Output.report_fn
-        (standard_message [] Markup.reportN) #>
+      Unsynchronized.setmp Private_Output.status_fn (standard_message [] Markup.statusN) #>
+      Unsynchronized.setmp Private_Output.report_fn report_message #>
       Unsynchronized.setmp Private_Output.result_fn
         (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #>
       Unsynchronized.setmp Private_Output.writeln_fn
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/Tools/build.scala	Fri Apr 03 17:35:10 2020 +0200
@@ -162,12 +162,13 @@
     val numa_node: Option[Int],
     command_timings: List[Properties.T])
   {
-    private val options = NUMA.policy_options(info.options, numa_node)
+    private def build_options(options: Options): Options = options + "pide_reports=false"
+    private val job_options = build_options(NUMA.policy_options(info.options, numa_node))
 
     private val sessions_structure = deps.sessions_structure
 
     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
-    graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display)
+    graphview.Graph_File.write(job_options, graph_file, deps(session_name).session_graph_display)
 
     private val export_tmp_dir = Isabelle_System.tmp_dir("export")
     private val export_consumer =
@@ -177,6 +178,8 @@
       Future.thread("build") {
         val parent = info.parent.getOrElse("")
         val base = deps(parent)
+        val encode_theory_options: XML.Encode.T[Options] =
+          (options => Options.encode(build_options(options)))
         val args_yxml =
           YXML.string_of_body(
             {
@@ -184,7 +187,7 @@
               pair(list(pair(string, int)), pair(list(properties), pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
-                pair(list(pair(Options.encode, list(pair(string, properties)))),
+                pair(list(pair(encode_theory_options, list(pair(string, properties)))),
                 pair(list(pair(string, properties)),
                 pair(list(pair(string, string)),
                 pair(list(string), pair(list(pair(string, string)),
@@ -202,7 +205,7 @@
         val env =
           Isabelle_System.settings() +
             ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) +
-            ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
+            ("ISABELLE_ML_DEBUGGER" -> job_options.bool("ML_debugger").toString)
 
         val is_pure = Sessions.is_pure(session_name)
 
@@ -216,9 +219,9 @@
           }
           else Nil
 
-        if (options.bool("pide_build")) {
+        if (job_options.bool("pide_build")) {
           val resources = new Resources(sessions_structure, deps(parent))
-          val session = new Session(options, resources)
+          val session = new Session(job_options, resources)
 
           val stdout = new StringBuilder(1000)
           val messages = new mutable.ListBuffer[String]
@@ -288,7 +291,7 @@
           val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
           val process =
-            Isabelle_Process(session, options, sessions_structure, store,
+            Isabelle_Process(session, job_options, sessions_structure, store,
               logic = parent, raw_ml_system = is_pure,
               use_prelude = use_prelude, eval_main = eval_main,
               cwd = info.dir.file, env = env)
@@ -326,7 +329,7 @@
           val eval_main = Command_Line.ML_tool(eval_build :: eval_store)
 
           val process =
-            ML_Process(options, deps.sessions_structure, store,
+            ML_Process(job_options, deps.sessions_structure, store,
               logic = parent, raw_ml_system = is_pure,
               use_prelude = use_prelude, eval_main = eval_main,
               cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
@@ -348,7 +351,7 @@
                 case _ =>
               },
             progress_limit =
-              options.int("process_output_limit") match {
+              job_options.int("process_output_limit") match {
                 case 0 => None
                 case m => Some(m * 1000000L)
               },
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/Tools/rail.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -191,7 +191,7 @@
   ANTIQUOTE of (bool * Antiquote.antiq) * Position.range;
 
 fun reports_of_tree ctxt =
-  if Context_Position.is_visible ctxt then
+  if Context_Position.reports_enabled ctxt then
     let
       fun reports r =
         if r = Position.no_range then []
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/context_position.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -17,6 +17,10 @@
   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_enabled_generic: Context.generic -> bool
+  val reports_enabled: Proof.context -> bool
+  val reports_enabled_global: theory -> bool
   val is_reported_generic: Context.generic -> Position.T -> bool
   val is_reported: Proof.context -> Position.T -> bool
   val is_reported_global: theory -> Position.T -> bool
@@ -62,7 +66,14 @@
 
 (* PIDE reports *)
 
-fun is_reported_generic context pos = is_visible_generic context andalso Position.is_reported pos;
+fun pide_reports () = Options.default_bool "pide_reports";
+
+fun reports_enabled_generic context = pide_reports () andalso is_visible_generic context;
+val reports_enabled = reports_enabled_generic o Context.Proof;
+val reports_enabled_global = reports_enabled_generic o Context.Theory;
+
+fun is_reported_generic context pos =
+  reports_enabled_generic context andalso Position.is_reported pos;
 
 val is_reported = is_reported_generic o Context.Proof;
 val is_reported_global = is_reported_generic o Context.Theory;
@@ -78,8 +89,11 @@
 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 "";
 
-fun reports_text ctxt reps = if is_visible ctxt then Position.reports_text reps else ();
-fun reports_generic context reps = if is_visible_generic context then Position.reports reps else ();
+fun reports_text ctxt reps =
+  if reports_enabled ctxt then Position.reports_text reps else ();
+
+fun reports_generic context reps =
+  if reports_enabled_generic context then Position.reports reps else ();
 
 val reports = reports_generic o Context.Proof;
 val reports_global = reports_generic o Context.Theory;
diff -r 48ff625687f5 -r 55cb4271858b src/Pure/skip_proof.ML
--- a/src/Pure/skip_proof.ML	Fri Apr 03 13:51:56 2020 +0200
+++ b/src/Pure/skip_proof.ML	Fri Apr 03 17:35:10 2020 +0200
@@ -18,7 +18,7 @@
 (* report *)
 
 fun report ctxt =
-  if Context_Position.is_visible ctxt then
+  if Context_Position.reports_enabled ctxt then
     Output.report [Markup.markup (Markup.bad ()) "Skipped proof"]
   else ();