--- a/etc/options Fri Nov 04 11:38:01 2022 +0100
+++ b/etc/options Fri Nov 04 13:33:04 2022 +0100
@@ -178,6 +178,9 @@
option build_pide_reports : bool = true
-- "report PIDE markup (in batch build)"
+option pide_presentation : bool = false
+ -- "presentation of consolidated theories in PIDE"
+
section "Editor Session"
@@ -226,9 +229,6 @@
option editor_syslog_limit : int = 100
-- "maximum amount of buffered syslog messages"
-public option editor_presentation : bool = false
- -- "dynamic presentation while editing"
-
section "Headless Session"
--- a/src/Pure/PIDE/document.ML Fri Nov 04 11:38:01 2022 +0100
+++ b/src/Pure/PIDE/document.ML Fri Nov 04 13:33:04 2022 +0100
@@ -784,7 +784,7 @@
(Lazy.force (get_consolidated node);
Output.status [Markup.markup_only Markup.consolidated]);
val consolidation =
- if Options.bool options "editor_presentation" then
+ if Options.bool options "pide_presentation" then
let val context = presentation_context options the_command_span node_name node in
fn _ =>
let
--- a/src/Pure/Tools/dump.scala Fri Nov 04 11:38:01 2022 +0100
+++ b/src/Pure/Tools/dump.scala Fri Nov 04 13:33:04 2022 +0100
@@ -102,8 +102,8 @@
options0 +
"parallel_proofs=0" +
"completion_limit=0" +
- "editor_tracing_messages=0" +
- "editor_presentation"
+ "pide_presentation" +
+ "editor_tracing_messages=0"
aspects.foldLeft(options1) { case (opts, aspect) => aspect.options.foldLeft(opts)(_ + _) }
}