--- a/src/Pure/PIDE/command.ML Fri Nov 04 17:11:48 2022 +0100
+++ b/src/Pure/PIDE/command.ML Fri Nov 04 17:14:41 2022 +0100
@@ -403,7 +403,7 @@
end;
fun parallel_print (Print {pri, ...}) =
- pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print");
+ pri <= 0 orelse (Future.enabled () andalso Options.default_bool \<^system_option>\<open>parallel_print\<close>);
fun print_function name f =
Synchronized.change print_functions (fn funs =>
@@ -497,7 +497,8 @@
val _ =
Command.print_function "print_state"
(fn {keywords, command_name, ...} =>
- if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name
+ if Options.default_bool \<^system_option>\<open>editor_output_state\<close>
+ andalso Keyword.is_printed keywords command_name
then
SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
print_fn = fn _ => fn st =>
--- a/src/Pure/PIDE/document.ML Fri Nov 04 17:11:48 2022 +0100
+++ b/src/Pure/PIDE/document.ML Fri Nov 04 17:14:41 2022 +0100
@@ -530,7 +530,7 @@
let
val {version_id, execution_id, delay_request, parallel_prints} = execution;
- val delay = seconds (Options.default_real "editor_execution_delay");
+ val delay = seconds (Options.default_real \<^system_option>\<open>editor_execution_delay\<close>);
val _ = Future.cancel delay_request;
val delay_request' = Event_Timer.future {physical = true} (Time.now () + delay);
@@ -779,7 +779,7 @@
(Lazy.force (get_consolidated node);
Output.status [Markup.markup_only Markup.consolidated]);
val consolidation =
- if Options.bool options "pide_presentation" then
+ if Options.bool options \<^system_option>\<open>pide_presentation\<close> then
let val context = presentation_context options the_command_span node_name node in
fn _ =>
let