# HG changeset patch
# User wenzelm
# Date 1667578481 -3600
# Node ID 9e5098cbf81fccd9e33a4e107b5e27294fc2a0da
# Parent  0901321dd6b2b71c59b86fd5b2bc08c4bee9f467
more antiquotations;

diff -r 0901321dd6b2 -r 9e5098cbf81f src/Pure/PIDE/command.ML
--- 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 =>
diff -r 0901321dd6b2 -r 9e5098cbf81f src/Pure/PIDE/document.ML
--- 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