# HG changeset patch
# User wenzelm
# Date 1662658346 -7200
# Node ID 13ae8dff47b6a687c810f8b02c2a463dba49e773
# Parent  bec8677d0e5bc3c8d6fd2c051a3d88aff5c9e66f
updated documentation;

diff -r bec8677d0e5b -r 13ae8dff47b6 NEWS
--- a/NEWS	Thu Sep 08 17:42:48 2022 +0200
+++ b/NEWS	Thu Sep 08 19:32:26 2022 +0200
@@ -280,6 +280,10 @@
 Occasional INCOMPATIBILITY, see also the official Scala documentation
 https://docs.scala-lang.org/scala3/guides/migration/compatibility-intro.html
 
+* Command-line tool "isabelle log" has been refined to support multiple
+sessions, and to match messages against regular expressions (using Java
+Pattern syntax).
+
 * Command-line tool "isabelle scala_project" supports Gradle as
 alternative to Maven: either option -G or -M needs to be specified
 explicitly. This increases the chances that the Java/Scala IDE project
diff -r bec8677d0e5b -r 13ae8dff47b6 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Thu Sep 08 17:42:48 2022 +0200
+++ b/src/Doc/System/Sessions.thy	Thu Sep 08 19:32:26 2022 +0200
@@ -554,24 +554,31 @@
   database of the given session. Its command-line usage is:
 
   @{verbatim [display]
-\<open>Usage: isabelle log [OPTIONS] SESSION
+\<open>Usage: isabelle log [OPTIONS] [SESSIONS ...]
 
   Options are:
+    -H REGEX     filter messages by matching against head
+    -M REGEX     filter messages by matching against body
     -T NAME      restrict to given theories (multiple options possible)
     -U           output Unicode symbols
     -m MARGIN    margin for pretty printing (default: 76.0)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           print all messages, including information etc.
 
-  Print messages from the build database of the given session, without any
-  checks against current sources: results from a failed build can be
-  printed as well.\<close>}
+  Print messages from the build database of the given sessions, without any
+  checks against current sources nor session structure: results from old
+  sessions or failed builds can be printed as well.
 
-  The specified session database is taken as is, independently of the current
-  session structure and theories sources. The order of messages follows the
-  source positions of source files; thus the erratic evaluation of parallel
-  processing rarely matters. There is \<^emph>\<open>no\<close> implicit build process involved,
-  so it is possible to retrieve error messages from a failed session as well.
+  Multiple options -H and -M are conjunctive: all given patterns need to
+  match. Patterns match any substring, but ^ or $ may be used to match the
+  start or end explicitly.\<close>}
+
+  The specified session databases are taken as is, with formal checking
+  against current sources: There is \<^emph>\<open>no\<close> implicit build process involved, so
+  it is possible to retrieve error messages from a failed session as well. The
+  order of messages follows the source positions of source files; thus the
+  result is mostly deterministic, independent of the somewhat erratic
+  evaluation of parallel processing.
 
   \<^medskip> Option \<^verbatim>\<open>-o\<close> allows to change system options, as in @{tool build}
   (\secref{sec:tool-build}). This may affect the storage space for the build
@@ -588,6 +595,16 @@
 
   \<^medskip> Option \<^verbatim>\<open>-v\<close> prints all messages from the session database that are
   normally inlined into the source text, including information messages etc.
+
+  \<^medskip> Options \<^verbatim>\<open>-H\<close> and \<^verbatim>\<open>-M\<close> filter messages according to their header or body
+  content, respectively. The header follows a very basic format that makes it
+  easy to match message kinds (e.g. \<^verbatim>\<open>Warning\<close> or \<^verbatim>\<open>Error\<close>) and file names
+  (e.g. \<^verbatim>\<open>src/HOL/Nat.thy\<close>). The body is usually pretty-printed, but for
+  matching it is treated like one long line: blocks are ignored and breaks are
+  turned into plain spaces (according to their formal width).
+
+  The syntax for patters follows regular expressions of the Java
+  platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
 \<close>
 
 subsubsection \<open>Examples\<close>
@@ -596,6 +613,15 @@
   Print messages from theory \<^verbatim>\<open>HOL.Nat\<close> of session \<^verbatim>\<open>HOL\<close>, using Unicode
   rendering of Isabelle symbols and a margin of 100 characters:
   @{verbatim [display] \<open>  isabelle log -T HOL.Nat -U -m 100 HOL\<close>}
+
+  Print warnings about ambiguous input (inner syntax) of session
+  \<^verbatim>\<open>HOL-Library\<close>, which is built beforehand:
+  @{verbatim [display] \<open>  isabelle build HOL-Library
+  isabelle log -H "Warning" -M "Ambiguous input" HOL-Library\<close>}
+
+  Print all errors from all sessions, e.g. from a partial build of
+  Isabelle/AFP:
+  @{verbatim [display] \<open>  isabelle log -H "Error" $(isabelle sessions -a -d AFP/thys)\<close>}
 \<close>