clarified modules;
authorwenzelm
Tue Sep 18 11:05:14 2018 +0200 (21 months ago)
changeset 69012c91d14ab065f
parent 69011 8745ca1e7e93
child 69013 bb4e4c253ebe
clarified modules;
src/Pure/PIDE/headless.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/dump.scala
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/headless.scala	Tue Sep 18 11:05:14 2018 +0200
     1.3 @@ -0,0 +1,514 @@
     1.4 +/*  Title:      Pure/PIDE/headless.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Headless PIDE session and resources from file-system.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.io.{File => JFile}
    1.14 +
    1.15 +import scala.annotation.tailrec
    1.16 +
    1.17 +
    1.18 +object Headless
    1.19 +{
    1.20 +  /** session **/
    1.21 +
    1.22 +  def start_session(
    1.23 +    options: Options,
    1.24 +    session_name: String,
    1.25 +    session_dirs: List[Path] = Nil,
    1.26 +    include_sessions: List[String] = Nil,
    1.27 +    session_base: Option[Sessions.Base] = None,
    1.28 +    print_mode: List[String] = Nil,
    1.29 +    progress: Progress = No_Progress,
    1.30 +    log: Logger = No_Logger): Session =
    1.31 +  {
    1.32 +    val base =
    1.33 +      session_base getOrElse
    1.34 +        Sessions.base_info(options, session_name, include_sessions = include_sessions,
    1.35 +          progress = progress, dirs = session_dirs).check_base
    1.36 +    val resources = new Resources(base, log = log)
    1.37 +    val session = new Session(session_name, options, resources)
    1.38 +
    1.39 +    val session_error = Future.promise[String]
    1.40 +    var session_phase: Session.Consumer[Session.Phase] = null
    1.41 +    session_phase =
    1.42 +      Session.Consumer(getClass.getName) {
    1.43 +        case Session.Ready =>
    1.44 +          session.phase_changed -= session_phase
    1.45 +          session_error.fulfill("")
    1.46 +        case Session.Terminated(result) if !result.ok =>
    1.47 +          session.phase_changed -= session_phase
    1.48 +          session_error.fulfill("Session start failed: return code " + result.rc)
    1.49 +        case _ =>
    1.50 +      }
    1.51 +    session.phase_changed += session_phase
    1.52 +
    1.53 +    progress.echo("Starting session " + session_name + " ...")
    1.54 +    Isabelle_Process.start(session, options,
    1.55 +      logic = session_name, dirs = session_dirs, modes = print_mode)
    1.56 +
    1.57 +    session_error.join match {
    1.58 +      case "" => session
    1.59 +      case msg => session.stop(); error(msg)
    1.60 +    }
    1.61 +  }
    1.62 +
    1.63 +  private def stable_snapshot(
    1.64 +    state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
    1.65 +  {
    1.66 +    val snapshot = state.snapshot(name)
    1.67 +    assert(version.id == snapshot.version.id)
    1.68 +    snapshot
    1.69 +  }
    1.70 +
    1.71 +  class Theories_Result private[Headless](
    1.72 +    val state: Document.State,
    1.73 +    val version: Document.Version,
    1.74 +    val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
    1.75 +    val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
    1.76 +  {
    1.77 +    def snapshot(name: Document.Node.Name): Document.Snapshot =
    1.78 +      stable_snapshot(state, version, name)
    1.79 +
    1.80 +    def ok: Boolean =
    1.81 +      (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
    1.82 +  }
    1.83 +
    1.84 +  val default_check_delay = Time.seconds(0.5)
    1.85 +  val default_nodes_status_delay = Time.seconds(-1.0)
    1.86 +  val default_commit_cleanup_delay = Time.seconds(60.0)
    1.87 +  val default_watchdog_timeout = Time.seconds(600.0)
    1.88 +
    1.89 +
    1.90 +  class Session private[Headless](
    1.91 +    session_name: String,
    1.92 +    session_options: Options,
    1.93 +    override val resources: Resources) extends isabelle.Session(session_options, resources)
    1.94 +  {
    1.95 +    session =>
    1.96 +
    1.97 +
    1.98 +    /* temporary directory */
    1.99 +
   1.100 +    val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
   1.101 +    val tmp_dir_name: String = File.path(tmp_dir).implode
   1.102 +
   1.103 +    def master_directory(master_dir: String): String =
   1.104 +      proper_string(master_dir) getOrElse tmp_dir_name
   1.105 +
   1.106 +    override def toString: String = session_name
   1.107 +
   1.108 +    override def stop(): Process_Result =
   1.109 +    {
   1.110 +      try { super.stop() }
   1.111 +      finally { Isabelle_System.rm_tree(tmp_dir) }
   1.112 +    }
   1.113 +
   1.114 +
   1.115 +    /* theories */
   1.116 +
   1.117 +    private sealed case class Use_Theories_State(
   1.118 +      last_update: Time = Time.now(),
   1.119 +      nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
   1.120 +      already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
   1.121 +      result: Promise[Theories_Result] = Future.promise[Theories_Result])
   1.122 +    {
   1.123 +      def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
   1.124 +        copy(last_update = Time.now(), nodes_status = new_nodes_status)
   1.125 +
   1.126 +      def watchdog(watchdog_timeout: Time): Boolean =
   1.127 +        watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
   1.128 +
   1.129 +      def cancel_result { result.cancel }
   1.130 +      def finished_result: Boolean = result.is_finished
   1.131 +      def await_result { result.join_result }
   1.132 +      def join_result: Theories_Result = result.join
   1.133 +      def check_result(
   1.134 +          state: Document.State,
   1.135 +          version: Document.Version,
   1.136 +          dep_theories: List[Document.Node.Name],
   1.137 +          beyond_limit: Boolean,
   1.138 +          watchdog_timeout: Time,
   1.139 +          commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
   1.140 +        : Use_Theories_State =
   1.141 +      {
   1.142 +        val st1 =
   1.143 +          if (commit.isDefined) {
   1.144 +            val already_committed1 =
   1.145 +              (already_committed /: dep_theories)({ case (committed, name) =>
   1.146 +                def parents_committed: Boolean =
   1.147 +                  version.nodes(name).header.imports.forall({ case (parent, _) =>
   1.148 +                    Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
   1.149 +                  })
   1.150 +                if (!committed.isDefinedAt(name) && parents_committed &&
   1.151 +                    state.node_consolidated(version, name))
   1.152 +                {
   1.153 +                  val snapshot = stable_snapshot(state, version, name)
   1.154 +                  val status = Document_Status.Node_Status.make(state, version, name)
   1.155 +                  commit.get.apply(snapshot, status)
   1.156 +                  committed + (name -> status)
   1.157 +                }
   1.158 +                else committed
   1.159 +              })
   1.160 +            copy(already_committed = already_committed1)
   1.161 +          }
   1.162 +          else this
   1.163 +
   1.164 +        if (beyond_limit || watchdog(watchdog_timeout) ||
   1.165 +          dep_theories.forall(name =>
   1.166 +            already_committed.isDefinedAt(name) ||
   1.167 +            state.node_consolidated(version, name) ||
   1.168 +            nodes_status.quasi_consolidated(name)))
   1.169 +        {
   1.170 +          val nodes =
   1.171 +            for (name <- dep_theories)
   1.172 +            yield { (name -> Document_Status.Node_Status.make(state, version, name)) }
   1.173 +          val nodes_committed =
   1.174 +            for {
   1.175 +              name <- dep_theories
   1.176 +              status <- already_committed.get(name)
   1.177 +            } yield (name -> status)
   1.178 +
   1.179 +          try { result.fulfill(new Theories_Result(state, version, nodes, nodes_committed)) }
   1.180 +          catch { case _: IllegalStateException => }
   1.181 +        }
   1.182 +
   1.183 +        st1
   1.184 +      }
   1.185 +    }
   1.186 +
   1.187 +    def use_theories(
   1.188 +      theories: List[String],
   1.189 +      qualifier: String = Sessions.DRAFT,
   1.190 +      master_dir: String = "",
   1.191 +      check_delay: Time = default_check_delay,
   1.192 +      check_limit: Int = 0,
   1.193 +      watchdog_timeout: Time = default_watchdog_timeout,
   1.194 +      nodes_status_delay: Time = default_nodes_status_delay,
   1.195 +      id: UUID = UUID(),
   1.196 +      // commit: must not block, must not fail
   1.197 +      commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
   1.198 +      commit_cleanup_delay: Time = default_commit_cleanup_delay,
   1.199 +      progress: Progress = No_Progress): Theories_Result =
   1.200 +    {
   1.201 +      val dep_theories =
   1.202 +      {
   1.203 +        val import_names =
   1.204 +          theories.map(thy =>
   1.205 +            resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none)
   1.206 +        resources.dependencies(import_names, progress = progress).check_errors.theories
   1.207 +      }
   1.208 +
   1.209 +      val use_theories_state = Synchronized(Use_Theories_State())
   1.210 +
   1.211 +      def check_result(beyond_limit: Boolean = false)
   1.212 +      {
   1.213 +        val state = session.current_state()
   1.214 +        state.stable_tip_version match {
   1.215 +          case Some(version) =>
   1.216 +            use_theories_state.change(
   1.217 +              _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit))
   1.218 +          case None =>
   1.219 +        }
   1.220 +      }
   1.221 +
   1.222 +      val check_progress =
   1.223 +      {
   1.224 +        var check_count = 0
   1.225 +        Event_Timer.request(Time.now(), repeat = Some(check_delay))
   1.226 +          {
   1.227 +            if (progress.stopped) use_theories_state.value.cancel_result
   1.228 +            else {
   1.229 +              check_count += 1
   1.230 +              check_result(check_limit > 0 && check_count > check_limit)
   1.231 +            }
   1.232 +          }
   1.233 +      }
   1.234 +
   1.235 +      val consumer =
   1.236 +      {
   1.237 +        val delay_nodes_status =
   1.238 +          Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
   1.239 +            progress.nodes_status(use_theories_state.value.nodes_status)
   1.240 +          }
   1.241 +
   1.242 +        val delay_commit_clean =
   1.243 +          Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
   1.244 +            val clean = use_theories_state.value.already_committed.keySet
   1.245 +            resources.clean_theories(session, id, clean)
   1.246 +          }
   1.247 +
   1.248 +        val dep_theories_set = dep_theories.toSet
   1.249 +
   1.250 +        Session.Consumer[Session.Commands_Changed](getClass.getName) {
   1.251 +          case changed =>
   1.252 +            if (changed.nodes.exists(dep_theories_set)) {
   1.253 +              val snapshot = session.snapshot()
   1.254 +              val state = snapshot.state
   1.255 +              val version = snapshot.version
   1.256 +
   1.257 +              val theory_progress =
   1.258 +                use_theories_state.change_result(st =>
   1.259 +                  {
   1.260 +                    val domain =
   1.261 +                      if (st.nodes_status.is_empty) dep_theories_set
   1.262 +                      else changed.nodes.iterator.filter(dep_theories_set).toSet
   1.263 +
   1.264 +                    val (nodes_status_changed, nodes_status1) =
   1.265 +                      st.nodes_status.update(resources.session_base, state, version,
   1.266 +                        domain = Some(domain), trim = changed.assignment)
   1.267 +
   1.268 +                    if (nodes_status_delay >= Time.zero && nodes_status_changed) {
   1.269 +                      delay_nodes_status.invoke
   1.270 +                    }
   1.271 +
   1.272 +                    val theory_progress =
   1.273 +                      (for {
   1.274 +                        (name, node_status) <- nodes_status1.present.iterator
   1.275 +                        if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
   1.276 +                        p1 = node_status.percentage
   1.277 +                        if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
   1.278 +                      } yield Progress.Theory(name.theory, percentage = Some(p1))).toList
   1.279 +
   1.280 +                    (theory_progress, st.update(nodes_status1))
   1.281 +                  })
   1.282 +
   1.283 +              theory_progress.foreach(progress.theory(_))
   1.284 +
   1.285 +              check_result()
   1.286 +
   1.287 +              if (commit.isDefined && commit_cleanup_delay > Time.zero) {
   1.288 +                if (use_theories_state.value.finished_result)
   1.289 +                  delay_commit_clean.revoke
   1.290 +                else delay_commit_clean.invoke
   1.291 +              }
   1.292 +            }
   1.293 +        }
   1.294 +      }
   1.295 +
   1.296 +      try {
   1.297 +        session.commands_changed += consumer
   1.298 +        resources.load_theories(session, id, dep_theories, progress)
   1.299 +        use_theories_state.value.await_result
   1.300 +        check_progress.cancel
   1.301 +      }
   1.302 +      finally {
   1.303 +        session.commands_changed -= consumer
   1.304 +        resources.unload_theories(session, id, dep_theories)
   1.305 +      }
   1.306 +
   1.307 +      use_theories_state.value.join_result
   1.308 +    }
   1.309 +
   1.310 +    def purge_theories(
   1.311 +      theories: List[String],
   1.312 +      qualifier: String = Sessions.DRAFT,
   1.313 +      master_dir: String = "",
   1.314 +      all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
   1.315 +    {
   1.316 +      val nodes =
   1.317 +        if (all) None
   1.318 +        else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _)))
   1.319 +      resources.purge_theories(session, nodes)
   1.320 +    }
   1.321 +  }
   1.322 +
   1.323 +
   1.324 +
   1.325 +  /** resources **/
   1.326 +
   1.327 +  object Resources
   1.328 +  {
   1.329 +    final class Theory private[Headless](
   1.330 +      val node_name: Document.Node.Name,
   1.331 +      val node_header: Document.Node.Header,
   1.332 +      val text: String,
   1.333 +      val node_required: Boolean)
   1.334 +    {
   1.335 +      override def toString: String = node_name.toString
   1.336 +
   1.337 +      def node_perspective: Document.Node.Perspective_Text =
   1.338 +        Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
   1.339 +
   1.340 +      def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
   1.341 +        List(node_name -> Document.Node.Deps(node_header),
   1.342 +          node_name -> Document.Node.Edits(text_edits),
   1.343 +          node_name -> node_perspective)
   1.344 +
   1.345 +      def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
   1.346 +      {
   1.347 +        val (text_edits, old_required) =
   1.348 +          if (old.isEmpty) (Text.Edit.inserts(0, text), false)
   1.349 +          else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
   1.350 +
   1.351 +        if (text_edits.isEmpty && node_required == old_required) Nil
   1.352 +        else make_edits(text_edits)
   1.353 +      }
   1.354 +
   1.355 +      def purge_edits: List[Document.Edit_Text] =
   1.356 +        make_edits(Text.Edit.removes(0, text))
   1.357 +
   1.358 +      def required(required: Boolean): Theory =
   1.359 +        if (required == node_required) this
   1.360 +        else new Theory(node_name, node_header, text, required)
   1.361 +    }
   1.362 +
   1.363 +    sealed case class State(
   1.364 +      required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
   1.365 +      theories: Map[Document.Node.Name, Theory] = Map.empty)
   1.366 +    {
   1.367 +      lazy val theory_graph: Graph[Document.Node.Name, Unit] =
   1.368 +      {
   1.369 +        val entries =
   1.370 +          for ((name, theory) <- theories.toList)
   1.371 +          yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
   1.372 +        Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
   1.373 +      }
   1.374 +
   1.375 +      def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
   1.376 +
   1.377 +      def insert_required(id: UUID, names: List[Document.Node.Name]): State =
   1.378 +        copy(required = (required /: names)(_.insert(_, id)))
   1.379 +
   1.380 +      def remove_required(id: UUID, names: List[Document.Node.Name]): State =
   1.381 +        copy(required = (required /: names)(_.remove(_, id)))
   1.382 +
   1.383 +      def update_theories(update: List[(Document.Node.Name, Theory)]): State =
   1.384 +        copy(theories =
   1.385 +          (theories /: update)({ case (thys, (name, thy)) =>
   1.386 +            thys.get(name) match {
   1.387 +              case Some(thy1) if thy1 == thy => thys
   1.388 +              case _ => thys + (name -> thy)
   1.389 +            }
   1.390 +          }))
   1.391 +
   1.392 +      def remove_theories(remove: List[Document.Node.Name]): State =
   1.393 +      {
   1.394 +        require(remove.forall(name => !is_required(name)))
   1.395 +        copy(theories = theories -- remove)
   1.396 +      }
   1.397 +
   1.398 +      def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name]): State =
   1.399 +      {
   1.400 +        val st1 = remove_required(id, dep_theories)
   1.401 +        val theory_edits =
   1.402 +          for {
   1.403 +            node_name <- dep_theories
   1.404 +            theory <- st1.theories.get(node_name)
   1.405 +          }
   1.406 +          yield {
   1.407 +            val theory1 = theory.required(st1.is_required(node_name))
   1.408 +            val edits = theory1.node_edits(Some(theory))
   1.409 +            (edits, (node_name, theory1))
   1.410 +          }
   1.411 +        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   1.412 +        st1.update_theories(theory_edits.map(_._2))
   1.413 +      }
   1.414 +
   1.415 +      def purge_theories(session: Session, nodes: List[Document.Node.Name])
   1.416 +        : ((List[Document.Node.Name], List[Document.Node.Name]), State) =
   1.417 +      {
   1.418 +        val all_nodes = theory_graph.topological_order
   1.419 +        val purge = nodes.filterNot(is_required(_)).toSet
   1.420 +
   1.421 +        val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
   1.422 +        val (retained, purged) = all_nodes.partition(retain)
   1.423 +
   1.424 +        val purge_edits = purged.flatMap(name => theories(name).purge_edits)
   1.425 +        session.update(Document.Blobs.empty, purge_edits)
   1.426 +
   1.427 +        ((purged, retained), remove_theories(purged))
   1.428 +      }
   1.429 +
   1.430 +      def frontier_theories(clean: Set[Document.Node.Name]): Set[Document.Node.Name] =
   1.431 +      {
   1.432 +        @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name])
   1.433 +          : Set[Document.Node.Name] =
   1.434 +        {
   1.435 +          val add = base.filter(b => theory_graph.imm_succs(b).forall(front))
   1.436 +          if (add.isEmpty) front
   1.437 +          else {
   1.438 +            val pre_add = add.map(theory_graph.imm_preds)
   1.439 +            val base1 = (pre_add.head /: pre_add.tail)(_ ++ _).toList.filter(clean)
   1.440 +            frontier(base1, front ++ add)
   1.441 +          }
   1.442 +        }
   1.443 +        frontier(theory_graph.maximals.filter(clean), Set.empty)
   1.444 +      }
   1.445 +    }
   1.446 +  }
   1.447 +
   1.448 +  class Resources(session_base: Sessions.Base, log: Logger = No_Logger)
   1.449 +    extends isabelle.Resources(session_base, log = log)
   1.450 +  {
   1.451 +    resources =>
   1.452 +
   1.453 +    private val state = Synchronized(Resources.State())
   1.454 +
   1.455 +    def load_theories(
   1.456 +      session: Session,
   1.457 +      id: UUID,
   1.458 +      dep_theories: List[Document.Node.Name],
   1.459 +      progress: Progress)
   1.460 +    {
   1.461 +      val loaded_theories =
   1.462 +        for (node_name <- dep_theories)
   1.463 +        yield {
   1.464 +          val path = node_name.path
   1.465 +          if (!node_name.is_theory) error("Not a theory file: " + path)
   1.466 +
   1.467 +          progress.expose_interrupt()
   1.468 +          val text = File.read(path)
   1.469 +          val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
   1.470 +          new Resources.Theory(node_name, node_header, text, true)
   1.471 +        }
   1.472 +
   1.473 +      val loaded = loaded_theories.length
   1.474 +      if (loaded > 1) progress.echo("Loading " + loaded + " theories ...")
   1.475 +
   1.476 +      state.change(st =>
   1.477 +        {
   1.478 +          val st1 = st.insert_required(id, dep_theories)
   1.479 +          val theory_edits =
   1.480 +            for (theory <- loaded_theories)
   1.481 +            yield {
   1.482 +              val node_name = theory.node_name
   1.483 +              val theory1 = theory.required(st1.is_required(node_name))
   1.484 +              val edits = theory1.node_edits(st1.theories.get(node_name))
   1.485 +              (edits, (node_name, theory1))
   1.486 +            }
   1.487 +          session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   1.488 +          st1.update_theories(theory_edits.map(_._2))
   1.489 +        })
   1.490 +    }
   1.491 +
   1.492 +    def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
   1.493 +    {
   1.494 +      state.change(_.unload_theories(session, id, dep_theories))
   1.495 +    }
   1.496 +
   1.497 +    def clean_theories(session: Session, id: UUID, clean: Set[Document.Node.Name])
   1.498 +    {
   1.499 +      state.change(st =>
   1.500 +        {
   1.501 +          val frontier = st.frontier_theories(clean).toList
   1.502 +          if (frontier.isEmpty) st
   1.503 +          else {
   1.504 +            val st1 = st.unload_theories(session, id, frontier)
   1.505 +            val (_, st2) = st1.purge_theories(session, frontier)
   1.506 +            st2
   1.507 +          }
   1.508 +        })
   1.509 +    }
   1.510 +
   1.511 +    def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
   1.512 +      : (List[Document.Node.Name], List[Document.Node.Name]) =
   1.513 +    {
   1.514 +      state.change_result(st => st.purge_theories(session, nodes getOrElse st.theory_graph.keys))
   1.515 +    }
   1.516 +  }
   1.517 +}
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Mon Sep 17 22:11:12 2018 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,511 +0,0 @@
     2.4 -/*  Title:      Pure/Thy/thy_resources.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -PIDE resources for theory files: load/unload theories via PIDE document updates.
     2.8 -*/
     2.9 -
    2.10 -package isabelle
    2.11 -
    2.12 -
    2.13 -import java.io.{File => JFile}
    2.14 -
    2.15 -import scala.annotation.tailrec
    2.16 -
    2.17 -
    2.18 -object Thy_Resources
    2.19 -{
    2.20 -  /* PIDE session */
    2.21 -
    2.22 -  def start_session(
    2.23 -    options: Options,
    2.24 -    session_name: String,
    2.25 -    session_dirs: List[Path] = Nil,
    2.26 -    include_sessions: List[String] = Nil,
    2.27 -    session_base: Option[Sessions.Base] = None,
    2.28 -    print_mode: List[String] = Nil,
    2.29 -    progress: Progress = No_Progress,
    2.30 -    log: Logger = No_Logger): Session =
    2.31 -  {
    2.32 -    val base =
    2.33 -      session_base getOrElse
    2.34 -        Sessions.base_info(options, session_name, include_sessions = include_sessions,
    2.35 -          progress = progress, dirs = session_dirs).check_base
    2.36 -    val resources = new Thy_Resources(base, log = log)
    2.37 -    val session = new Session(session_name, options, resources)
    2.38 -
    2.39 -    val session_error = Future.promise[String]
    2.40 -    var session_phase: Session.Consumer[Session.Phase] = null
    2.41 -    session_phase =
    2.42 -      Session.Consumer(getClass.getName) {
    2.43 -        case Session.Ready =>
    2.44 -          session.phase_changed -= session_phase
    2.45 -          session_error.fulfill("")
    2.46 -        case Session.Terminated(result) if !result.ok =>
    2.47 -          session.phase_changed -= session_phase
    2.48 -          session_error.fulfill("Session start failed: return code " + result.rc)
    2.49 -        case _ =>
    2.50 -      }
    2.51 -    session.phase_changed += session_phase
    2.52 -
    2.53 -    progress.echo("Starting session " + session_name + " ...")
    2.54 -    Isabelle_Process.start(session, options,
    2.55 -      logic = session_name, dirs = session_dirs, modes = print_mode)
    2.56 -
    2.57 -    session_error.join match {
    2.58 -      case "" => session
    2.59 -      case msg => session.stop(); error(msg)
    2.60 -    }
    2.61 -  }
    2.62 -
    2.63 -  private def stable_snapshot(
    2.64 -    state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
    2.65 -  {
    2.66 -    val snapshot = state.snapshot(name)
    2.67 -    assert(version.id == snapshot.version.id)
    2.68 -    snapshot
    2.69 -  }
    2.70 -
    2.71 -  class Theories_Result private[Thy_Resources](
    2.72 -    val state: Document.State,
    2.73 -    val version: Document.Version,
    2.74 -    val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
    2.75 -    val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
    2.76 -  {
    2.77 -    def snapshot(name: Document.Node.Name): Document.Snapshot =
    2.78 -      stable_snapshot(state, version, name)
    2.79 -
    2.80 -    def ok: Boolean =
    2.81 -      (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
    2.82 -  }
    2.83 -
    2.84 -  val default_check_delay = Time.seconds(0.5)
    2.85 -  val default_nodes_status_delay = Time.seconds(-1.0)
    2.86 -  val default_commit_cleanup_delay = Time.seconds(60.0)
    2.87 -  val default_watchdog_timeout = Time.seconds(600.0)
    2.88 -
    2.89 -
    2.90 -  class Session private[Thy_Resources](
    2.91 -    session_name: String,
    2.92 -    session_options: Options,
    2.93 -    override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
    2.94 -  {
    2.95 -    session =>
    2.96 -
    2.97 -
    2.98 -    /* temporary directory */
    2.99 -
   2.100 -    val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
   2.101 -    val tmp_dir_name: String = File.path(tmp_dir).implode
   2.102 -
   2.103 -    def master_directory(master_dir: String): String =
   2.104 -      proper_string(master_dir) getOrElse tmp_dir_name
   2.105 -
   2.106 -    override def toString: String = session_name
   2.107 -
   2.108 -    override def stop(): Process_Result =
   2.109 -    {
   2.110 -      try { super.stop() }
   2.111 -      finally { Isabelle_System.rm_tree(tmp_dir) }
   2.112 -    }
   2.113 -
   2.114 -
   2.115 -    /* theories */
   2.116 -
   2.117 -    private sealed case class Use_Theories_State(
   2.118 -      last_update: Time = Time.now(),
   2.119 -      nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
   2.120 -      already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
   2.121 -      result: Promise[Theories_Result] = Future.promise[Theories_Result])
   2.122 -    {
   2.123 -      def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
   2.124 -        copy(last_update = Time.now(), nodes_status = new_nodes_status)
   2.125 -
   2.126 -      def watchdog(watchdog_timeout: Time): Boolean =
   2.127 -        watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
   2.128 -
   2.129 -      def cancel_result { result.cancel }
   2.130 -      def finished_result: Boolean = result.is_finished
   2.131 -      def await_result { result.join_result }
   2.132 -      def join_result: Theories_Result = result.join
   2.133 -      def check_result(
   2.134 -          state: Document.State,
   2.135 -          version: Document.Version,
   2.136 -          dep_theories: List[Document.Node.Name],
   2.137 -          beyond_limit: Boolean,
   2.138 -          watchdog_timeout: Time,
   2.139 -          commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
   2.140 -        : Use_Theories_State =
   2.141 -      {
   2.142 -        val st1 =
   2.143 -          if (commit.isDefined) {
   2.144 -            val already_committed1 =
   2.145 -              (already_committed /: dep_theories)({ case (committed, name) =>
   2.146 -                def parents_committed: Boolean =
   2.147 -                  version.nodes(name).header.imports.forall({ case (parent, _) =>
   2.148 -                    Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
   2.149 -                  })
   2.150 -                if (!committed.isDefinedAt(name) && parents_committed &&
   2.151 -                    state.node_consolidated(version, name))
   2.152 -                {
   2.153 -                  val snapshot = stable_snapshot(state, version, name)
   2.154 -                  val status = Document_Status.Node_Status.make(state, version, name)
   2.155 -                  commit.get.apply(snapshot, status)
   2.156 -                  committed + (name -> status)
   2.157 -                }
   2.158 -                else committed
   2.159 -              })
   2.160 -            copy(already_committed = already_committed1)
   2.161 -          }
   2.162 -          else this
   2.163 -
   2.164 -        if (beyond_limit || watchdog(watchdog_timeout) ||
   2.165 -          dep_theories.forall(name =>
   2.166 -            already_committed.isDefinedAt(name) ||
   2.167 -            state.node_consolidated(version, name) ||
   2.168 -            nodes_status.quasi_consolidated(name)))
   2.169 -        {
   2.170 -          val nodes =
   2.171 -            for (name <- dep_theories)
   2.172 -            yield { (name -> Document_Status.Node_Status.make(state, version, name)) }
   2.173 -          val nodes_committed =
   2.174 -            for {
   2.175 -              name <- dep_theories
   2.176 -              status <- already_committed.get(name)
   2.177 -            } yield (name -> status)
   2.178 -
   2.179 -          try { result.fulfill(new Theories_Result(state, version, nodes, nodes_committed)) }
   2.180 -          catch { case _: IllegalStateException => }
   2.181 -        }
   2.182 -
   2.183 -        st1
   2.184 -      }
   2.185 -    }
   2.186 -
   2.187 -    def use_theories(
   2.188 -      theories: List[String],
   2.189 -      qualifier: String = Sessions.DRAFT,
   2.190 -      master_dir: String = "",
   2.191 -      check_delay: Time = default_check_delay,
   2.192 -      check_limit: Int = 0,
   2.193 -      watchdog_timeout: Time = default_watchdog_timeout,
   2.194 -      nodes_status_delay: Time = default_nodes_status_delay,
   2.195 -      id: UUID = UUID(),
   2.196 -      // commit: must not block, must not fail
   2.197 -      commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
   2.198 -      commit_cleanup_delay: Time = default_commit_cleanup_delay,
   2.199 -      progress: Progress = No_Progress): Theories_Result =
   2.200 -    {
   2.201 -      val dep_theories =
   2.202 -      {
   2.203 -        val import_names =
   2.204 -          theories.map(thy =>
   2.205 -            resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none)
   2.206 -        resources.dependencies(import_names, progress = progress).check_errors.theories
   2.207 -      }
   2.208 -
   2.209 -      val use_theories_state = Synchronized(Use_Theories_State())
   2.210 -
   2.211 -      def check_result(beyond_limit: Boolean = false)
   2.212 -      {
   2.213 -        val state = session.current_state()
   2.214 -        state.stable_tip_version match {
   2.215 -          case Some(version) =>
   2.216 -            use_theories_state.change(
   2.217 -              _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit))
   2.218 -          case None =>
   2.219 -        }
   2.220 -      }
   2.221 -
   2.222 -      val check_progress =
   2.223 -      {
   2.224 -        var check_count = 0
   2.225 -        Event_Timer.request(Time.now(), repeat = Some(check_delay))
   2.226 -          {
   2.227 -            if (progress.stopped) use_theories_state.value.cancel_result
   2.228 -            else {
   2.229 -              check_count += 1
   2.230 -              check_result(check_limit > 0 && check_count > check_limit)
   2.231 -            }
   2.232 -          }
   2.233 -      }
   2.234 -
   2.235 -      val consumer =
   2.236 -      {
   2.237 -        val delay_nodes_status =
   2.238 -          Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
   2.239 -            progress.nodes_status(use_theories_state.value.nodes_status)
   2.240 -          }
   2.241 -
   2.242 -        val delay_commit_clean =
   2.243 -          Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
   2.244 -            val clean = use_theories_state.value.already_committed.keySet
   2.245 -            resources.clean_theories(session, id, clean)
   2.246 -          }
   2.247 -
   2.248 -        val dep_theories_set = dep_theories.toSet
   2.249 -
   2.250 -        Session.Consumer[Session.Commands_Changed](getClass.getName) {
   2.251 -          case changed =>
   2.252 -            if (changed.nodes.exists(dep_theories_set)) {
   2.253 -              val snapshot = session.snapshot()
   2.254 -              val state = snapshot.state
   2.255 -              val version = snapshot.version
   2.256 -
   2.257 -              val theory_progress =
   2.258 -                use_theories_state.change_result(st =>
   2.259 -                  {
   2.260 -                    val domain =
   2.261 -                      if (st.nodes_status.is_empty) dep_theories_set
   2.262 -                      else changed.nodes.iterator.filter(dep_theories_set).toSet
   2.263 -
   2.264 -                    val (nodes_status_changed, nodes_status1) =
   2.265 -                      st.nodes_status.update(resources.session_base, state, version,
   2.266 -                        domain = Some(domain), trim = changed.assignment)
   2.267 -
   2.268 -                    if (nodes_status_delay >= Time.zero && nodes_status_changed) {
   2.269 -                      delay_nodes_status.invoke
   2.270 -                    }
   2.271 -
   2.272 -                    val theory_progress =
   2.273 -                      (for {
   2.274 -                        (name, node_status) <- nodes_status1.present.iterator
   2.275 -                        if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
   2.276 -                        p1 = node_status.percentage
   2.277 -                        if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
   2.278 -                      } yield Progress.Theory(name.theory, percentage = Some(p1))).toList
   2.279 -
   2.280 -                    (theory_progress, st.update(nodes_status1))
   2.281 -                  })
   2.282 -
   2.283 -              theory_progress.foreach(progress.theory(_))
   2.284 -
   2.285 -              check_result()
   2.286 -
   2.287 -              if (commit.isDefined && commit_cleanup_delay > Time.zero) {
   2.288 -                if (use_theories_state.value.finished_result)
   2.289 -                  delay_commit_clean.revoke
   2.290 -                else delay_commit_clean.invoke
   2.291 -              }
   2.292 -            }
   2.293 -        }
   2.294 -      }
   2.295 -
   2.296 -      try {
   2.297 -        session.commands_changed += consumer
   2.298 -        resources.load_theories(session, id, dep_theories, progress)
   2.299 -        use_theories_state.value.await_result
   2.300 -        check_progress.cancel
   2.301 -      }
   2.302 -      finally {
   2.303 -        session.commands_changed -= consumer
   2.304 -        resources.unload_theories(session, id, dep_theories)
   2.305 -      }
   2.306 -
   2.307 -      use_theories_state.value.join_result
   2.308 -    }
   2.309 -
   2.310 -    def purge_theories(
   2.311 -      theories: List[String],
   2.312 -      qualifier: String = Sessions.DRAFT,
   2.313 -      master_dir: String = "",
   2.314 -      all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
   2.315 -    {
   2.316 -      val nodes =
   2.317 -        if (all) None
   2.318 -        else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _)))
   2.319 -      resources.purge_theories(session, nodes)
   2.320 -    }
   2.321 -  }
   2.322 -
   2.323 -
   2.324 -  /* internal state */
   2.325 -
   2.326 -  final class Theory private[Thy_Resources](
   2.327 -    val node_name: Document.Node.Name,
   2.328 -    val node_header: Document.Node.Header,
   2.329 -    val text: String,
   2.330 -    val node_required: Boolean)
   2.331 -  {
   2.332 -    override def toString: String = node_name.toString
   2.333 -
   2.334 -    def node_perspective: Document.Node.Perspective_Text =
   2.335 -      Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
   2.336 -
   2.337 -    def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
   2.338 -      List(node_name -> Document.Node.Deps(node_header),
   2.339 -        node_name -> Document.Node.Edits(text_edits),
   2.340 -        node_name -> node_perspective)
   2.341 -
   2.342 -    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
   2.343 -    {
   2.344 -      val (text_edits, old_required) =
   2.345 -        if (old.isEmpty) (Text.Edit.inserts(0, text), false)
   2.346 -        else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
   2.347 -
   2.348 -      if (text_edits.isEmpty && node_required == old_required) Nil
   2.349 -      else make_edits(text_edits)
   2.350 -    }
   2.351 -
   2.352 -    def purge_edits: List[Document.Edit_Text] =
   2.353 -      make_edits(Text.Edit.removes(0, text))
   2.354 -
   2.355 -    def required(required: Boolean): Theory =
   2.356 -      if (required == node_required) this
   2.357 -      else new Theory(node_name, node_header, text, required)
   2.358 -  }
   2.359 -
   2.360 -  sealed case class State(
   2.361 -    required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
   2.362 -    theories: Map[Document.Node.Name, Theory] = Map.empty)
   2.363 -  {
   2.364 -    lazy val theory_graph: Graph[Document.Node.Name, Unit] =
   2.365 -    {
   2.366 -      val entries =
   2.367 -        for ((name, theory) <- theories.toList)
   2.368 -        yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
   2.369 -      Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
   2.370 -    }
   2.371 -
   2.372 -    def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
   2.373 -
   2.374 -    def insert_required(id: UUID, names: List[Document.Node.Name]): State =
   2.375 -      copy(required = (required /: names)(_.insert(_, id)))
   2.376 -
   2.377 -    def remove_required(id: UUID, names: List[Document.Node.Name]): State =
   2.378 -      copy(required = (required /: names)(_.remove(_, id)))
   2.379 -
   2.380 -    def update_theories(update: List[(Document.Node.Name, Theory)]): State =
   2.381 -      copy(theories =
   2.382 -        (theories /: update)({ case (thys, (name, thy)) =>
   2.383 -          thys.get(name) match {
   2.384 -            case Some(thy1) if thy1 == thy => thys
   2.385 -            case _ => thys + (name -> thy)
   2.386 -          }
   2.387 -        }))
   2.388 -
   2.389 -    def remove_theories(remove: List[Document.Node.Name]): State =
   2.390 -    {
   2.391 -      require(remove.forall(name => !is_required(name)))
   2.392 -      copy(theories = theories -- remove)
   2.393 -    }
   2.394 -
   2.395 -    def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name]): State =
   2.396 -    {
   2.397 -      val st1 = remove_required(id, dep_theories)
   2.398 -      val theory_edits =
   2.399 -        for {
   2.400 -          node_name <- dep_theories
   2.401 -          theory <- st1.theories.get(node_name)
   2.402 -        }
   2.403 -        yield {
   2.404 -          val theory1 = theory.required(st1.is_required(node_name))
   2.405 -          val edits = theory1.node_edits(Some(theory))
   2.406 -          (edits, (node_name, theory1))
   2.407 -        }
   2.408 -      session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   2.409 -      st1.update_theories(theory_edits.map(_._2))
   2.410 -    }
   2.411 -
   2.412 -    def purge_theories(session: Session, nodes: List[Document.Node.Name])
   2.413 -      : ((List[Document.Node.Name], List[Document.Node.Name]), State) =
   2.414 -    {
   2.415 -      val all_nodes = theory_graph.topological_order
   2.416 -      val purge = nodes.filterNot(is_required(_)).toSet
   2.417 -
   2.418 -      val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
   2.419 -      val (retained, purged) = all_nodes.partition(retain)
   2.420 -
   2.421 -      val purge_edits = purged.flatMap(name => theories(name).purge_edits)
   2.422 -      session.update(Document.Blobs.empty, purge_edits)
   2.423 -
   2.424 -      ((purged, retained), remove_theories(purged))
   2.425 -    }
   2.426 -
   2.427 -    def frontier_theories(clean: Set[Document.Node.Name]): Set[Document.Node.Name] =
   2.428 -    {
   2.429 -      @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name])
   2.430 -        : Set[Document.Node.Name] =
   2.431 -      {
   2.432 -        val add = base.filter(b => theory_graph.imm_succs(b).forall(front))
   2.433 -        if (add.isEmpty) front
   2.434 -        else {
   2.435 -          val pre_add = add.map(theory_graph.imm_preds)
   2.436 -          val base1 = (pre_add.head /: pre_add.tail)(_ ++ _).toList.filter(clean)
   2.437 -          frontier(base1, front ++ add)
   2.438 -        }
   2.439 -      }
   2.440 -      frontier(theory_graph.maximals.filter(clean), Set.empty)
   2.441 -    }
   2.442 -  }
   2.443 -}
   2.444 -
   2.445 -class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
   2.446 -  extends Resources(session_base, log = log)
   2.447 -{
   2.448 -  resources =>
   2.449 -
   2.450 -  private val state = Synchronized(Thy_Resources.State())
   2.451 -
   2.452 -  def load_theories(
   2.453 -    session: Session,
   2.454 -    id: UUID,
   2.455 -    dep_theories: List[Document.Node.Name],
   2.456 -    progress: Progress)
   2.457 -  {
   2.458 -    val loaded_theories =
   2.459 -      for (node_name <- dep_theories)
   2.460 -      yield {
   2.461 -        val path = node_name.path
   2.462 -        if (!node_name.is_theory) error("Not a theory file: " + path)
   2.463 -
   2.464 -        progress.expose_interrupt()
   2.465 -        val text = File.read(path)
   2.466 -        val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
   2.467 -        new Thy_Resources.Theory(node_name, node_header, text, true)
   2.468 -      }
   2.469 -
   2.470 -    val loaded = loaded_theories.length
   2.471 -    if (loaded > 1) progress.echo("Loading " + loaded + " theories ...")
   2.472 -
   2.473 -    state.change(st =>
   2.474 -      {
   2.475 -        val st1 = st.insert_required(id, dep_theories)
   2.476 -        val theory_edits =
   2.477 -          for (theory <- loaded_theories)
   2.478 -          yield {
   2.479 -            val node_name = theory.node_name
   2.480 -            val theory1 = theory.required(st1.is_required(node_name))
   2.481 -            val edits = theory1.node_edits(st1.theories.get(node_name))
   2.482 -            (edits, (node_name, theory1))
   2.483 -          }
   2.484 -        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   2.485 -        st1.update_theories(theory_edits.map(_._2))
   2.486 -      })
   2.487 -  }
   2.488 -
   2.489 -  def unload_theories(
   2.490 -    session: Thy_Resources.Session, id: UUID, dep_theories: List[Document.Node.Name])
   2.491 -  {
   2.492 -    state.change(_.unload_theories(session, id, dep_theories))
   2.493 -  }
   2.494 -
   2.495 -  def clean_theories(session: Thy_Resources.Session, id: UUID, clean: Set[Document.Node.Name])
   2.496 -  {
   2.497 -    state.change(st =>
   2.498 -      {
   2.499 -        val frontier = st.frontier_theories(clean).toList
   2.500 -        if (frontier.isEmpty) st
   2.501 -        else {
   2.502 -          val st1 = st.unload_theories(session, id, frontier)
   2.503 -          val (_, st2) = st1.purge_theories(session, frontier)
   2.504 -          st2
   2.505 -        }
   2.506 -      })
   2.507 -  }
   2.508 -
   2.509 -  def purge_theories(session: Thy_Resources.Session, nodes: Option[List[Document.Node.Name]])
   2.510 -    : (List[Document.Node.Name], List[Document.Node.Name]) =
   2.511 -  {
   2.512 -    state.change_result(st => st.purge_theories(session, nodes getOrElse st.theory_graph.keys))
   2.513 -  }
   2.514 -}
     3.1 --- a/src/Pure/Tools/dump.scala	Mon Sep 17 22:11:12 2018 +0200
     3.2 +++ b/src/Pure/Tools/dump.scala	Tue Sep 18 11:05:14 2018 +0200
     3.3 @@ -92,8 +92,8 @@
     3.4      select_dirs: List[Path] = Nil,
     3.5      output_dir: Path = default_output_dir,
     3.6      verbose: Boolean = false,
     3.7 -    commit_cleanup_delay: Time = Thy_Resources.default_commit_cleanup_delay,
     3.8 -    watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
     3.9 +    commit_cleanup_delay: Time = Headless.default_commit_cleanup_delay,
    3.10 +    watchdog_timeout: Time = Headless.default_watchdog_timeout,
    3.11      system_mode: Boolean = false,
    3.12      selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
    3.13    {
    3.14 @@ -155,7 +155,7 @@
    3.15      /* session */
    3.16  
    3.17      val session =
    3.18 -      Thy_Resources.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
    3.19 +      Headless.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
    3.20          include_sessions = include_sessions, progress = progress, log = log)
    3.21  
    3.22      val theories_result =
    3.23 @@ -181,11 +181,11 @@
    3.24      {
    3.25        var aspects: List[Aspect] = known_aspects
    3.26        var base_sessions: List[String] = Nil
    3.27 -      var commit_cleanup_delay = Thy_Resources.default_commit_cleanup_delay
    3.28 +      var commit_cleanup_delay = Headless.default_commit_cleanup_delay
    3.29        var select_dirs: List[Path] = Nil
    3.30        var output_dir = default_output_dir
    3.31        var requirements = false
    3.32 -      var watchdog_timeout = Thy_Resources.default_watchdog_timeout
    3.33 +      var watchdog_timeout = Headless.default_watchdog_timeout
    3.34        var exclude_session_groups: List[String] = Nil
    3.35        var all_sessions = false
    3.36        var dirs: List[Path] = Nil
    3.37 @@ -203,12 +203,12 @@
    3.38      -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
    3.39      -B NAME      include session NAME and all descendants
    3.40      -C SECONDS   delay for cleaning of already dumped theories (0 = disabled, default: """ +
    3.41 -      Value.Seconds(Thy_Resources.default_commit_cleanup_delay) + """)
    3.42 +      Value.Seconds(Headless.default_commit_cleanup_delay) + """)
    3.43      -D DIR       include session directory and select its sessions
    3.44      -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
    3.45      -R           operate on requirements of selected sessions
    3.46      -W SECONDS   watchdog timeout for PIDE processing (0 = disabled, default: """ +
    3.47 -      Value.Seconds(Thy_Resources.default_watchdog_timeout) + """)
    3.48 +      Value.Seconds(Headless.default_watchdog_timeout) + """)
    3.49      -X NAME      exclude sessions from group NAME and all descendants
    3.50      -a           select all sessions
    3.51      -d DIR       include session directory
     4.1 --- a/src/Pure/Tools/server.scala	Mon Sep 17 22:11:12 2018 +0200
     4.2 +++ b/src/Pure/Tools/server.scala	Tue Sep 18 11:05:14 2018 +0200
     4.3 @@ -506,12 +506,11 @@
     4.4  
     4.5    private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
     4.6  
     4.7 -  private val _sessions = Synchronized(Map.empty[UUID, Thy_Resources.Session])
     4.8 +  private val _sessions = Synchronized(Map.empty[UUID, Headless.Session])
     4.9    def err_session(id: UUID): Nothing = error("No session " + Library.single_quote(id.toString))
    4.10 -  def the_session(id: UUID): Thy_Resources.Session =
    4.11 -    _sessions.value.get(id) getOrElse err_session(id)
    4.12 -  def add_session(entry: (UUID, Thy_Resources.Session)) { _sessions.change(_ + entry) }
    4.13 -  def remove_session(id: UUID): Thy_Resources.Session =
    4.14 +  def the_session(id: UUID): Headless.Session = _sessions.value.get(id) getOrElse err_session(id)
    4.15 +  def add_session(entry: (UUID, Headless.Session)) { _sessions.change(_ + entry) }
    4.16 +  def remove_session(id: UUID): Headless.Session =
    4.17    {
    4.18      _sessions.change_result(sessions =>
    4.19        sessions.get(id) match {
     5.1 --- a/src/Pure/Tools/server_commands.scala	Mon Sep 17 22:11:12 2018 +0200
     5.2 +++ b/src/Pure/Tools/server_commands.scala	Tue Sep 18 11:05:14 2018 +0200
     5.3 @@ -107,14 +107,14 @@
     5.4        yield Args(build = build, print_mode = print_mode)
     5.5  
     5.6      def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
     5.7 -      : (JSON.Object.T, (UUID, Thy_Resources.Session)) =
     5.8 +      : (JSON.Object.T, (UUID, Headless.Session)) =
     5.9      {
    5.10        val base_info =
    5.11          try { Session_Build.command(args.build, progress = progress)._3 }
    5.12          catch { case exn: Server.Error => error(exn.message) }
    5.13  
    5.14        val session =
    5.15 -        Thy_Resources.start_session(
    5.16 +        Headless.start_session(
    5.17            base_info.options,
    5.18            base_info.session,
    5.19            session_dirs = base_info.dirs,
    5.20 @@ -139,7 +139,7 @@
    5.21      def unapply(json: JSON.T): Option[UUID] =
    5.22        JSON.uuid(json, "session_id")
    5.23  
    5.24 -    def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) =
    5.25 +    def command(session: Headless.Session): (JSON.Object.T, Process_Result) =
    5.26      {
    5.27        val result = session.stop()
    5.28        val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
    5.29 @@ -158,10 +158,10 @@
    5.30        pretty_margin: Double = Pretty.default_margin,
    5.31        unicode_symbols: Boolean = false,
    5.32        export_pattern: String = "",
    5.33 -      check_delay: Time = Thy_Resources.default_check_delay,
    5.34 +      check_delay: Time = Headless.default_check_delay,
    5.35        check_limit: Int = 0,
    5.36 -      watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
    5.37 -      nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
    5.38 +      watchdog_timeout: Time = Headless.default_watchdog_timeout,
    5.39 +      nodes_status_delay: Time = Headless.default_nodes_status_delay)
    5.40  
    5.41      def unapply(json: JSON.T): Option[Args] =
    5.42        for {
    5.43 @@ -171,12 +171,12 @@
    5.44          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    5.45          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
    5.46          export_pattern <- JSON.string_default(json, "export_pattern")
    5.47 -        check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay)
    5.48 +        check_delay <- JSON.seconds_default(json, "check_delay", Headless.default_check_delay)
    5.49          check_limit <- JSON.int_default(json, "check_limit")
    5.50          watchdog_timeout <-
    5.51 -          JSON.seconds_default(json, "watchdog_timeout", Thy_Resources.default_watchdog_timeout)
    5.52 +          JSON.seconds_default(json, "watchdog_timeout", Headless.default_watchdog_timeout)
    5.53          nodes_status_delay <-
    5.54 -          JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    5.55 +          JSON.seconds_default(json, "nodes_status_delay", Headless.default_nodes_status_delay)
    5.56        }
    5.57        yield {
    5.58          Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
    5.59 @@ -186,9 +186,9 @@
    5.60        }
    5.61  
    5.62      def command(args: Args,
    5.63 -      session: Thy_Resources.Session,
    5.64 +      session: Headless.Session,
    5.65        id: UUID = UUID(),
    5.66 -      progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) =
    5.67 +      progress: Progress = No_Progress): (JSON.Object.T, Headless.Theories_Result) =
    5.68      {
    5.69        val result =
    5.70          session.use_theories(args.theories, master_dir = args.master_dir,
    5.71 @@ -263,7 +263,7 @@
    5.72        }
    5.73        yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }
    5.74  
    5.75 -    def command(args: Args, session: Thy_Resources.Session)
    5.76 +    def command(args: Args, session: Headless.Session)
    5.77        : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) =
    5.78      {
    5.79        val (purged, retained) =
     6.1 --- a/src/Pure/build-jars	Mon Sep 17 22:11:12 2018 +0200
     6.2 +++ b/src/Pure/build-jars	Tue Sep 18 11:05:14 2018 +0200
     6.3 @@ -95,6 +95,7 @@
     6.4    PIDE/document_id.scala
     6.5    PIDE/document_status.scala
     6.6    PIDE/editor.scala
     6.7 +  PIDE/headless.scala
     6.8    PIDE/line.scala
     6.9    PIDE/markup.scala
    6.10    PIDE/markup_tree.scala
    6.11 @@ -137,7 +138,6 @@
    6.12    Thy/sessions.scala
    6.13    Thy/thy_element.scala
    6.14    Thy/thy_header.scala
    6.15 -  Thy/thy_resources.scala
    6.16    Thy/thy_syntax.scala
    6.17    Tools/dump.scala
    6.18    Tools/build.scala