--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/headless.scala Tue Sep 18 11:05:14 2018 +0200
@@ -0,0 +1,514 @@
+/* Title: Pure/PIDE/headless.scala
+ Author: Makarius
+
+Headless PIDE session and resources from file-system.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+import scala.annotation.tailrec
+
+
+object Headless
+{
+ /** session **/
+
+ def start_session(
+ options: Options,
+ session_name: String,
+ session_dirs: List[Path] = Nil,
+ include_sessions: List[String] = Nil,
+ session_base: Option[Sessions.Base] = None,
+ print_mode: List[String] = Nil,
+ progress: Progress = No_Progress,
+ log: Logger = No_Logger): Session =
+ {
+ val base =
+ session_base getOrElse
+ Sessions.base_info(options, session_name, include_sessions = include_sessions,
+ progress = progress, dirs = session_dirs).check_base
+ val resources = new Resources(base, log = log)
+ val session = new Session(session_name, options, resources)
+
+ val session_error = Future.promise[String]
+ var session_phase: Session.Consumer[Session.Phase] = null
+ session_phase =
+ Session.Consumer(getClass.getName) {
+ case Session.Ready =>
+ session.phase_changed -= session_phase
+ session_error.fulfill("")
+ case Session.Terminated(result) if !result.ok =>
+ session.phase_changed -= session_phase
+ session_error.fulfill("Session start failed: return code " + result.rc)
+ case _ =>
+ }
+ session.phase_changed += session_phase
+
+ progress.echo("Starting session " + session_name + " ...")
+ Isabelle_Process.start(session, options,
+ logic = session_name, dirs = session_dirs, modes = print_mode)
+
+ session_error.join match {
+ case "" => session
+ case msg => session.stop(); error(msg)
+ }
+ }
+
+ private def stable_snapshot(
+ state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
+ {
+ val snapshot = state.snapshot(name)
+ assert(version.id == snapshot.version.id)
+ snapshot
+ }
+
+ class Theories_Result private[Headless](
+ val state: Document.State,
+ val version: Document.Version,
+ val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
+ val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
+ {
+ def snapshot(name: Document.Node.Name): Document.Snapshot =
+ stable_snapshot(state, version, name)
+
+ def ok: Boolean =
+ (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
+ }
+
+ val default_check_delay = Time.seconds(0.5)
+ val default_nodes_status_delay = Time.seconds(-1.0)
+ val default_commit_cleanup_delay = Time.seconds(60.0)
+ val default_watchdog_timeout = Time.seconds(600.0)
+
+
+ class Session private[Headless](
+ session_name: String,
+ session_options: Options,
+ override val resources: Resources) extends isabelle.Session(session_options, resources)
+ {
+ session =>
+
+
+ /* temporary directory */
+
+ val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
+ val tmp_dir_name: String = File.path(tmp_dir).implode
+
+ def master_directory(master_dir: String): String =
+ proper_string(master_dir) getOrElse tmp_dir_name
+
+ override def toString: String = session_name
+
+ override def stop(): Process_Result =
+ {
+ try { super.stop() }
+ finally { Isabelle_System.rm_tree(tmp_dir) }
+ }
+
+
+ /* theories */
+
+ private sealed case class Use_Theories_State(
+ last_update: Time = Time.now(),
+ nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
+ already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
+ result: Promise[Theories_Result] = Future.promise[Theories_Result])
+ {
+ def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
+ copy(last_update = Time.now(), nodes_status = new_nodes_status)
+
+ def watchdog(watchdog_timeout: Time): Boolean =
+ watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
+
+ def cancel_result { result.cancel }
+ def finished_result: Boolean = result.is_finished
+ def await_result { result.join_result }
+ def join_result: Theories_Result = result.join
+ def check_result(
+ state: Document.State,
+ version: Document.Version,
+ dep_theories: List[Document.Node.Name],
+ beyond_limit: Boolean,
+ watchdog_timeout: Time,
+ commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
+ : Use_Theories_State =
+ {
+ val st1 =
+ if (commit.isDefined) {
+ val already_committed1 =
+ (already_committed /: dep_theories)({ case (committed, name) =>
+ def parents_committed: Boolean =
+ version.nodes(name).header.imports.forall({ case (parent, _) =>
+ Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
+ })
+ if (!committed.isDefinedAt(name) && parents_committed &&
+ state.node_consolidated(version, name))
+ {
+ val snapshot = stable_snapshot(state, version, name)
+ val status = Document_Status.Node_Status.make(state, version, name)
+ commit.get.apply(snapshot, status)
+ committed + (name -> status)
+ }
+ else committed
+ })
+ copy(already_committed = already_committed1)
+ }
+ else this
+
+ if (beyond_limit || watchdog(watchdog_timeout) ||
+ dep_theories.forall(name =>
+ already_committed.isDefinedAt(name) ||
+ state.node_consolidated(version, name) ||
+ nodes_status.quasi_consolidated(name)))
+ {
+ val nodes =
+ for (name <- dep_theories)
+ yield { (name -> Document_Status.Node_Status.make(state, version, name)) }
+ val nodes_committed =
+ for {
+ name <- dep_theories
+ status <- already_committed.get(name)
+ } yield (name -> status)
+
+ try { result.fulfill(new Theories_Result(state, version, nodes, nodes_committed)) }
+ catch { case _: IllegalStateException => }
+ }
+
+ st1
+ }
+ }
+
+ def use_theories(
+ theories: List[String],
+ qualifier: String = Sessions.DRAFT,
+ master_dir: String = "",
+ check_delay: Time = default_check_delay,
+ check_limit: Int = 0,
+ watchdog_timeout: Time = default_watchdog_timeout,
+ nodes_status_delay: Time = default_nodes_status_delay,
+ id: UUID = UUID(),
+ // commit: must not block, must not fail
+ commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
+ commit_cleanup_delay: Time = default_commit_cleanup_delay,
+ progress: Progress = No_Progress): Theories_Result =
+ {
+ val dep_theories =
+ {
+ val import_names =
+ theories.map(thy =>
+ resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none)
+ resources.dependencies(import_names, progress = progress).check_errors.theories
+ }
+
+ val use_theories_state = Synchronized(Use_Theories_State())
+
+ def check_result(beyond_limit: Boolean = false)
+ {
+ val state = session.current_state()
+ state.stable_tip_version match {
+ case Some(version) =>
+ use_theories_state.change(
+ _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit))
+ case None =>
+ }
+ }
+
+ val check_progress =
+ {
+ var check_count = 0
+ Event_Timer.request(Time.now(), repeat = Some(check_delay))
+ {
+ if (progress.stopped) use_theories_state.value.cancel_result
+ else {
+ check_count += 1
+ check_result(check_limit > 0 && check_count > check_limit)
+ }
+ }
+ }
+
+ val consumer =
+ {
+ val delay_nodes_status =
+ Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
+ progress.nodes_status(use_theories_state.value.nodes_status)
+ }
+
+ val delay_commit_clean =
+ Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
+ val clean = use_theories_state.value.already_committed.keySet
+ resources.clean_theories(session, id, clean)
+ }
+
+ val dep_theories_set = dep_theories.toSet
+
+ Session.Consumer[Session.Commands_Changed](getClass.getName) {
+ case changed =>
+ if (changed.nodes.exists(dep_theories_set)) {
+ val snapshot = session.snapshot()
+ val state = snapshot.state
+ val version = snapshot.version
+
+ val theory_progress =
+ use_theories_state.change_result(st =>
+ {
+ val domain =
+ if (st.nodes_status.is_empty) dep_theories_set
+ else changed.nodes.iterator.filter(dep_theories_set).toSet
+
+ val (nodes_status_changed, nodes_status1) =
+ st.nodes_status.update(resources.session_base, state, version,
+ domain = Some(domain), trim = changed.assignment)
+
+ if (nodes_status_delay >= Time.zero && nodes_status_changed) {
+ delay_nodes_status.invoke
+ }
+
+ val theory_progress =
+ (for {
+ (name, node_status) <- nodes_status1.present.iterator
+ if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
+ p1 = node_status.percentage
+ if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
+ } yield Progress.Theory(name.theory, percentage = Some(p1))).toList
+
+ (theory_progress, st.update(nodes_status1))
+ })
+
+ theory_progress.foreach(progress.theory(_))
+
+ check_result()
+
+ if (commit.isDefined && commit_cleanup_delay > Time.zero) {
+ if (use_theories_state.value.finished_result)
+ delay_commit_clean.revoke
+ else delay_commit_clean.invoke
+ }
+ }
+ }
+ }
+
+ try {
+ session.commands_changed += consumer
+ resources.load_theories(session, id, dep_theories, progress)
+ use_theories_state.value.await_result
+ check_progress.cancel
+ }
+ finally {
+ session.commands_changed -= consumer
+ resources.unload_theories(session, id, dep_theories)
+ }
+
+ use_theories_state.value.join_result
+ }
+
+ def purge_theories(
+ theories: List[String],
+ qualifier: String = Sessions.DRAFT,
+ master_dir: String = "",
+ all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
+ {
+ val nodes =
+ if (all) None
+ else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _)))
+ resources.purge_theories(session, nodes)
+ }
+ }
+
+
+
+ /** resources **/
+
+ object Resources
+ {
+ final class Theory private[Headless](
+ val node_name: Document.Node.Name,
+ val node_header: Document.Node.Header,
+ val text: String,
+ val node_required: Boolean)
+ {
+ override def toString: String = node_name.toString
+
+ def node_perspective: Document.Node.Perspective_Text =
+ Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
+
+ def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
+ List(node_name -> Document.Node.Deps(node_header),
+ node_name -> Document.Node.Edits(text_edits),
+ node_name -> node_perspective)
+
+ def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
+ {
+ val (text_edits, old_required) =
+ if (old.isEmpty) (Text.Edit.inserts(0, text), false)
+ else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
+
+ if (text_edits.isEmpty && node_required == old_required) Nil
+ else make_edits(text_edits)
+ }
+
+ def purge_edits: List[Document.Edit_Text] =
+ make_edits(Text.Edit.removes(0, text))
+
+ def required(required: Boolean): Theory =
+ if (required == node_required) this
+ else new Theory(node_name, node_header, text, required)
+ }
+
+ sealed case class State(
+ required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
+ theories: Map[Document.Node.Name, Theory] = Map.empty)
+ {
+ lazy val theory_graph: Graph[Document.Node.Name, Unit] =
+ {
+ val entries =
+ for ((name, theory) <- theories.toList)
+ yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
+ Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
+ }
+
+ def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
+
+ def insert_required(id: UUID, names: List[Document.Node.Name]): State =
+ copy(required = (required /: names)(_.insert(_, id)))
+
+ def remove_required(id: UUID, names: List[Document.Node.Name]): State =
+ copy(required = (required /: names)(_.remove(_, id)))
+
+ def update_theories(update: List[(Document.Node.Name, Theory)]): State =
+ copy(theories =
+ (theories /: update)({ case (thys, (name, thy)) =>
+ thys.get(name) match {
+ case Some(thy1) if thy1 == thy => thys
+ case _ => thys + (name -> thy)
+ }
+ }))
+
+ def remove_theories(remove: List[Document.Node.Name]): State =
+ {
+ require(remove.forall(name => !is_required(name)))
+ copy(theories = theories -- remove)
+ }
+
+ def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name]): State =
+ {
+ val st1 = remove_required(id, dep_theories)
+ val theory_edits =
+ for {
+ node_name <- dep_theories
+ theory <- st1.theories.get(node_name)
+ }
+ yield {
+ val theory1 = theory.required(st1.is_required(node_name))
+ val edits = theory1.node_edits(Some(theory))
+ (edits, (node_name, theory1))
+ }
+ session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
+ st1.update_theories(theory_edits.map(_._2))
+ }
+
+ def purge_theories(session: Session, nodes: List[Document.Node.Name])
+ : ((List[Document.Node.Name], List[Document.Node.Name]), State) =
+ {
+ val all_nodes = theory_graph.topological_order
+ val purge = nodes.filterNot(is_required(_)).toSet
+
+ val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
+ val (retained, purged) = all_nodes.partition(retain)
+
+ val purge_edits = purged.flatMap(name => theories(name).purge_edits)
+ session.update(Document.Blobs.empty, purge_edits)
+
+ ((purged, retained), remove_theories(purged))
+ }
+
+ def frontier_theories(clean: Set[Document.Node.Name]): Set[Document.Node.Name] =
+ {
+ @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name])
+ : Set[Document.Node.Name] =
+ {
+ val add = base.filter(b => theory_graph.imm_succs(b).forall(front))
+ if (add.isEmpty) front
+ else {
+ val pre_add = add.map(theory_graph.imm_preds)
+ val base1 = (pre_add.head /: pre_add.tail)(_ ++ _).toList.filter(clean)
+ frontier(base1, front ++ add)
+ }
+ }
+ frontier(theory_graph.maximals.filter(clean), Set.empty)
+ }
+ }
+ }
+
+ class Resources(session_base: Sessions.Base, log: Logger = No_Logger)
+ extends isabelle.Resources(session_base, log = log)
+ {
+ resources =>
+
+ private val state = Synchronized(Resources.State())
+
+ def load_theories(
+ session: Session,
+ id: UUID,
+ dep_theories: List[Document.Node.Name],
+ progress: Progress)
+ {
+ val loaded_theories =
+ for (node_name <- dep_theories)
+ yield {
+ val path = node_name.path
+ if (!node_name.is_theory) error("Not a theory file: " + path)
+
+ progress.expose_interrupt()
+ val text = File.read(path)
+ val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
+ new Resources.Theory(node_name, node_header, text, true)
+ }
+
+ val loaded = loaded_theories.length
+ if (loaded > 1) progress.echo("Loading " + loaded + " theories ...")
+
+ state.change(st =>
+ {
+ val st1 = st.insert_required(id, dep_theories)
+ val theory_edits =
+ for (theory <- loaded_theories)
+ yield {
+ val node_name = theory.node_name
+ val theory1 = theory.required(st1.is_required(node_name))
+ val edits = theory1.node_edits(st1.theories.get(node_name))
+ (edits, (node_name, theory1))
+ }
+ session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
+ st1.update_theories(theory_edits.map(_._2))
+ })
+ }
+
+ def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
+ {
+ state.change(_.unload_theories(session, id, dep_theories))
+ }
+
+ def clean_theories(session: Session, id: UUID, clean: Set[Document.Node.Name])
+ {
+ state.change(st =>
+ {
+ val frontier = st.frontier_theories(clean).toList
+ if (frontier.isEmpty) st
+ else {
+ val st1 = st.unload_theories(session, id, frontier)
+ val (_, st2) = st1.purge_theories(session, frontier)
+ st2
+ }
+ })
+ }
+
+ def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
+ : (List[Document.Node.Name], List[Document.Node.Name]) =
+ {
+ state.change_result(st => st.purge_theories(session, nodes getOrElse st.theory_graph.keys))
+ }
+ }
+}
--- a/src/Pure/Thy/thy_resources.scala Mon Sep 17 22:11:12 2018 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,511 +0,0 @@
-/* Title: Pure/Thy/thy_resources.scala
- Author: Makarius
-
-PIDE resources for theory files: load/unload theories via PIDE document updates.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-import scala.annotation.tailrec
-
-
-object Thy_Resources
-{
- /* PIDE session */
-
- def start_session(
- options: Options,
- session_name: String,
- session_dirs: List[Path] = Nil,
- include_sessions: List[String] = Nil,
- session_base: Option[Sessions.Base] = None,
- print_mode: List[String] = Nil,
- progress: Progress = No_Progress,
- log: Logger = No_Logger): Session =
- {
- val base =
- session_base getOrElse
- Sessions.base_info(options, session_name, include_sessions = include_sessions,
- progress = progress, dirs = session_dirs).check_base
- val resources = new Thy_Resources(base, log = log)
- val session = new Session(session_name, options, resources)
-
- val session_error = Future.promise[String]
- var session_phase: Session.Consumer[Session.Phase] = null
- session_phase =
- Session.Consumer(getClass.getName) {
- case Session.Ready =>
- session.phase_changed -= session_phase
- session_error.fulfill("")
- case Session.Terminated(result) if !result.ok =>
- session.phase_changed -= session_phase
- session_error.fulfill("Session start failed: return code " + result.rc)
- case _ =>
- }
- session.phase_changed += session_phase
-
- progress.echo("Starting session " + session_name + " ...")
- Isabelle_Process.start(session, options,
- logic = session_name, dirs = session_dirs, modes = print_mode)
-
- session_error.join match {
- case "" => session
- case msg => session.stop(); error(msg)
- }
- }
-
- private def stable_snapshot(
- state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
- {
- val snapshot = state.snapshot(name)
- assert(version.id == snapshot.version.id)
- snapshot
- }
-
- class Theories_Result private[Thy_Resources](
- val state: Document.State,
- val version: Document.Version,
- val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
- val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
- {
- def snapshot(name: Document.Node.Name): Document.Snapshot =
- stable_snapshot(state, version, name)
-
- def ok: Boolean =
- (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
- }
-
- val default_check_delay = Time.seconds(0.5)
- val default_nodes_status_delay = Time.seconds(-1.0)
- val default_commit_cleanup_delay = Time.seconds(60.0)
- val default_watchdog_timeout = Time.seconds(600.0)
-
-
- class Session private[Thy_Resources](
- session_name: String,
- session_options: Options,
- override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
- {
- session =>
-
-
- /* temporary directory */
-
- val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
- val tmp_dir_name: String = File.path(tmp_dir).implode
-
- def master_directory(master_dir: String): String =
- proper_string(master_dir) getOrElse tmp_dir_name
-
- override def toString: String = session_name
-
- override def stop(): Process_Result =
- {
- try { super.stop() }
- finally { Isabelle_System.rm_tree(tmp_dir) }
- }
-
-
- /* theories */
-
- private sealed case class Use_Theories_State(
- last_update: Time = Time.now(),
- nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
- already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
- result: Promise[Theories_Result] = Future.promise[Theories_Result])
- {
- def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
- copy(last_update = Time.now(), nodes_status = new_nodes_status)
-
- def watchdog(watchdog_timeout: Time): Boolean =
- watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
-
- def cancel_result { result.cancel }
- def finished_result: Boolean = result.is_finished
- def await_result { result.join_result }
- def join_result: Theories_Result = result.join
- def check_result(
- state: Document.State,
- version: Document.Version,
- dep_theories: List[Document.Node.Name],
- beyond_limit: Boolean,
- watchdog_timeout: Time,
- commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
- : Use_Theories_State =
- {
- val st1 =
- if (commit.isDefined) {
- val already_committed1 =
- (already_committed /: dep_theories)({ case (committed, name) =>
- def parents_committed: Boolean =
- version.nodes(name).header.imports.forall({ case (parent, _) =>
- Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
- })
- if (!committed.isDefinedAt(name) && parents_committed &&
- state.node_consolidated(version, name))
- {
- val snapshot = stable_snapshot(state, version, name)
- val status = Document_Status.Node_Status.make(state, version, name)
- commit.get.apply(snapshot, status)
- committed + (name -> status)
- }
- else committed
- })
- copy(already_committed = already_committed1)
- }
- else this
-
- if (beyond_limit || watchdog(watchdog_timeout) ||
- dep_theories.forall(name =>
- already_committed.isDefinedAt(name) ||
- state.node_consolidated(version, name) ||
- nodes_status.quasi_consolidated(name)))
- {
- val nodes =
- for (name <- dep_theories)
- yield { (name -> Document_Status.Node_Status.make(state, version, name)) }
- val nodes_committed =
- for {
- name <- dep_theories
- status <- already_committed.get(name)
- } yield (name -> status)
-
- try { result.fulfill(new Theories_Result(state, version, nodes, nodes_committed)) }
- catch { case _: IllegalStateException => }
- }
-
- st1
- }
- }
-
- def use_theories(
- theories: List[String],
- qualifier: String = Sessions.DRAFT,
- master_dir: String = "",
- check_delay: Time = default_check_delay,
- check_limit: Int = 0,
- watchdog_timeout: Time = default_watchdog_timeout,
- nodes_status_delay: Time = default_nodes_status_delay,
- id: UUID = UUID(),
- // commit: must not block, must not fail
- commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
- commit_cleanup_delay: Time = default_commit_cleanup_delay,
- progress: Progress = No_Progress): Theories_Result =
- {
- val dep_theories =
- {
- val import_names =
- theories.map(thy =>
- resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none)
- resources.dependencies(import_names, progress = progress).check_errors.theories
- }
-
- val use_theories_state = Synchronized(Use_Theories_State())
-
- def check_result(beyond_limit: Boolean = false)
- {
- val state = session.current_state()
- state.stable_tip_version match {
- case Some(version) =>
- use_theories_state.change(
- _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit))
- case None =>
- }
- }
-
- val check_progress =
- {
- var check_count = 0
- Event_Timer.request(Time.now(), repeat = Some(check_delay))
- {
- if (progress.stopped) use_theories_state.value.cancel_result
- else {
- check_count += 1
- check_result(check_limit > 0 && check_count > check_limit)
- }
- }
- }
-
- val consumer =
- {
- val delay_nodes_status =
- Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
- progress.nodes_status(use_theories_state.value.nodes_status)
- }
-
- val delay_commit_clean =
- Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
- val clean = use_theories_state.value.already_committed.keySet
- resources.clean_theories(session, id, clean)
- }
-
- val dep_theories_set = dep_theories.toSet
-
- Session.Consumer[Session.Commands_Changed](getClass.getName) {
- case changed =>
- if (changed.nodes.exists(dep_theories_set)) {
- val snapshot = session.snapshot()
- val state = snapshot.state
- val version = snapshot.version
-
- val theory_progress =
- use_theories_state.change_result(st =>
- {
- val domain =
- if (st.nodes_status.is_empty) dep_theories_set
- else changed.nodes.iterator.filter(dep_theories_set).toSet
-
- val (nodes_status_changed, nodes_status1) =
- st.nodes_status.update(resources.session_base, state, version,
- domain = Some(domain), trim = changed.assignment)
-
- if (nodes_status_delay >= Time.zero && nodes_status_changed) {
- delay_nodes_status.invoke
- }
-
- val theory_progress =
- (for {
- (name, node_status) <- nodes_status1.present.iterator
- if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
- p1 = node_status.percentage
- if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
- } yield Progress.Theory(name.theory, percentage = Some(p1))).toList
-
- (theory_progress, st.update(nodes_status1))
- })
-
- theory_progress.foreach(progress.theory(_))
-
- check_result()
-
- if (commit.isDefined && commit_cleanup_delay > Time.zero) {
- if (use_theories_state.value.finished_result)
- delay_commit_clean.revoke
- else delay_commit_clean.invoke
- }
- }
- }
- }
-
- try {
- session.commands_changed += consumer
- resources.load_theories(session, id, dep_theories, progress)
- use_theories_state.value.await_result
- check_progress.cancel
- }
- finally {
- session.commands_changed -= consumer
- resources.unload_theories(session, id, dep_theories)
- }
-
- use_theories_state.value.join_result
- }
-
- def purge_theories(
- theories: List[String],
- qualifier: String = Sessions.DRAFT,
- master_dir: String = "",
- all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
- {
- val nodes =
- if (all) None
- else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _)))
- resources.purge_theories(session, nodes)
- }
- }
-
-
- /* internal state */
-
- final class Theory private[Thy_Resources](
- val node_name: Document.Node.Name,
- val node_header: Document.Node.Header,
- val text: String,
- val node_required: Boolean)
- {
- override def toString: String = node_name.toString
-
- def node_perspective: Document.Node.Perspective_Text =
- Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
-
- def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
- List(node_name -> Document.Node.Deps(node_header),
- node_name -> Document.Node.Edits(text_edits),
- node_name -> node_perspective)
-
- def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
- {
- val (text_edits, old_required) =
- if (old.isEmpty) (Text.Edit.inserts(0, text), false)
- else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
-
- if (text_edits.isEmpty && node_required == old_required) Nil
- else make_edits(text_edits)
- }
-
- def purge_edits: List[Document.Edit_Text] =
- make_edits(Text.Edit.removes(0, text))
-
- def required(required: Boolean): Theory =
- if (required == node_required) this
- else new Theory(node_name, node_header, text, required)
- }
-
- sealed case class State(
- required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
- theories: Map[Document.Node.Name, Theory] = Map.empty)
- {
- lazy val theory_graph: Graph[Document.Node.Name, Unit] =
- {
- val entries =
- for ((name, theory) <- theories.toList)
- yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
- Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
- }
-
- def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
-
- def insert_required(id: UUID, names: List[Document.Node.Name]): State =
- copy(required = (required /: names)(_.insert(_, id)))
-
- def remove_required(id: UUID, names: List[Document.Node.Name]): State =
- copy(required = (required /: names)(_.remove(_, id)))
-
- def update_theories(update: List[(Document.Node.Name, Theory)]): State =
- copy(theories =
- (theories /: update)({ case (thys, (name, thy)) =>
- thys.get(name) match {
- case Some(thy1) if thy1 == thy => thys
- case _ => thys + (name -> thy)
- }
- }))
-
- def remove_theories(remove: List[Document.Node.Name]): State =
- {
- require(remove.forall(name => !is_required(name)))
- copy(theories = theories -- remove)
- }
-
- def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name]): State =
- {
- val st1 = remove_required(id, dep_theories)
- val theory_edits =
- for {
- node_name <- dep_theories
- theory <- st1.theories.get(node_name)
- }
- yield {
- val theory1 = theory.required(st1.is_required(node_name))
- val edits = theory1.node_edits(Some(theory))
- (edits, (node_name, theory1))
- }
- session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
- st1.update_theories(theory_edits.map(_._2))
- }
-
- def purge_theories(session: Session, nodes: List[Document.Node.Name])
- : ((List[Document.Node.Name], List[Document.Node.Name]), State) =
- {
- val all_nodes = theory_graph.topological_order
- val purge = nodes.filterNot(is_required(_)).toSet
-
- val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
- val (retained, purged) = all_nodes.partition(retain)
-
- val purge_edits = purged.flatMap(name => theories(name).purge_edits)
- session.update(Document.Blobs.empty, purge_edits)
-
- ((purged, retained), remove_theories(purged))
- }
-
- def frontier_theories(clean: Set[Document.Node.Name]): Set[Document.Node.Name] =
- {
- @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name])
- : Set[Document.Node.Name] =
- {
- val add = base.filter(b => theory_graph.imm_succs(b).forall(front))
- if (add.isEmpty) front
- else {
- val pre_add = add.map(theory_graph.imm_preds)
- val base1 = (pre_add.head /: pre_add.tail)(_ ++ _).toList.filter(clean)
- frontier(base1, front ++ add)
- }
- }
- frontier(theory_graph.maximals.filter(clean), Set.empty)
- }
- }
-}
-
-class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
- extends Resources(session_base, log = log)
-{
- resources =>
-
- private val state = Synchronized(Thy_Resources.State())
-
- def load_theories(
- session: Session,
- id: UUID,
- dep_theories: List[Document.Node.Name],
- progress: Progress)
- {
- val loaded_theories =
- for (node_name <- dep_theories)
- yield {
- val path = node_name.path
- if (!node_name.is_theory) error("Not a theory file: " + path)
-
- progress.expose_interrupt()
- val text = File.read(path)
- val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
- new Thy_Resources.Theory(node_name, node_header, text, true)
- }
-
- val loaded = loaded_theories.length
- if (loaded > 1) progress.echo("Loading " + loaded + " theories ...")
-
- state.change(st =>
- {
- val st1 = st.insert_required(id, dep_theories)
- val theory_edits =
- for (theory <- loaded_theories)
- yield {
- val node_name = theory.node_name
- val theory1 = theory.required(st1.is_required(node_name))
- val edits = theory1.node_edits(st1.theories.get(node_name))
- (edits, (node_name, theory1))
- }
- session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
- st1.update_theories(theory_edits.map(_._2))
- })
- }
-
- def unload_theories(
- session: Thy_Resources.Session, id: UUID, dep_theories: List[Document.Node.Name])
- {
- state.change(_.unload_theories(session, id, dep_theories))
- }
-
- def clean_theories(session: Thy_Resources.Session, id: UUID, clean: Set[Document.Node.Name])
- {
- state.change(st =>
- {
- val frontier = st.frontier_theories(clean).toList
- if (frontier.isEmpty) st
- else {
- val st1 = st.unload_theories(session, id, frontier)
- val (_, st2) = st1.purge_theories(session, frontier)
- st2
- }
- })
- }
-
- def purge_theories(session: Thy_Resources.Session, nodes: Option[List[Document.Node.Name]])
- : (List[Document.Node.Name], List[Document.Node.Name]) =
- {
- state.change_result(st => st.purge_theories(session, nodes getOrElse st.theory_graph.keys))
- }
-}
--- a/src/Pure/Tools/dump.scala Mon Sep 17 22:11:12 2018 +0200
+++ b/src/Pure/Tools/dump.scala Tue Sep 18 11:05:14 2018 +0200
@@ -92,8 +92,8 @@
select_dirs: List[Path] = Nil,
output_dir: Path = default_output_dir,
verbose: Boolean = false,
- commit_cleanup_delay: Time = Thy_Resources.default_commit_cleanup_delay,
- watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
+ commit_cleanup_delay: Time = Headless.default_commit_cleanup_delay,
+ watchdog_timeout: Time = Headless.default_watchdog_timeout,
system_mode: Boolean = false,
selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
{
@@ -155,7 +155,7 @@
/* session */
val session =
- Thy_Resources.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
+ Headless.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
include_sessions = include_sessions, progress = progress, log = log)
val theories_result =
@@ -181,11 +181,11 @@
{
var aspects: List[Aspect] = known_aspects
var base_sessions: List[String] = Nil
- var commit_cleanup_delay = Thy_Resources.default_commit_cleanup_delay
+ var commit_cleanup_delay = Headless.default_commit_cleanup_delay
var select_dirs: List[Path] = Nil
var output_dir = default_output_dir
var requirements = false
- var watchdog_timeout = Thy_Resources.default_watchdog_timeout
+ var watchdog_timeout = Headless.default_watchdog_timeout
var exclude_session_groups: List[String] = Nil
var all_sessions = false
var dirs: List[Path] = Nil
@@ -203,12 +203,12 @@
-A NAMES dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
-B NAME include session NAME and all descendants
-C SECONDS delay for cleaning of already dumped theories (0 = disabled, default: """ +
- Value.Seconds(Thy_Resources.default_commit_cleanup_delay) + """)
+ Value.Seconds(Headless.default_commit_cleanup_delay) + """)
-D DIR include session directory and select its sessions
-O DIR output directory for dumped files (default: """ + default_output_dir + """)
-R operate on requirements of selected sessions
-W SECONDS watchdog timeout for PIDE processing (0 = disabled, default: """ +
- Value.Seconds(Thy_Resources.default_watchdog_timeout) + """)
+ Value.Seconds(Headless.default_watchdog_timeout) + """)
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-d DIR include session directory
--- a/src/Pure/Tools/server.scala Mon Sep 17 22:11:12 2018 +0200
+++ b/src/Pure/Tools/server.scala Tue Sep 18 11:05:14 2018 +0200
@@ -506,12 +506,11 @@
private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
- private val _sessions = Synchronized(Map.empty[UUID, Thy_Resources.Session])
+ private val _sessions = Synchronized(Map.empty[UUID, Headless.Session])
def err_session(id: UUID): Nothing = error("No session " + Library.single_quote(id.toString))
- def the_session(id: UUID): Thy_Resources.Session =
- _sessions.value.get(id) getOrElse err_session(id)
- def add_session(entry: (UUID, Thy_Resources.Session)) { _sessions.change(_ + entry) }
- def remove_session(id: UUID): Thy_Resources.Session =
+ def the_session(id: UUID): Headless.Session = _sessions.value.get(id) getOrElse err_session(id)
+ def add_session(entry: (UUID, Headless.Session)) { _sessions.change(_ + entry) }
+ def remove_session(id: UUID): Headless.Session =
{
_sessions.change_result(sessions =>
sessions.get(id) match {
--- a/src/Pure/Tools/server_commands.scala Mon Sep 17 22:11:12 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala Tue Sep 18 11:05:14 2018 +0200
@@ -107,14 +107,14 @@
yield Args(build = build, print_mode = print_mode)
def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
- : (JSON.Object.T, (UUID, Thy_Resources.Session)) =
+ : (JSON.Object.T, (UUID, Headless.Session)) =
{
val base_info =
try { Session_Build.command(args.build, progress = progress)._3 }
catch { case exn: Server.Error => error(exn.message) }
val session =
- Thy_Resources.start_session(
+ Headless.start_session(
base_info.options,
base_info.session,
session_dirs = base_info.dirs,
@@ -139,7 +139,7 @@
def unapply(json: JSON.T): Option[UUID] =
JSON.uuid(json, "session_id")
- def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) =
+ def command(session: Headless.Session): (JSON.Object.T, Process_Result) =
{
val result = session.stop()
val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
@@ -158,10 +158,10 @@
pretty_margin: Double = Pretty.default_margin,
unicode_symbols: Boolean = false,
export_pattern: String = "",
- check_delay: Time = Thy_Resources.default_check_delay,
+ check_delay: Time = Headless.default_check_delay,
check_limit: Int = 0,
- watchdog_timeout: Time = Thy_Resources.default_watchdog_timeout,
- nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay)
+ watchdog_timeout: Time = Headless.default_watchdog_timeout,
+ nodes_status_delay: Time = Headless.default_nodes_status_delay)
def unapply(json: JSON.T): Option[Args] =
for {
@@ -171,12 +171,12 @@
pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
export_pattern <- JSON.string_default(json, "export_pattern")
- check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay)
+ check_delay <- JSON.seconds_default(json, "check_delay", Headless.default_check_delay)
check_limit <- JSON.int_default(json, "check_limit")
watchdog_timeout <-
- JSON.seconds_default(json, "watchdog_timeout", Thy_Resources.default_watchdog_timeout)
+ JSON.seconds_default(json, "watchdog_timeout", Headless.default_watchdog_timeout)
nodes_status_delay <-
- JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
+ JSON.seconds_default(json, "nodes_status_delay", Headless.default_nodes_status_delay)
}
yield {
Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
@@ -186,9 +186,9 @@
}
def command(args: Args,
- session: Thy_Resources.Session,
+ session: Headless.Session,
id: UUID = UUID(),
- progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) =
+ progress: Progress = No_Progress): (JSON.Object.T, Headless.Theories_Result) =
{
val result =
session.use_theories(args.theories, master_dir = args.master_dir,
@@ -263,7 +263,7 @@
}
yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }
- def command(args: Args, session: Thy_Resources.Session)
+ def command(args: Args, session: Headless.Session)
: (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) =
{
val (purged, retained) =
--- a/src/Pure/build-jars Mon Sep 17 22:11:12 2018 +0200
+++ b/src/Pure/build-jars Tue Sep 18 11:05:14 2018 +0200
@@ -95,6 +95,7 @@
PIDE/document_id.scala
PIDE/document_status.scala
PIDE/editor.scala
+ PIDE/headless.scala
PIDE/line.scala
PIDE/markup.scala
PIDE/markup_tree.scala
@@ -137,7 +138,6 @@
Thy/sessions.scala
Thy/thy_element.scala
Thy/thy_header.scala
- Thy/thy_resources.scala
Thy/thy_syntax.scala
Tools/dump.scala
Tools/build.scala