--- 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'
--- 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] \<open> isabelle process_theories HOL-Library.Multiset\<close>}
\<^smallskip>
- Process a theory with prover output enabled:
- @{verbatim [display] \<open> isabelle process_theories -O HOL-Library.Multiset\<close>}
+ Process a theory with prover output enabled (using Unicode symbols):
+ @{verbatim [display] \<open> isabelle process_theories -U -O HOL-Library.Multiset\<close>}
\<^smallskip>
Process a theory with prover output enabled, including proof states:
- @{verbatim [display] \<open> isabelle process_theories -O -o show_states HOL-Library.Multiset\<close>}
+ @{verbatim [display] \<open> isabelle process_theories -U -O -o show_states HOL-Library.Multiset\<close>}
\<^smallskip>
Process a self-contained theory file from the Isabelle distribution, outside
--- 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)
}
}
--- 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 =
--- 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)