# HG changeset patch
# User wenzelm
# Date 1621850286 -7200
# Node ID 52e43a93d51f5043b82cba1088437002bc533678
# Parent  9f205ca4178a4dbc7c2a7541c40865667e24e200
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");

diff -r 9f205ca4178a -r 52e43a93d51f NEWS
--- a/NEWS	Sun May 23 23:15:04 2021 +0200
+++ b/NEWS	Mon May 24 11:58:06 2021 +0200
@@ -226,9 +226,10 @@
 
 *** System ***
 
-* Command-line tool "isabelle build" supports option -L FILE for syslog
-messages. Such messages can be produced in Isabelle/ML via formal
-Output.system_message or informal Output.physical_stderr.
+* System option "system_log" specifies an optional log file for internal
+messages produced by Output.system_message in Isabelle/ML; "-" refers to
+console progress of the build job. This works for "isabelle build" or
+any derivative of it.
 
 * Command-line tool "isabelle version" supports repository archives
 (without full .hg directory). More options.
diff -r 9f205ca4178a -r 52e43a93d51f etc/options
--- a/etc/options	Sun May 23 23:15:04 2021 +0200
+++ b/etc/options	Mon May 24 11:58:06 2021 +0200
@@ -133,6 +133,9 @@
 option profiling : string = ""
   -- "ML profiling (possible values: time, allocations)"
 
+option system_log : string = ""
+  -- "output for system messages (log file or \"-\" for console progress)"
+
 option system_heaps : bool = false
   -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
 
diff -r 9f205ca4178a -r 52e43a93d51f src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun May 23 23:15:04 2021 +0200
+++ b/src/Doc/System/Sessions.thy	Mon May 24 11:58:06 2021 +0200
@@ -276,6 +276,10 @@
     \<^ML>\<open>profile_time\<close> and \<^verbatim>\<open>allocations\<close> for \<^ML>\<open>profile_allocations\<close>.
     Results appear near the bottom of the session log file.
 
+    \<^item> @{system_option_def system_log} specifies an optional log file for
+    low-level messages produced by \<^ML>\<open>Output.system_message\<close> in
+    Isabelle/ML; ``\<^verbatim>\<open>-\<close>'' refers to console progress of the build job.
+
     \<^item> @{system_option_def "system_heaps"} determines the directories for
     session heap images: \<^path>\<open>$ISABELLE_HEAPS\<close> is the user directory and
     \<^path>\<open>$ISABELLE_HEAPS_SYSTEM\<close> the system directory (usually within the
@@ -326,7 +330,6 @@
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
-    -L FILE      append syslog messages to given FILE
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -R           refer to requirements of selected sessions
@@ -461,11 +464,6 @@
   the source files that contribute to a session.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-L\<close>~\<open>FILE\<close> appends syslog messages to the given file. Such messages
-  can be produced in Isabelle/ML via formal \<^ML>\<open>Output.system_message\<close> or
-  informal \<^ML>\<open>Output.physical_stderr\<close>.
-
-  \<^medskip>
   Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax (multiple
   uses allowed). The theory sources are checked for conflicts wrt.\ this
   hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers
diff -r 9f205ca4178a -r 52e43a93d51f src/Pure/General/logger.scala
--- a/src/Pure/General/logger.scala	Sun May 23 23:15:04 2021 +0200
+++ b/src/Pure/General/logger.scala	Mon May 24 11:58:06 2021 +0200
@@ -11,6 +11,9 @@
 {
   def make(log_file: Option[Path]): Logger =
     log_file match { case Some(file) => new File_Logger(file) case None => No_Logger }
+
+  def make(progress: Progress): Logger =
+    new Logger { def apply(msg: => String): Unit = progress.echo(msg) }
 }
 
 trait Logger
diff -r 9f205ca4178a -r 52e43a93d51f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun May 23 23:15:04 2021 +0200
+++ b/src/Pure/Tools/build.scala	Mon May 24 11:58:06 2021 +0200
@@ -169,7 +169,6 @@
     selection: Sessions.Selection = Sessions.Selection.empty,
     presentation: Presentation.Context = Presentation.Context.none,
     progress: Progress = new Progress,
-    log: Logger = No_Logger,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
@@ -293,6 +292,13 @@
     def sleep(): Unit =
       Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep() }
 
+    val log =
+      build_options.string("system_log") match {
+        case "" => No_Logger
+        case "-" => Logger.make(progress)
+        case log_file => Logger.make(Some(Path.explode(log_file)))
+      }
+
     val numa_nodes = new NUMA.Nodes(numa_shuffling)
 
     @tailrec def loop(
@@ -419,7 +425,7 @@
                   val numa_node = numa_nodes.next(used_node)
                   val job =
                     new Build_Job(progress, session_name, info, deps, store, do_store,
-                      verbose, numa_node, log, queue.command_timings(session_name))
+                      verbose, log, numa_node, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
                 else {
@@ -556,7 +562,6 @@
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
-    -L FILE      append syslog messages to given FILE
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -R           refer to requirements of selected sessions
@@ -582,7 +587,6 @@
 """ + Library.indent_lines(2,  Build_Log.Settings.show()) + "\n",
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
-      "L:" -> (arg => log = Logger.make(Some(Path.explode(arg)))),
       "N" -> (_ => numa_shuffling = true),
       "P:" -> (arg => presentation = Presentation.Context.make(arg)),
       "R" -> (_ => requirements = true),
@@ -629,7 +633,6 @@
             sessions = sessions),
           presentation = presentation,
           progress = progress,
-          log = log,
           check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
           build_heap = build_heap,
           clean_build = clean_build,
diff -r 9f205ca4178a -r 52e43a93d51f src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sun May 23 23:15:04 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Mon May 24 11:58:06 2021 +0200
@@ -203,8 +203,8 @@
   store: Sessions.Store,
   do_store: Boolean,
   verbose: Boolean,
+  log: Logger,
   val numa_node: Option[Int],
-  log: Logger,
   command_timings0: List[Properties.T])
 {
   val options: Options = NUMA.policy_options(info.options, numa_node)
@@ -391,7 +391,7 @@
         {
           case msg: Prover.Output =>
             val message = msg.message
-            if (msg.is_syslog) resources.log(msg.toString)
+            if (msg.is_system) resources.log(Protocol.message_text(message))
 
             if (msg.is_stdout) {
               stdout ++= Symbol.encode(XML.content(message))