etc/options
changeset 77674 488a48453d74
parent 77606 b0a4f8c29446
child 77675 9e5f8f6e58a0
--- a/etc/options	Thu Mar 16 11:44:07 2023 +0100
+++ b/etc/options	Thu Mar 16 13:18:25 2023 +0100
@@ -50,6 +50,9 @@
 
 section "Prover Output"
 
+option pide_reports : bool = true for content
+  -- "enable reports of PIDE markup"
+
 option show_types : bool = false for content
   -- "show type constraints when printing terms"
 option show_sorts : bool = false for content
@@ -171,12 +174,6 @@
 
 section "Build Process"
 
-option pide_reports : bool = true for content
-  -- "report PIDE markup (in ML)"
-
-option build_pide_reports : bool = true for content
-  -- "report PIDE markup (in batch build)"
-
 option build_hostname : string = ""
   -- "alternative hostname for build process (default $ISABELLE_HOSTNAME)"