# HG changeset patch # User wenzelm # Date 1754908498 -7200 # Node ID 71ffc2c2234823f0dfea8cb2a7349998de67678d # Parent 1143c65b58292825709408d347ecd23821250bfb explicit "isabelle process_theories -U" as in "isabelle build_log"; diff -r 1143c65b5829 -r 71ffc2c22348 NEWS --- a/NEWS Mon Aug 11 12:13:48 2025 +0200 +++ b/NEWS Mon Aug 11 12:34:58 2025 +0200 @@ -342,9 +342,9 @@ Examples: - isabelle process_theories -O HOL-Library.Multiset - - isabelle process_theories -O -o show_states HOL-Library.Multiset + isabelle process_theories -U -O HOL-Library.Multiset + + isabelle process_theories -U -O -o show_states HOL-Library.Multiset isabelle process_theories -f '~~/src/HOL/Examples/Seq.thy' diff -r 1143c65b5829 -r 71ffc2c22348 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Mon Aug 11 12:13:48 2025 +0200 +++ b/src/Doc/System/Sessions.thy Mon Aug 11 12:34:58 2025 +0200 @@ -1259,12 +1259,12 @@ @{verbatim [display] \ isabelle process_theories HOL-Library.Multiset\} \<^smallskip> - Process a theory with prover output enabled: - @{verbatim [display] \ isabelle process_theories -O HOL-Library.Multiset\} + Process a theory with prover output enabled (using Unicode symbols): + @{verbatim [display] \ isabelle process_theories -U -O HOL-Library.Multiset\} \<^smallskip> Process a theory with prover output enabled, including proof states: - @{verbatim [display] \ isabelle process_theories -O -o show_states HOL-Library.Multiset\} + @{verbatim [display] \ isabelle process_theories -U -O -o show_states HOL-Library.Multiset\} \<^smallskip> Process a self-contained theory file from the Isabelle distribution, outside diff -r 1143c65b5829 -r 71ffc2c22348 src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Mon Aug 11 12:13:48 2025 +0200 +++ b/src/Pure/General/pretty.scala Mon Aug 11 12:34:58 2025 +0200 @@ -218,6 +218,7 @@ val default_breakgain: Double = default_margin / 20 def formatted(input: XML.Body, + recode: String => String = identity, margin: Double = default_margin, breakgain: Double = default_breakgain, metric: Metric = Codepoint.Metric @@ -240,7 +241,8 @@ List(make_block(make_tree(body), markup = (markup, None), open_block = true)) } case XML.Text(text) => - Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s)))) + Library.separate(FBreak, + split_lines(text).map { s0 => val s = recode(s0); Str(s, metric(s)) }) } def format(trees: List[Tree], before: Double, after: Double, text: Text): Text = @@ -277,11 +279,14 @@ } def string_of(input: XML.Body, + recode: String => String = identity, margin: Double = default_margin, breakgain: Double = default_breakgain, metric: Metric = Codepoint.Metric, pure: Boolean = false ): String = { - output_content(pure, formatted(input, margin = margin, breakgain = breakgain, metric = metric)) + val out = + formatted(input, recode = recode, margin = margin, breakgain = breakgain, metric = metric) + output_content(pure, out) } } diff -r 1143c65b5829 -r 71ffc2c22348 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Mon Aug 11 12:13:48 2025 +0200 +++ b/src/Pure/PIDE/protocol.scala Mon Aug 11 12:34:58 2025 +0200 @@ -188,14 +188,15 @@ def message_text(elem: XML.Elem, heading: Boolean = false, pos: Position.T = Position.none, + recode: String => String = identity, margin: Double = Pretty.default_margin, breakgain: Double = Pretty.default_breakgain, metric: Pretty.Metric = Codepoint.Metric ): String = { - val text1 = if (heading) "\n" + message_heading(elem, pos) + ":\n" else "" + val text1 = if (heading) "\n" + recode(message_heading(elem, pos)) + ":\n" else "" val body = - Pretty.string_of(List(elem), margin = margin, breakgain = breakgain, + Pretty.string_of(List(elem), recode = recode, margin = margin, breakgain = breakgain, metric = metric, pure = true) val text2 = diff -r 1143c65b5829 -r 71ffc2c22348 src/Pure/Tools/process_theories.scala --- a/src/Pure/Tools/process_theories.scala Mon Aug 11 12:13:48 2025 +0200 +++ b/src/Pure/Tools/process_theories.scala Mon Aug 11 12:34:58 2025 +0200 @@ -31,6 +31,7 @@ margin: Double = Pretty.default_margin, breakgain: Double = Pretty.default_breakgain, metric: Pretty.Metric = Symbol.Metric, + unicode_symbols: Boolean = false, progress: Progress = new Progress ): Build.Results = { Isabelle_System.with_tmp_dir("private") { private_dir => @@ -99,6 +100,7 @@ def session_setup(setup_session_name: String, session: Session): Unit = { if (output_messages && setup_session_name == session_name) { + def recode(s: String): String = Symbol.output(unicode_symbols, s) session.all_messages += Session.Consumer[Prover.Message]("process_theories") { case output: Prover.Output if Protocol.is_exported(output.message) || Protocol.is_state(output.message) => @@ -108,7 +110,7 @@ val pos = Position.Line_File(line, file) if (Build.print_log_check(pos, output.message, message_head, message_body)) { progress.echo(Protocol.message_text(output.message, heading = true, pos = pos, - margin = margin, breakgain = breakgain, metric = metric)) + recode = recode, margin = margin, breakgain = breakgain, metric = metric)) } case _ => } @@ -134,6 +136,7 @@ val message_head = new mutable.ListBuffer[Regex] val message_body = new mutable.ListBuffer[Regex] var output_messages = false + var unicode_symbols = false val dirs = new mutable.ListBuffer[Path] val files = new mutable.ListBuffer[Path] var logic = Isabelle_System.getenv("ISABELLE_LOGIC") @@ -150,6 +153,7 @@ -H REGEX filter messages by matching against head -M REGEX filter messages by matching against body -O output messages + -U output Unicode symbols -d DIR include session directory -f FILE include addition session files -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) @@ -163,6 +167,7 @@ "H:" -> (arg => message_head += arg.r), "M:" -> (arg => message_body += arg.r), "O" -> (_ => output_messages = true), + "U" -> (_ => unicode_symbols = true), "d:" -> (arg => dirs += Path.explode(arg)), "f:" -> (arg => files += Path.explode(arg)), "l:" -> (arg => logic = arg), @@ -178,7 +183,8 @@ progress.interrupt_handler { process_theories(options, logic, theories, files = files.toList, dirs = dirs.toList, output_messages = output_messages, message_head = message_head.toList, - message_body = message_body.toList, margin = margin, progress = progress) + message_body = message_body.toList, margin = margin, unicode_symbols = unicode_symbols, + progress = progress) } sys.exit(results.rc)