etc/options
changeset 71675 55cb4271858b
parent 71651 e26cfcbe20f7
child 71845 b8d7b623e274
--- a/etc/options	Fri Apr 03 13:51:56 2020 +0200
+++ b/etc/options	Fri Apr 03 17:35:10 2020 +0200
@@ -123,9 +123,6 @@
 option system_heaps : bool = false
   -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
 
-option pide_build : bool = false
-  -- "build session heaps via PIDE"
-
 
 section "ML System"
 
@@ -151,6 +148,15 @@
   -- "ML process command prefix (process policy)"
 
 
+section "PIDE Build"
+
+option pide_build : bool = false
+  -- "build session heaps via PIDE"
+
+option pide_reports : bool = true
+  -- "report PIDE markup"
+
+
 section "Editor Session"
 
 public option editor_load_delay : real = 0.5