# HG changeset patch
# User wenzelm
# Date 1585768244 -7200
# Node ID e26cfcbe20f78046fd61498a6c4cb9faf755740a
# Parent  95ab607398bdbc726a0e660bc43a1f1559996e7c
prefer system option: easier to make it default;

diff -r 95ab607398bd -r e26cfcbe20f7 etc/options
--- a/etc/options	Wed Apr 01 20:55:48 2020 +0200
+++ b/etc/options	Wed Apr 01 21:10:44 2020 +0200
@@ -123,6 +123,9 @@
 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"
 
diff -r 95ab607398bd -r e26cfcbe20f7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 01 20:55:48 2020 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 01 21:10:44 2020 +0200
@@ -194,7 +194,6 @@
     store: Sessions.Store,
     do_store: Boolean,
     verbose: Boolean,
-    pide: Boolean,
     val numa_node: Option[Int],
     command_timings: List[Properties.T])
   {
@@ -252,7 +251,7 @@
           }
           else Nil
 
-        if (pide) {
+        if (options.bool("pide_build")) {
           val resources = new Resources(sessions_structure, deps(parent))
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
@@ -419,7 +418,6 @@
     soft_build: Boolean = false,
     verbose: Boolean = false,
     export_files: Boolean = false,
-    pide: Boolean = false,
     requirements: Boolean = false,
     all_sessions: Boolean = false,
     base_sessions: List[String] = Nil,
@@ -654,7 +652,7 @@
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
-                    new Job(progress, name, info, deps, store, do_store, verbose, pide = pide,
+                    new Job(progress, name, info, deps, store, do_store, verbose,
                       numa_node, queue.command_timings(name))
                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
                 }
@@ -742,7 +740,6 @@
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
     var numa_shuffling = false
-    var pide = false
     var requirements = false
     var soft_build = false
     var exclude_session_groups: List[String] = Nil
@@ -768,7 +765,6 @@
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
-    -P           build via PIDE protocol
     -R           operate on requirements of selected sessions
     -S           soft build: only observe changes of sources, not heap images
     -X NAME      exclude sessions from group NAME and all descendants
@@ -793,7 +789,6 @@
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "N" -> (_ => numa_shuffling = true),
-      "P" -> (_ => pide = true),
       "R" -> (_ => requirements = true),
       "S" -> (_ => soft_build = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
@@ -843,7 +838,6 @@
           soft_build = soft_build,
           verbose = verbose,
           export_files = export_files,
-          pide = pide,
           requirements = requirements,
           all_sessions = all_sessions,
           base_sessions = base_sessions,