src/Pure/PIDE/headless.scala
author wenzelm
Tue, 18 Sep 2018 11:05:14 +0200
changeset 69012 c91d14ab065f
parent 68986 src/Pure/Thy/thy_resources.scala@22f02724e7d1
child 69013 bb4e4c253ebe
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
     1
/*  Title:      Pure/PIDE/headless.scala
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     3
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
     4
Headless PIDE session and resources from file-system.
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     5
*/
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     6
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     7
package isabelle
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     8
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     9
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    10
import java.io.{File => JFile}
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    11
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
    12
import scala.annotation.tailrec
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
    13
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    14
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
    15
object Headless
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    16
{
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
    17
  /** session **/
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    18
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    19
  def start_session(
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    20
    options: Options,
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    21
    session_name: String,
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    22
    session_dirs: List[Path] = Nil,
67948
83902fff6243 clarified signature;
wenzelm
parents: 67946
diff changeset
    23
    include_sessions: List[String] = Nil,
67062
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    24
    session_base: Option[Sessions.Base] = None,
67869
8cb4fef58379 support for "session_start";
wenzelm
parents: 67852
diff changeset
    25
    print_mode: List[String] = Nil,
8cb4fef58379 support for "session_start";
wenzelm
parents: 67852
diff changeset
    26
    progress: Progress = No_Progress,
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    27
    log: Logger = No_Logger): Session =
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    28
  {
67062
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    29
    val base =
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    30
      session_base getOrElse
67948
83902fff6243 clarified signature;
wenzelm
parents: 67946
diff changeset
    31
        Sessions.base_info(options, session_name, include_sessions = include_sessions,
83902fff6243 clarified signature;
wenzelm
parents: 67946
diff changeset
    32
          progress = progress, dirs = session_dirs).check_base
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
    33
    val resources = new Resources(base, log = log)
67945
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
    34
    val session = new Session(session_name, options, resources)
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    35
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    36
    val session_error = Future.promise[String]
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    37
    var session_phase: Session.Consumer[Session.Phase] = null
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    38
    session_phase =
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    39
      Session.Consumer(getClass.getName) {
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    40
        case Session.Ready =>
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    41
          session.phase_changed -= session_phase
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    42
          session_error.fulfill("")
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    43
        case Session.Terminated(result) if !result.ok =>
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    44
          session.phase_changed -= session_phase
67869
8cb4fef58379 support for "session_start";
wenzelm
parents: 67852
diff changeset
    45
          session_error.fulfill("Session start failed: return code " + result.rc)
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    46
        case _ =>
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    47
      }
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    48
    session.phase_changed += session_phase
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    49
68986
22f02724e7d1 tuned message;
wenzelm
parents: 68981
diff changeset
    50
    progress.echo("Starting session " + session_name + " ...")
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    51
    Isabelle_Process.start(session, options,
67869
8cb4fef58379 support for "session_start";
wenzelm
parents: 67852
diff changeset
    52
      logic = session_name, dirs = session_dirs, modes = print_mode)
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    53
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    54
    session_error.join match {
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    55
      case "" => session
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    56
      case msg => session.stop(); error(msg)
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    57
    }
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    58
  }
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    59
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    60
  private def stable_snapshot(
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    61
    state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    62
  {
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    63
    val snapshot = state.snapshot(name)
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    64
    assert(version.id == snapshot.version.id)
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    65
    snapshot
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    66
  }
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    67
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
    68
  class Theories_Result private[Headless](
67883
171e7735ce25 support for "use_theories";
wenzelm
parents: 67881
diff changeset
    69
    val state: Document.State,
67889
wenzelm
parents: 67888
diff changeset
    70
    val version: Document.Version,
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    71
    val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    72
    val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
67879
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
    73
  {
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    74
    def snapshot(name: Document.Node.Name): Document.Snapshot =
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    75
      stable_snapshot(state, version, name)
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    76
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    77
    def ok: Boolean =
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    78
      (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
67879
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
    79
  }
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
    80
68943
e564605d4cac tuned signature;
wenzelm
parents: 68936
diff changeset
    81
  val default_check_delay = Time.seconds(0.5)
e564605d4cac tuned signature;
wenzelm
parents: 68936
diff changeset
    82
  val default_nodes_status_delay = Time.seconds(-1.0)
68981
30daac7848b9 tuned signature;
wenzelm
parents: 68962
diff changeset
    83
  val default_commit_cleanup_delay = Time.seconds(60.0)
68947
ea804c814693 clarified defaults;
wenzelm
parents: 68943
diff changeset
    84
  val default_watchdog_timeout = Time.seconds(600.0)
68694
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
    85
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
    86
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
    87
  class Session private[Headless](
67945
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
    88
    session_name: String,
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
    89
    session_options: Options,
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
    90
    override val resources: Resources) extends isabelle.Session(session_options, resources)
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    91
  {
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    92
    session =>
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    93
68922
wenzelm
parents: 68916
diff changeset
    94
wenzelm
parents: 68916
diff changeset
    95
    /* temporary directory */
wenzelm
parents: 68916
diff changeset
    96
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    97
    val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
67946
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
    98
    val tmp_dir_name: String = File.path(tmp_dir).implode
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    99
68923
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   100
    def master_directory(master_dir: String): String =
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   101
      proper_string(master_dir) getOrElse tmp_dir_name
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   102
67945
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
   103
    override def toString: String = session_name
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
   104
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   105
    override def stop(): Process_Result =
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   106
    {
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   107
      try { super.stop() }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   108
      finally { Isabelle_System.rm_tree(tmp_dir) }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   109
    }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   110
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   111
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   112
    /* theories */
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   113
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   114
    private sealed case class Use_Theories_State(
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   115
      last_update: Time = Time.now(),
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   116
      nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   117
      already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   118
      result: Promise[Theories_Result] = Future.promise[Theories_Result])
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   119
    {
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   120
      def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   121
        copy(last_update = Time.now(), nodes_status = new_nodes_status)
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   122
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   123
      def watchdog(watchdog_timeout: Time): Boolean =
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   124
        watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   125
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   126
      def cancel_result { result.cancel }
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   127
      def finished_result: Boolean = result.is_finished
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   128
      def await_result { result.join_result }
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   129
      def join_result: Theories_Result = result.join
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   130
      def check_result(
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   131
          state: Document.State,
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   132
          version: Document.Version,
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   133
          dep_theories: List[Document.Node.Name],
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   134
          beyond_limit: Boolean,
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   135
          watchdog_timeout: Time,
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   136
          commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   137
        : Use_Theories_State =
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   138
      {
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   139
        val st1 =
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   140
          if (commit.isDefined) {
68949
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   141
            val already_committed1 =
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   142
              (already_committed /: dep_theories)({ case (committed, name) =>
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   143
                def parents_committed: Boolean =
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   144
                  version.nodes(name).header.imports.forall({ case (parent, _) =>
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   145
                    Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   146
                  })
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   147
                if (!committed.isDefinedAt(name) && parents_committed &&
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   148
                    state.node_consolidated(version, name))
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   149
                {
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   150
                  val snapshot = stable_snapshot(state, version, name)
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   151
                  val status = Document_Status.Node_Status.make(state, version, name)
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   152
                  commit.get.apply(snapshot, status)
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   153
                  committed + (name -> status)
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   154
                }
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   155
                else committed
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   156
              })
e848328cb2c1 ensure foundational order of commits, taking Pure as implicit starting point;
wenzelm
parents: 68947
diff changeset
   157
            copy(already_committed = already_committed1)
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   158
          }
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   159
          else this
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   160
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   161
        if (beyond_limit || watchdog(watchdog_timeout) ||
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   162
          dep_theories.forall(name =>
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   163
            already_committed.isDefinedAt(name) ||
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   164
            state.node_consolidated(version, name) ||
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   165
            nodes_status.quasi_consolidated(name)))
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   166
        {
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   167
          val nodes =
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   168
            for (name <- dep_theories)
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   169
            yield { (name -> Document_Status.Node_Status.make(state, version, name)) }
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   170
          val nodes_committed =
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   171
            for {
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   172
              name <- dep_theories
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   173
              status <- already_committed.get(name)
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   174
            } yield (name -> status)
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   175
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   176
          try { result.fulfill(new Theories_Result(state, version, nodes, nodes_committed)) }
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   177
          catch { case _: IllegalStateException => }
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   178
        }
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   179
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   180
        st1
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   181
      }
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   182
    }
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   183
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   184
    def use_theories(
67940
b4e80f062fbf clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents: 67939
diff changeset
   185
      theories: List[String],
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   186
      qualifier: String = Sessions.DRAFT,
67881
812ed06dadec interruptible exploration of dependencies;
wenzelm
parents: 67879
diff changeset
   187
      master_dir: String = "",
68943
e564605d4cac tuned signature;
wenzelm
parents: 68936
diff changeset
   188
      check_delay: Time = default_check_delay,
68694
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   189
      check_limit: Int = 0,
68947
ea804c814693 clarified defaults;
wenzelm
parents: 68943
diff changeset
   190
      watchdog_timeout: Time = default_watchdog_timeout,
68943
e564605d4cac tuned signature;
wenzelm
parents: 68936
diff changeset
   191
      nodes_status_delay: Time = default_nodes_status_delay,
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   192
      id: UUID = UUID(),
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   193
      // commit: must not block, must not fail
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   194
      commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
68981
30daac7848b9 tuned signature;
wenzelm
parents: 68962
diff changeset
   195
      commit_cleanup_delay: Time = default_commit_cleanup_delay,
67881
812ed06dadec interruptible exploration of dependencies;
wenzelm
parents: 67879
diff changeset
   196
      progress: Progress = No_Progress): Theories_Result =
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   197
    {
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   198
      val dep_theories =
68894
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   199
      {
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   200
        val import_names =
68923
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   201
          theories.map(thy =>
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   202
            resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none)
68894
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   203
        resources.dependencies(import_names, progress = progress).check_errors.theories
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   204
      }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   205
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   206
      val use_theories_state = Synchronized(Use_Theories_State())
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   207
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   208
      def check_result(beyond_limit: Boolean = false)
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   209
      {
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   210
        val state = session.current_state()
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   211
        state.stable_tip_version match {
68694
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   212
          case Some(version) =>
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   213
            use_theories_state.change(
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   214
              _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit))
68694
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   215
          case None =>
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   216
        }
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   217
      }
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   218
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   219
      val check_progress =
68694
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   220
      {
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   221
        var check_count = 0
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   222
        Event_Timer.request(Time.now(), repeat = Some(check_delay))
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   223
          {
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   224
            if (progress.stopped) use_theories_state.value.cancel_result
68694
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   225
            else {
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   226
              check_count += 1
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   227
              check_result(check_limit > 0 && check_count > check_limit)
68694
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   228
            }
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   229
          }
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   230
      }
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   231
68906
wenzelm
parents: 68905
diff changeset
   232
      val consumer =
wenzelm
parents: 68905
diff changeset
   233
      {
wenzelm
parents: 68905
diff changeset
   234
        val delay_nodes_status =
wenzelm
parents: 68905
diff changeset
   235
          Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   236
            progress.nodes_status(use_theories_state.value.nodes_status)
68906
wenzelm
parents: 68905
diff changeset
   237
          }
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   238
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   239
        val delay_commit_clean =
68981
30daac7848b9 tuned signature;
wenzelm
parents: 68962
diff changeset
   240
          Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   241
            val clean = use_theories_state.value.already_committed.keySet
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   242
            resources.clean_theories(session, id, clean)
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   243
          }
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   244
68952
wenzelm
parents: 68951
diff changeset
   245
        val dep_theories_set = dep_theories.toSet
wenzelm
parents: 68951
diff changeset
   246
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   247
        Session.Consumer[Session.Commands_Changed](getClass.getName) {
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   248
          case changed =>
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   249
            if (changed.nodes.exists(dep_theories_set)) {
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   250
              val snapshot = session.snapshot()
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   251
              val state = snapshot.state
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   252
              val version = snapshot.version
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   253
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68952
diff changeset
   254
              val theory_progress =
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   255
                use_theories_state.change_result(st =>
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   256
                  {
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   257
                    val domain =
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   258
                      if (st.nodes_status.is_empty) dep_theories_set
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   259
                      else changed.nodes.iterator.filter(dep_theories_set).toSet
68899
b15b03c13dbb more detailed progress;
wenzelm
parents: 68894
diff changeset
   260
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   261
                    val (nodes_status_changed, nodes_status1) =
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   262
                      st.nodes_status.update(resources.session_base, state, version,
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   263
                        domain = Some(domain), trim = changed.assignment)
68899
b15b03c13dbb more detailed progress;
wenzelm
parents: 68894
diff changeset
   264
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   265
                    if (nodes_status_delay >= Time.zero && nodes_status_changed) {
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   266
                      delay_nodes_status.invoke
68899
b15b03c13dbb more detailed progress;
wenzelm
parents: 68894
diff changeset
   267
                    }
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   268
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68952
diff changeset
   269
                    val theory_progress =
68905
90a6b714aca3 tuned -- prefer immutable data;
wenzelm
parents: 68904
diff changeset
   270
                      (for {
68904
09151c54aaac tuned signature;
wenzelm
parents: 68903
diff changeset
   271
                        (name, node_status) <- nodes_status1.present.iterator
68959
d4223afddd47 clarified message;
wenzelm
parents: 68958
diff changeset
   272
                        if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
68962
50676b0ab970 tuned message (again);
wenzelm
parents: 68959
diff changeset
   273
                        p1 = node_status.percentage
50676b0ab970 tuned message (again);
wenzelm
parents: 68959
diff changeset
   274
                        if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
50676b0ab970 tuned message (again);
wenzelm
parents: 68959
diff changeset
   275
                      } yield Progress.Theory(name.theory, percentage = Some(p1))).toList
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   276
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68952
diff changeset
   277
                    (theory_progress, st.update(nodes_status1))
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   278
                  })
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   279
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68952
diff changeset
   280
              theory_progress.foreach(progress.theory(_))
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   281
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   282
              check_result()
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   283
68981
30daac7848b9 tuned signature;
wenzelm
parents: 68962
diff changeset
   284
              if (commit.isDefined && commit_cleanup_delay > Time.zero) {
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   285
                if (use_theories_state.value.finished_result)
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   286
                  delay_commit_clean.revoke
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   287
                else delay_commit_clean.invoke
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   288
              }
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   289
            }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   290
        }
68906
wenzelm
parents: 68905
diff changeset
   291
      }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   292
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   293
      try {
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   294
        session.commands_changed += consumer
68894
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   295
        resources.load_theories(session, id, dep_theories, progress)
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   296
        use_theories_state.value.await_result
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   297
        check_progress.cancel
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   298
      }
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   299
      finally {
68907
wenzelm
parents: 68906
diff changeset
   300
        session.commands_changed -= consumer
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   301
        resources.unload_theories(session, id, dep_theories)
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   302
      }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   303
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   304
      use_theories_state.value.join_result
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   305
    }
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   306
67939
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   307
    def purge_theories(
68915
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   308
      theories: List[String],
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   309
      qualifier: String = Sessions.DRAFT,
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   310
      master_dir: String = "",
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   311
      all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   312
    {
68923
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   313
      val nodes =
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   314
        if (all) None
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   315
        else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _)))
68915
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   316
      resources.purge_theories(session, nodes)
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   317
    }
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
   318
  }
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
   319
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
   320
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   321
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   322
  /** resources **/
