src/Pure/Tools/build.scala

     val info: Sessions.Info,
     deps: Sessions.Deps,
     store: Sessions.Store,
     do_store: Boolean,
     verbose: Boolean,
-    pide: Boolean,
     val numa_node: Option[Int],
     command_timings: List[Properties.T])
   {
     private val options = NUMA.policy_options(info.options, numa_node)
 

             List("ML_Heap.save_child " +
               ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name))))
           }
           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)
           session.init_protocol_handler(handler)
 

     fresh_build: Boolean = false,
     no_build: Boolean = false,
     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,
     exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,

                   store.clean_output(name)
                   using(store.open_database(name, output = true))(store.init_session_info(_, name))
 
                   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)
                 }
                 else {
                   progress.echo(name + " CANCELLED")

     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
     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
     var all_sessions = false
     var build_heap = false

 
   Options are:
     -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
     -a           select all sessions
     -b           build heap images

 
 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
       "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)),
       "a" -> (_ => all_sessions = true),
       "b" -> (_ => build_heap = true),

           fresh_build = fresh_build,
           no_build = no_build,
           soft_build = soft_build,
           verbose = verbose,
           export_files = export_files,
-          pide = pide,
           requirements = requirements,
           all_sessions = all_sessions,
           base_sessions = base_sessions,
           exclude_session_groups = exclude_session_groups,
           exclude_sessions = exclude_sessions,