src/HOL/Tools/Mirabelle/mirabelle.scala

                       case List("mirabelle", action, "goal", goal_name, line, offset, cpu_ms) =>
                         action + " goal." + String.format("%-5s", goal_name) + " " + String.format("%5sms", cpu_ms) + " " +
                           args.theory_name + " " + line + ":" + offset + "  "
                       case _ => ""
                     }
-                  val body = Library.prefix_lines(prefix, lines) + "\n"
+                  val body = (if (lines == "") prefix else Library.prefix_lines(prefix, lines)) + "\n"
                   val log_file = output_dir + Path.basic("mirabelle.log")
                   File.append(log_file, body)
                 case _ =>
               }
             case _ =>

     Scala_Project.here, args =>
   {
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
     var options = Options.init(opts = build_options)
+    val mirabelle_dry_run = options.check_name("mirabelle_dry_run")
     val mirabelle_max_calls = options.check_name("mirabelle_max_calls")
     val mirabelle_randomize = options.check_name("mirabelle_randomize")
     val mirabelle_stride = options.check_name("mirabelle_stride")
     val mirabelle_timeout = options.check_name("mirabelle_timeout")
     val mirabelle_output_dir = options.check_name("mirabelle_output_dir")

     -r INT       """ + mirabelle_randomize.description + " (default " + mirabelle_randomize.default_value + """)
     -s INT       """ + mirabelle_stride.description + " (default " + mirabelle_stride.default_value + """)
     -t SECONDS   """ + mirabelle_timeout.description + " (default " + mirabelle_timeout.default_value + """)
     -v           verbose
     -x NAME      exclude session NAME and all descendants
+    -y           """ + mirabelle_dry_run.description + " (default " + mirabelle_dry_run.default_value + """)
 
   Apply the given ACTIONs at all theories and proof steps of the
   specified sessions.
 
   The absence of theory restrictions (option -T) means to check all

       "o:" -> (arg => options = options + arg),
       "r:" -> (arg => options = options + ("mirabelle_randomize=" + arg)),
       "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)),
       "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)),
       "v" -> (_ => verbose = true),
-      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)),
+      "y" -> (arg => options = options + ("mirabelle_dry_run=true")))
 
     val sessions = getopts(args)
     if (actions.isEmpty) getopts.usage()
 
     val progress = new Console_Progress(verbose = verbose)