68922
wenzelm
parents: 68916
diff changeset
   323
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   324
  object Resources
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   325
  {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   326
    final class Theory private[Headless](
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   327
      val node_name: Document.Node.Name,
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   328
      val node_header: Document.Node.Header,
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   329
      val text: String,
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   330
      val node_required: Boolean)
68922
wenzelm
parents: 68916
diff changeset
   331
    {
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   332
      override def toString: String = node_name.toString
68922
wenzelm
parents: 68916
diff changeset
   333
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   334
      def node_perspective: Document.Node.Perspective_Text =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   335
        Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
68922
wenzelm
parents: 68916
diff changeset
   336
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   337
      def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   338
        List(node_name -> Document.Node.Deps(node_header),
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   339
          node_name -> Document.Node.Edits(text_edits),
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   340
          node_name -> node_perspective)
68922
wenzelm
parents: 68916
diff changeset
   341
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   342
      def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   343
      {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   344
        val (text_edits, old_required) =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   345
          if (old.isEmpty) (Text.Edit.inserts(0, text), false)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   346
          else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   347
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   348
        if (text_edits.isEmpty && node_required == old_required) Nil
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   349
        else make_edits(text_edits)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   350
      }
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   351
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   352
      def purge_edits: List[Document.Edit_Text] =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   353
        make_edits(Text.Edit.removes(0, text))
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   354
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   355
      def required(required: Boolean): Theory =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   356
        if (required == node_required) this
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   357
        else new Theory(node_name, node_header, text, required)
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   358
    }
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   359
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   360
    sealed case class State(
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   361
      required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   362
      theories: Map[Document.Node.Name, Theory] = Map.empty)
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   363
    {
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   364
      lazy val theory_graph: Graph[Document.Node.Name, Unit] =
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   365
      {
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   366
        val entries =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   367
          for ((name, theory) <- theories.toList)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   368
          yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   369
        Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
67888
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   370
      }
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   371
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   372
      def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   373
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   374
      def insert_required(id: UUID, names: List[Document.Node.Name]): State =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   375
        copy(required = (required /: names)(_.insert(_, id)))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   376
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   377
      def remove_required(id: UUID, names: List[Document.Node.Name]): State =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   378
        copy(required = (required /: names)(_.remove(_, id)))
68958
9199f9da512a tuned message;
wenzelm
parents: 68957
diff changeset
   379
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   380
      def update_theories(update: List[(Document.Node.Name, Theory)]): State =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   381
        copy(theories =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   382
          (theories /: update)({ case (thys, (name, thy)) =>
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   383
            thys.get(name) match {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   384
              case Some(thy1) if thy1 == thy => thys
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   385
              case _ => thys + (name -> thy)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   386
            }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   387
          }))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   388
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   389
      def remove_theories(remove: List[Document.Node.Name]): State =
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   390
      {
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   391
        require(remove.forall(name => !is_required(name)))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   392
        copy(theories = theories -- remove)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   393
      }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   394
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   395
      def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name]): State =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   396
      {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   397
        val st1 = remove_required(id, dep_theories)
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   398
        val theory_edits =
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   399
          for {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   400
            node_name <- dep_theories
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   401
            theory <- st1.theories.get(node_name)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   402
          }
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   403
          yield {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   404
            val theory1 = theory.required(st1.is_required(node_name))
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   405
            val edits = theory1.node_edits(Some(theory))
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   406
            (edits, (node_name, theory1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   407
          }
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   408
        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   409
        st1.update_theories(theory_edits.map(_._2))
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   410
      }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   411
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   412
      def purge_theories(session: Session, nodes: List[Document.Node.Name])
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   413
        : ((List[Document.Node.Name], List[Document.Node.Name]), State) =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   414
      {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   415
        val all_nodes = theory_graph.topological_order
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   416
        val purge = nodes.filterNot(is_required(_)).toSet
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   417
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   418
        val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   419
        val (retained, purged) = all_nodes.partition(retain)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   420
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   421
        val purge_edits = purged.flatMap(name => theories(name).purge_edits)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   422
        session.update(Document.Blobs.empty, purge_edits)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   423
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   424
        ((purged, retained), remove_theories(purged))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   425
      }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   426
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   427
      def frontier_theories(clean: Set[Document.Node.Name]): Set[Document.Node.Name] =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   428
      {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   429
        @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name])
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   430
          : Set[Document.Node.Name] =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   431
        {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   432
          val add = base.filter(b => theory_graph.imm_succs(b).forall(front))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   433
          if (add.isEmpty) front
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   434
          else {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   435
            val pre_add = add.map(theory_graph.imm_preds)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   436
            val base1 = (pre_add.head /: pre_add.tail)(_ ++ _).toList.filter(clean)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   437
            frontier(base1, front ++ add)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   438
          }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   439
        }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   440
        frontier(theory_graph.maximals.filter(clean), Set.empty)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   441
      }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   442
    }
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   443
  }
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   444
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   445
  class Resources(session_base: Sessions.Base, log: Logger = No_Logger)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   446
    extends isabelle.Resources(session_base, log = log)
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   447
  {
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   448
    resources =>
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   449
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   450
    private val state = Synchronized(Resources.State())
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   451
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   452
    def load_theories(
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   453
      session: Session,
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   454
      id: UUID,
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   455
      dep_theories: List[Document.Node.Name],
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   456
      progress: Progress)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   457
    {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   458
      val loaded_theories =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   459
        for (node_name <- dep_theories)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   460
        yield {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   461
          val path = node_name.path
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   462
          if (!node_name.is_theory) error("Not a theory file: " + path)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   463
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   464
          progress.expose_interrupt()
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   465
          val text = File.read(path)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   466
          val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   467
          new Resources.Theory(node_name, node_header, text, true)
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   468
        }
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   469
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   470
      val loaded = loaded_theories.length
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   471
      if (loaded > 1) progress.echo("Loading " + loaded + " theories ...")
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   472
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   473
      state.change(st =>
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   474
        {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   475
          val st1 = st.insert_required(id, dep_theories)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   476
          val theory_edits =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   477
            for (theory <- loaded_theories)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   478
            yield {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   479
              val node_name = theory.node_name
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   480
              val theory1 = theory.required(st1.is_required(node_name))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   481
              val edits = theory1.node_edits(st1.theories.get(node_name))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   482
              (edits, (node_name, theory1))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   483
            }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   484
          session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   485
          st1.update_theories(theory_edits.map(_._2))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   486
        })
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   487
    }
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   488
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   489
    def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   490
    {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   491
      state.change(_.unload_theories(session, id, dep_theories))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   492
    }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   493
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   494
    def clean_theories(session: Session, id: UUID, clean: Set[Document.Node.Name])
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   495
    {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   496
      state.change(st =>
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   497
        {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   498
          val frontier = st.frontier_theories(clean).toList
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   499
          if (frontier.isEmpty) st
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   500
          else {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   501
            val st1 = st.unload_theories(session, id, frontier)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   502
            val (_, st2) = st1.purge_theories(session, frontier)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   503
            st2
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   504
          }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   505
        })
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   506
    }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   507
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   508
    def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   509
      : (List[Document.Node.Name], List[Document.Node.Name]) =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   510
    {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   511
      state.change_result(st => st.purge_theories(session, nodes getOrElse st.theory_graph.keys))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   512
    }
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   513
  }
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   514
}