src/Pure/PIDE/headless.scala
author wenzelm
Mon, 30 Sep 2019 12:52:16 +0200
changeset 70769 9514fdbb8abe
parent 70768 670bb96096a7
child 70770 8abda6f6b700
permissions -rw-r--r--
clarified incremental loading: requirements based on maximal nodes;
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
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
    13
import scala.collection.mutable
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
    14
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    15
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
    16
object Headless
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    17
{
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
    18
  /** session **/
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    19
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    20
  private def stable_snapshot(
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    21
    state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    22
  {
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    23
    val snapshot = state.snapshot(name)
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    24
    assert(version.id == snapshot.version.id)
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    25
    snapshot
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    26
  }
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
    27
69013
bb4e4c253ebe tuned signature;
wenzelm
parents: 69012
diff changeset
    28
  class Use_Theories_Result private[Headless](
67883
171e7735ce25 support for "use_theories";
wenzelm
parents: 67881
diff changeset
    29
    val state: Document.State,
67889
wenzelm
parents: 67888
diff changeset
    30
    val version: Document.Version,
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    31
    val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    32
    val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
67879
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
    33
  {
69032
90bb4cabe1e8 clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents: 69013
diff changeset
    34
    def nodes_pending: List[(Document.Node.Name, Document_Status.Node_Status)] =
90bb4cabe1e8 clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents: 69013
diff changeset
    35
    {
90bb4cabe1e8 clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents: 69013
diff changeset
    36
      val committed = nodes_committed.iterator.map(_._1).toSet
90bb4cabe1e8 clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents: 69013
diff changeset
    37
      nodes.filter(p => !committed(p._1))
90bb4cabe1e8 clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents: 69013
diff changeset
    38
    }
90bb4cabe1e8 clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents: 69013
diff changeset
    39
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    40
    def snapshot(name: Document.Node.Name): Document.Snapshot =
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    41
      stable_snapshot(state, version, name)
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    42
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    43
    def ok: Boolean =
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
    44
      (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
67879
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
    45
  }
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
    46
70765
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
    47
  private sealed abstract class Load_State
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
    48
  {
70769
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    49
    type Result = (List[Document.Node.Name], Load_State)
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    50
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    51
    def next(dep_graph: Document.Node.Name.Graph[Unit], finished: Document.Node.Name => Boolean)
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    52
      : Result =
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
    53
    {
70769
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    54
      def load_checkpoints(checkpoints: List[Document.Node.Name]): Result =
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    55
        Load_Init(checkpoints).next(dep_graph, finished)
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    56
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    57
      def load_requirements(
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    58
        pending: List[Document.Node.Name], checkpoints: List[Document.Node.Name]): Result =
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    59
      {
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    60
        if (pending.nonEmpty) {
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    61
          val requirements = dep_graph.all_preds(pending).reverse
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    62
          (requirements, Load_Bulk(pending, checkpoints))
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    63
        }
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    64
        else load_checkpoints(checkpoints)
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    65
      }
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    66
70765
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
    67
      val (load_theories, st1) =
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
    68
        this match {
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
    69
          case Load_Init(Nil) =>
70769
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    70
            val pending = dep_graph.maximals.filterNot(finished)
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    71
            if (pending.isEmpty) (Nil, Load_Finished) else load_requirements(pending, Nil)
70767
wenzelm
parents: 70766
diff changeset
    72
          case Load_Init(target :: checkpoints) =>
wenzelm
parents: 70766
diff changeset
    73
            (dep_graph.all_preds(List(target)).reverse, Load_Target(target, checkpoints))
70768
670bb96096a7 tuned signature;
wenzelm
parents: 70767
diff changeset
    74
          case Load_Target(pending, checkpoints) if finished(pending) =>
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
    75
            val dep_graph1 =
70767
wenzelm
parents: 70766
diff changeset
    76
              if (checkpoints.isEmpty) dep_graph
wenzelm
parents: 70766
diff changeset
    77
              else dep_graph.exclude(dep_graph.all_succs(checkpoints).toSet)
70769
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    78
            val dep_graph2 =
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    79
              dep_graph1.restrict(dep_graph.all_succs(List(pending)).toSet)
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    80
            val pending2 =
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    81
              dep_graph.maximals.filter(node => dep_graph2.defined(node) && !finished(node))
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    82
            load_requirements(pending2, checkpoints)
70768
670bb96096a7 tuned signature;
wenzelm
parents: 70767
diff changeset
    83
          case Load_Bulk(pending, checkpoints) if pending.forall(finished) =>
70769
9514fdbb8abe clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents: 70768
diff changeset
    84
            load_checkpoints(checkpoints)
70765
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
    85
          case st => (Nil, st)
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
    86
        }
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
    87
      (load_theories.filterNot(finished), st1)
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
    88
    }
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
    89
  }
70765
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
    90
  private case class Load_Init(checkpoints: List[Document.Node.Name]) extends Load_State
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
    91
  private case class Load_Target(
70768
670bb96096a7 tuned signature;
wenzelm
parents: 70767
diff changeset
    92
    pending: Document.Node.Name, checkpoints: List[Document.Node.Name]) extends Load_State
670bb96096a7 tuned signature;
wenzelm
parents: 70767
diff changeset
    93
  private case class Load_Bulk(
670bb96096a7 tuned signature;
wenzelm
parents: 70767
diff changeset
    94
    pending: List[Document.Node.Name], checkpoints: List[Document.Node.Name]) extends Load_State
70765
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
    95
  private case object Load_Finished extends Load_State
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
    96
69520
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
    97
  class Session private[Headless](
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
    98
    session_name: String,
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
    99
    _session_options: => Options,
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   100
    override val resources: Resources) extends isabelle.Session(_session_options, resources)
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   101
  {
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   102
    session =>
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
   103
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   104
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   105
    private def loaded_theory(name: Document.Node.Name): Boolean =
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   106
      resources.session_base.loaded_theory(name.theory)
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   107
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   108
69520
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   109
    /* options */
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   110
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   111
    def default_check_delay: Time = session_options.seconds("headless_check_delay")
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   112
    def default_check_limit: Int = session_options.int("headless_check_limit")
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   113
    def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay")
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   114
    def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout")
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   115
    def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay")
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
   116
68922
wenzelm
parents: 68916
diff changeset
   117
wenzelm
parents: 68916
diff changeset
   118
    /* temporary directory */
wenzelm
parents: 68916
diff changeset
   119
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   120
    val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
67946
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
   121
    val tmp_dir_name: String = File.path(tmp_dir).implode
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   122
68923
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   123
    def master_directory(master_dir: String): String =
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   124
      proper_string(master_dir) getOrElse tmp_dir_name
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   125
67945
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
   126
    override def toString: String = session_name
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
   127
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   128
    override def stop(): Process_Result =
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   129
    {
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   130
      try { super.stop() }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   131
      finally { Isabelle_System.rm_tree(tmp_dir) }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   132
    }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
   133
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   134
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   135
    /* theories */
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   136
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   137
    private sealed case class Use_Theories_State(
70697
43bdcf778cfe tuned signature;
wenzelm
parents: 70683
diff changeset
   138
      dep_graph: Document.Node.Name.Graph[Unit],
70765
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
   139
      load_state: Load_State,
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   140
      watchdog_timeout: Time,
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   141
      commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit],
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   142
      last_update: Time = Time.now(),
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   143
      nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   144
      already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
70644
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   145
      result: Option[Exn.Result[Use_Theories_Result]] = None)
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   146
    {
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   147
      def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   148
        copy(last_update = Time.now(), nodes_status = new_nodes_status)
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   149
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   150
      def watchdog: Boolean =
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   151
        watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   152
70644
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   153
      def finished_result: Boolean = result.isDefined
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   154
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   155
      def join_result: Option[(Exn.Result[Use_Theories_Result], Use_Theories_State)] =
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   156
        if (finished_result) Some((result.get, this)) else None
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   157
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   158
      def cancel_result: Use_Theories_State =
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   159
        if (finished_result) this else copy(result = Some(Exn.Exn(Exn.Interrupt())))
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   160
70763
5fae55752c70 tuned messages (again) -- avoid confusion wrt. total remaining size;
wenzelm
parents: 70710
diff changeset
   161
      def clean_theories: (List[Document.Node.Name], Use_Theories_State) =
70698
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   162
      {
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   163
        @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name])
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   164
          : Set[Document.Node.Name] =
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   165
        {
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   166
          val add = base.filter(name => dep_graph.imm_succs(name).forall(front))
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   167
          if (add.isEmpty) front
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   168
          else {
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   169
            val preds = add.map(dep_graph.imm_preds)
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   170
            val base1 = (preds.head /: preds.tail)(_ ++ _).toList.filter(already_committed.keySet)
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   171
            frontier(base1, front ++ add)
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   172
          }
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   173
        }
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   174
70763
5fae55752c70 tuned messages (again) -- avoid confusion wrt. total remaining size;
wenzelm
parents: 70710
diff changeset
   175
        if (already_committed.isEmpty) (Nil, this)
70698
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   176
        else {
70705
wenzelm
parents: 70704
diff changeset
   177
          val base =
wenzelm
parents: 70704
diff changeset
   178
            (for {
wenzelm
parents: 70704
diff changeset
   179
              (name, (_, (_, succs))) <- dep_graph.iterator
wenzelm
parents: 70704
diff changeset
   180
              if succs.isEmpty && already_committed.isDefinedAt(name)
wenzelm
parents: 70704
diff changeset
   181
            } yield name).toList
wenzelm
parents: 70704
diff changeset
   182
          val clean = frontier(base, Set.empty)
70763
5fae55752c70 tuned messages (again) -- avoid confusion wrt. total remaining size;
wenzelm
parents: 70710
diff changeset
   183
          if (clean.isEmpty) (Nil, this)
70698
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   184
          else {
70763
5fae55752c70 tuned messages (again) -- avoid confusion wrt. total remaining size;
wenzelm
parents: 70710
diff changeset
   185
            (dep_graph.topological_order.filter(clean),
70699
3eb30d80cee6 tuned signature;
wenzelm
parents: 70698
diff changeset
   186
              copy(dep_graph = dep_graph.exclude(clean)))
70698
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   187
          }
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   188
        }
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   189
      }
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   190
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   191
      def check(state: Document.State, version: Document.Version, beyond_limit: Boolean)
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   192
        : (List[Document.Node.Name], Use_Theories_State) =
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   193
      {
69035
d75cd481f8d9 proper status after commit;
wenzelm
parents: 69032
diff changeset
   194
        val already_committed1 =
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   195
          commit match {
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   196
            case None => already_committed
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   197
            case Some(commit_fn) =>
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   198
              (already_committed /: dep_graph.topological_order)(
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   199
                { case (committed, name) =>
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   200
                    def parents_committed: Boolean =
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   201
                      version.nodes(name).header.imports.forall(parent =>
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   202
                        loaded_theory(parent) || committed.isDefinedAt(parent))
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   203
                    if (!committed.isDefinedAt(name) && parents_committed &&
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   204
                        state.node_consolidated(version, name))
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   205
                    {
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   206
                      val snapshot = stable_snapshot(state, version, name)
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   207
                      val status = Document_Status.Node_Status.make(state, version, name)
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   208
                      commit_fn(snapshot, status)
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   209
                      committed + (name -> status)
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   210
                    }
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   211
                    else committed
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   212
                })
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   213
          }
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   214
70657
2bf1d0e57695 proper finished_theory status for result;
wenzelm
parents: 70653
diff changeset
   215
        def finished_theory(name: Document.Node.Name): Boolean =
2bf1d0e57695 proper finished_theory status for result;
wenzelm
parents: 70653
diff changeset
   216
          loaded_theory(name) ||
70704
b080d1fb9777 clarified theory status;
wenzelm
parents: 70702
diff changeset
   217
          (if (commit.isDefined) already_committed1.isDefinedAt(name)
b080d1fb9777 clarified theory status;
wenzelm
parents: 70702
diff changeset
   218
           else state.node_consolidated(version, name))
70657
2bf1d0e57695 proper finished_theory status for result;
wenzelm
parents: 70653
diff changeset
   219
70644
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   220
        val result1 =
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   221
          if (!finished_result &&
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   222
            (beyond_limit || watchdog ||
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   223
              dep_graph.keys_iterator.forall(name =>
70657
2bf1d0e57695 proper finished_theory status for result;
wenzelm
parents: 70653
diff changeset
   224
                finished_theory(name) || nodes_status.quasi_consolidated(name))))
70644
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   225
          {
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   226
            val nodes =
70657
2bf1d0e57695 proper finished_theory status for result;
wenzelm
parents: 70653
diff changeset
   227
              (for {
2bf1d0e57695 proper finished_theory status for result;
wenzelm
parents: 70653
diff changeset
   228
                name <- dep_graph.keys_iterator
2bf1d0e57695 proper finished_theory status for result;
wenzelm
parents: 70653
diff changeset
   229
                if !loaded_theory(name)
2bf1d0e57695 proper finished_theory status for result;
wenzelm
parents: 70653
diff changeset
   230
              } yield { (name -> Document_Status.Node_Status.make(state, version, name)) }).toList
70644
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   231
            val nodes_committed =
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   232
              (for {
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   233
                name <- dep_graph.keys_iterator
70644
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   234
                status <- already_committed1.get(name)
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   235
              } yield (name -> status)).toList
70644
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   236
            Some(Exn.Res(new Use_Theories_Result(state, version, nodes, nodes_committed)))
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   237
          }
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   238
          else result
68925
76ce16eefab9 record status of already committed nodes;
wenzelm
parents: 68923
diff changeset
   239
70765
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
   240
        val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory(_))
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   241
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   242
        (load_theories,
70765
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
   243
          copy(already_committed = already_committed1, result = result1, load_state = load_state1))
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   244
      }
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   245
    }
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   246
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   247
    def use_theories(
67940
b4e80f062fbf clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents: 67939
diff changeset
   248
      theories: List[String],
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   249
      qualifier: String = Sessions.DRAFT,
67881
812ed06dadec interruptible exploration of dependencies;
wenzelm
parents: 67879
diff changeset
   250
      master_dir: String = "",
69920
79c8ff387ed1 support unicode_symbols in input source;
wenzelm
parents: 69857
diff changeset
   251
      unicode_symbols: Boolean = false,
68943
e564605d4cac tuned signature;
wenzelm
parents: 68936
diff changeset
   252
      check_delay: Time = default_check_delay,
69520
16779868de1f clarified defaults via system options;
wenzelm
parents: 69458
diff changeset
   253
      check_limit: Int = default_check_limit,
68947
ea804c814693 clarified defaults;
wenzelm
parents: 68943
diff changeset
   254
      watchdog_timeout: Time = default_watchdog_timeout,
68943
e564605d4cac tuned signature;
wenzelm
parents: 68936
diff changeset
   255
      nodes_status_delay: Time = default_nodes_status_delay,
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69255
diff changeset
   256
      id: UUID.T = UUID.random(),
70625
1ae987cc052f support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
wenzelm
parents: 69920
diff changeset
   257
      share_common_data: Boolean = false,
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   258
      checkpoints: Set[Document.Node.Name] = Set.empty,
68916
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   259
      // commit: must not block, must not fail
2a1583baaaa0 support dynamic commit of consilidated nodes;
wenzelm
parents: 68915
diff changeset
   260
      commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
68981
30daac7848b9 tuned signature;
wenzelm
parents: 68962
diff changeset
   261
      commit_cleanup_delay: Time = default_commit_cleanup_delay,
69013
bb4e4c253ebe tuned signature;
wenzelm
parents: 69012
diff changeset
   262
      progress: Progress = No_Progress): Use_Theories_Result =
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   263
    {
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   264
      val dependencies =
68894
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   265
      {
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   266
        val import_names =
68923
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   267
          theories.map(thy =>
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   268
            resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none)
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   269
        resources.dependencies(import_names, progress = progress).check_errors
68894
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   270
      }
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   271
      val dep_theories = dependencies.theories
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   272
      val dep_theories_set = dep_theories.toSet
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   273
      val dep_files =
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   274
        dependencies.loaded_files(false).flatMap(_._2).
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   275
          map(path => Document.Node.Name(resources.append("", path)))
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   276
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   277
      val use_theories_state =
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   278
      {
70765
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
   279
        val load_state =
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
   280
          Load_Init(
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   281
            if (checkpoints.isEmpty) Nil
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   282
            else dependencies.theory_graph.topological_order.filter(checkpoints(_)))
70697
43bdcf778cfe tuned signature;
wenzelm
parents: 70683
diff changeset
   283
        Synchronized(
70765
87beb7fb0cc6 more explicit type Load_State;
wenzelm
parents: 70763
diff changeset
   284
          Use_Theories_State(dependencies.theory_graph, load_state, watchdog_timeout, commit))
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   285
      }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   286
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   287
      def check_state(beyond_limit: Boolean = false)
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   288
      {
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   289
        val state = session.current_state()
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   290
        for (version <- state.stable_tip_version) {
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   291
          val load_theories = use_theories_state.change_result(_.check(state, version, beyond_limit))
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   292
          if (load_theories.nonEmpty) {
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   293
            resources.load_theories(
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   294
              session, id, load_theories, dep_files, unicode_symbols, share_common_data, progress)
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   295
          }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   296
        }
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   297
      }
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   298
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   299
      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
   300
      {
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   301
        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
   302
        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
   303
          {
70644
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   304
            if (progress.stopped) use_theories_state.change(_.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
   305
            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
   306
              check_count += 1
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   307
              check_state(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
   308
            }
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   309
          }
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   310
      }
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   311
68906
wenzelm
parents: 68905
diff changeset
   312
      val consumer =
wenzelm
parents: 68905
diff changeset
   313
      {
wenzelm
parents: 68905
diff changeset
   314
        val delay_nodes_status =
wenzelm
parents: 68905
diff changeset
   315
          Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
69818
60d0ee8f2ddb more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents: 69817
diff changeset
   316
            progress.nodes_status(use_theories_state.value.nodes_status)
68906
wenzelm
parents: 68905
diff changeset
   317
          }
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   318
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   319
        val delay_commit_clean =
68981
30daac7848b9 tuned signature;
wenzelm
parents: 68962
diff changeset
   320
          Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
70763
5fae55752c70 tuned messages (again) -- avoid confusion wrt. total remaining size;
wenzelm
parents: 70710
diff changeset
   321
            val clean_theories = use_theories_state.change_result(_.clean_theories)
70702
a65b9624cb98 tuned messages;
wenzelm
parents: 70699
diff changeset
   322
            if (clean_theories.nonEmpty) {
70766
5006ca9aadbb tuned message;
wenzelm
parents: 70765
diff changeset
   323
              progress.echo("Removing " + clean_theories.length + " theories")
70702
a65b9624cb98 tuned messages;
wenzelm
parents: 70699
diff changeset
   324
              resources.clean_theories(session, id, clean_theories)
a65b9624cb98 tuned messages;
wenzelm
parents: 70699
diff changeset
   325
            }
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   326
          }
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   327
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   328
        Session.Consumer[Session.Commands_Changed](getClass.getName) {
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   329
          case changed =>
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   330
            if (changed.nodes.exists(dep_theories_set)) {
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   331
              val snapshot = session.snapshot()
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   332
              val state = snapshot.state
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   333
              val version = snapshot.version
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   334
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68952
diff changeset
   335
              val theory_progress =
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   336
                use_theories_state.change_result(st =>
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   337
                  {
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   338
                    val domain =
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   339
                      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
   340
                      else changed.nodes.iterator.filter(dep_theories_set).toSet
68899
b15b03c13dbb more detailed progress;
wenzelm
parents: 68894
diff changeset
   341
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   342
                    val (nodes_status_changed, nodes_status1) =
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 69035
diff changeset
   343
                      st.nodes_status.update(resources, state, version,
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   344
                        domain = Some(domain), trim = changed.assignment)
68899
b15b03c13dbb more detailed progress;
wenzelm
parents: 68894
diff changeset
   345
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   346
                    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
   347
                      delay_nodes_status.invoke
68899
b15b03c13dbb more detailed progress;
wenzelm
parents: 68894
diff changeset
   348
                    }
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   349
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68952
diff changeset
   350
                    val theory_progress =
68905
90a6b714aca3 tuned -- prefer immutable data;
wenzelm
parents: 68904
diff changeset
   351
                      (for {
69818
60d0ee8f2ddb more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents: 69817
diff changeset
   352
                        (name, node_status) <- nodes_status1.present.iterator
68959
d4223afddd47 clarified message;
wenzelm
parents: 68958
diff changeset
   353
                        if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
68962
50676b0ab970 tuned message (again);
wenzelm
parents: 68959
diff changeset
   354
                        p1 = node_status.percentage
50676b0ab970 tuned message (again);
wenzelm
parents: 68959
diff changeset
   355
                        if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
50676b0ab970 tuned message (again);
wenzelm
parents: 68959
diff changeset
   356
                      } yield Progress.Theory(name.theory, percentage = Some(p1))).toList
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   357
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68952
diff changeset
   358
                    (theory_progress, st.update(nodes_status1))
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   359
                  })
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   360
68957
eef4e983fd9d clarified theory progress;
wenzelm
parents: 68952
diff changeset
   361
              theory_progress.foreach(progress.theory(_))
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   362
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   363
              check_state()
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   364
68981
30daac7848b9 tuned signature;
wenzelm
parents: 68962
diff changeset
   365
              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
   366
                if (use_theories_state.value.finished_result)
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   367
                  delay_commit_clean.revoke
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   368
                else delay_commit_clean.invoke
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   369
              }
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   370
            }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   371
        }
68906
wenzelm
parents: 68905
diff changeset
   372
      }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   373
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   374
      try {
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   375
        session.commands_changed += consumer
70653
f7c5b30fc432 load theories in stages, to reduce ML heap requirements;
wenzelm
parents: 70649
diff changeset
   376
        check_state()
70644
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   377
        use_theories_state.guarded_access(_.join_result)
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   378
        check_progress.cancel
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   379
      }
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   380
      finally {
68907
wenzelm
parents: 68906
diff changeset
   381
        session.commands_changed -= consumer
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   382
        resources.unload_theories(session, id, dep_theories)
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   383
      }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   384
70644
b23a6dfcfd57 clarified state variable: avoid extra mutability via Promise;
wenzelm
parents: 70640
diff changeset
   385
      Exn.release(use_theories_state.guarded_access(_.join_result))
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   386
    }
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   387
67939
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   388
    def purge_theories(
68915
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   389
      theories: List[String],
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   390
      qualifier: String = Sessions.DRAFT,
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   391
      master_dir: String = "",
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   392
      all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   393
    {
68923
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   394
      val nodes =
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   395
        if (all) None
59d2eab3f8b9 tuned signature;
wenzelm
parents: 68922
diff changeset
   396
        else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _)))
68915
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   397
      resources.purge_theories(session, nodes)
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   398
    }
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
   399
  }
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
   400
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
   401
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   402
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   403
  /** resources **/
68922
wenzelm
parents: 68916
diff changeset
   404
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   405
  object Resources
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   406
  {
69536
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   407
    def apply(base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   408
      new Resources(base_info, log = log)
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   409
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   410
    def make(
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   411
      options: Options,
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   412
      session_name: String,
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   413
      session_dirs: List[Path] = Nil,
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   414
      include_sessions: List[String] = Nil,
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   415
      progress: Progress = No_Progress,
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   416
      log: Logger = No_Logger): Resources =
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   417
    {
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   418
      val base_info =
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   419
        Sessions.base_info(options, session_name, dirs = session_dirs,
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   420
          include_sessions = include_sessions, progress = progress)
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   421
      apply(base_info, log = log)
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   422
    }
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   423
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   424
    final class Theory private[Headless](
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   425
      val node_name: Document.Node.Name,
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   426
      val node_header: Document.Node.Header,
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   427
      val text: String,
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   428
      val node_required: Boolean)
68922
wenzelm
parents: 68916
diff changeset
   429
    {
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   430
      override def toString: String = node_name.toString
68922
wenzelm
parents: 68916
diff changeset
   431
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   432
      def node_perspective: Document.Node.Perspective_Text =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   433
        Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
68922
wenzelm
parents: 68916
diff changeset
   434
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   435
      def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   436
        List(node_name -> Document.Node.Deps(node_header),
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   437
          node_name -> Document.Node.Edits(text_edits),
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   438
          node_name -> node_perspective)
68922
wenzelm
parents: 68916
diff changeset
   439
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   440
      def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   441
      {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   442
        val (text_edits, old_required) =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   443
          if (old.isEmpty) (Text.Edit.inserts(0, text), false)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   444
          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
   445
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   446
        if (text_edits.isEmpty && node_required == old_required) Nil
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   447
        else make_edits(text_edits)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   448
      }
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   449
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   450
      def purge_edits: List[Document.Edit_Text] =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   451
        make_edits(Text.Edit.removes(0, text))
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   452
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   453
      def required(required: Boolean): Theory =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   454
        if (required == node_required) this
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   455
        else new Theory(node_name, node_header, text, required)
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   456
    }
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   457
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   458
    sealed case class State(
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   459
      blobs: Map[Document.Node.Name, Document.Blob] = Map.empty,
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   460
      theories: Map[Document.Node.Name, Theory] = Map.empty,
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   461
      required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty)
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   462
    {
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   463
      /* blobs */
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   464
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   465
      def doc_blobs: Document.Blobs = Document.Blobs(blobs)
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   466
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   467
      def update_blobs(names: List[Document.Node.Name]): (Document.Blobs, State) =
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   468
      {
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   469
        val new_blobs =
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   470
          names.flatMap(name =>
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   471
          {
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   472
            val bytes = Bytes.read(name.path)
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   473
            def new_blob: Document.Blob =
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   474
            {
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   475
              val text = bytes.text
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   476
              Document.Blob(bytes, text, Symbol.Text_Chunk(text), changed = true)
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   477
            }
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   478
            blobs.get(name) match {
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   479
              case Some(blob) => if (blob.bytes == bytes) None else Some(name -> new_blob)
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   480
              case None => Some(name -> new_blob)
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   481
            }
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   482
          })
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   483
        val blobs1 = (blobs /: new_blobs)(_ + _)
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   484
        val blobs2 = (blobs /: new_blobs)({ case (map, (a, b)) => map + (a -> b.unchanged) })
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   485
        (Document.Blobs(blobs1), copy(blobs = blobs2))
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   486
      }
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   487
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   488
      def blob_edits(name: Document.Node.Name, old_blob: Option[Document.Blob])
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   489
        : List[Document.Edit_Text] =
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   490
      {
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   491
        val blob = blobs.getOrElse(name, error("Missing blob " + quote(name.toString)))
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   492
        val text_edits =
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   493
          old_blob match {
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   494
            case None => List(Text.Edit.insert(0, blob.source))
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   495
            case Some(blob0) => Text.Edit.replace(0, blob0.source, blob.source)
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   496
          }
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   497
        if (text_edits.isEmpty) Nil
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   498
        else List(name -> Document.Node.Blob(blob), name -> Document.Node.Edits(text_edits))
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   499
      }
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   500
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   501
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   502
      /* theories */
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   503
70674
29bb1ebb188f clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
wenzelm
parents: 70657
diff changeset
   504
      lazy val theory_graph: Document.Node.Name.Graph[Unit] =
29bb1ebb188f clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
wenzelm
parents: 70657
diff changeset
   505
        Document.Node.Name.make_graph(
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   506
          for ((name, theory) <- theories.toList)
70647
3047b7671279 tuned signature;
wenzelm
parents: 70644
diff changeset
   507
          yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_))))
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   508
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   509
      def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   510
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69255
diff changeset
   511
      def insert_required(id: UUID.T, names: List[Document.Node.Name]): State =
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   512
        copy(required = (required /: names)(_.insert(_, id)))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   513
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69255
diff changeset
   514
      def remove_required(id: UUID.T, names: List[Document.Node.Name]): State =
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   515
        copy(required = (required /: names)(_.remove(_, id)))
68958
9199f9da512a tuned message;
wenzelm
parents: 68957
diff changeset
   516
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   517
      def update_theories(update: List[(Document.Node.Name, Theory)]): State =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   518
        copy(theories =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   519
          (theories /: update)({ case (thys, (name, thy)) =>
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   520
            thys.get(name) match {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   521
              case Some(thy1) if thy1 == thy => thys
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   522
              case _ => thys + (name -> thy)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   523
            }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   524
          }))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   525
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   526
      def remove_theories(remove: List[Document.Node.Name]): State =
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   527
      {
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   528
        require(remove.forall(name => !is_required(name)))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   529
        copy(theories = theories -- remove)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   530
      }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   531
70649
9a40720750dc clarified signature;
wenzelm
parents: 70648
diff changeset
   532
      def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name])
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69255
diff changeset
   533
        : State =
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   534
      {
70649
9a40720750dc clarified signature;
wenzelm
parents: 70648
diff changeset
   535
        val st1 = remove_required(id, theories)
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   536
        val theory_edits =
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   537
          for {
70649
9a40720750dc clarified signature;
wenzelm
parents: 70648
diff changeset
   538
            node_name <- theories
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   539
            theory <- st1.theories.get(node_name)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   540
          }
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   541
          yield {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   542
            val theory1 = theory.required(st1.is_required(node_name))
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   543
            val edits = theory1.node_edits(Some(theory))
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   544
            (edits, (node_name, theory1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   545
          }
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   546
        session.update(doc_blobs, theory_edits.flatMap(_._1))
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   547
        st1.update_theories(theory_edits.map(_._2))
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   548
      }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   549
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   550
      def purge_theories(session: Session, nodes: List[Document.Node.Name])
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   551
        : ((List[Document.Node.Name], List[Document.Node.Name]), State) =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   552
      {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   553
        val all_nodes = theory_graph.topological_order
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   554
        val purge = nodes.filterNot(is_required(_)).toSet
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   555
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   556
        val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   557
        val (retained, purged) = all_nodes.partition(retain)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   558
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   559
        val purge_edits = purged.flatMap(name => theories(name).purge_edits)
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   560
        session.update(doc_blobs, purge_edits)
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   561
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   562
        ((purged, retained), remove_theories(purged))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   563
      }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   564
    }
68936
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   565
  }
90c08c7bab9c continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents: 68935
diff changeset
   566
69536
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   567
  class Resources private[Headless](
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   568
      val session_base_info: Sessions.Base_Info,
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   569
      log: Logger = No_Logger)
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70674
diff changeset
   570
    extends isabelle.Resources(
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70674
diff changeset
   571
      session_base_info.sessions_structure, session_base_info.check_base, log = log)
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   572
  {
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   573
    resources =>
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   574
69538
faf547d2834c clarified signature, notably cascade of dump_options, deps, resources, session;
wenzelm
parents: 69536
diff changeset
   575
    def options: Options = session_base_info.options
faf547d2834c clarified signature, notably cascade of dump_options, deps, resources, session;
wenzelm
parents: 69536
diff changeset
   576
69536
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   577
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   578
    /* session */
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   579
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   580
    def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   581
    {
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   582
      val session = new Session(session_base_info.session, options, resources)
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   583
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   584
      val session_error = Future.promise[String]
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   585
      var session_phase: Session.Consumer[Session.Phase] = null
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   586
      session_phase =
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   587
        Session.Consumer(getClass.getName) {
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   588
          case Session.Ready =>
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   589
            session.phase_changed -= session_phase
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   590
            session_error.fulfill("")
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   591
          case Session.Terminated(result) if !result.ok =>
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   592
            session.phase_changed -= session_phase
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   593
            session_error.fulfill("Session start failed: return code " + result.rc)
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   594
          case _ =>
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   595
        }
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   596
      session.phase_changed += session_phase
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   597
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   598
      progress.echo("Starting session " + session_base_info.session + " ...")
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   599
      Isabelle_Process.start(session, options,
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   600
        logic = session_base_info.session, dirs = session_base_info.dirs, modes = print_mode)
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   601
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   602
      session_error.join match {
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   603
        case "" => session
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   604
        case msg => session.stop(); error(msg)
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   605
      }
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   606
    }
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   607
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   608
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   609
    /* theories */
892b68f932f9 clarified signature;
wenzelm
parents: 69520
diff changeset
   610
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   611
    private val state = Synchronized(Resources.State())
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   612
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   613
    def load_theories(
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   614
      session: Session,
69458
5655af3ea5bd clarified modules and signature;
wenzelm
parents: 69255
diff changeset
   615
      id: UUID.T,
70649
9a40720750dc clarified signature;
wenzelm
parents: 70648
diff changeset
   616
      theories: List[Document.Node.Name],
9a40720750dc clarified signature;
wenzelm
parents: 70648
diff changeset
   617
      files: List[Document.Node.Name],
69920
79c8ff387ed1 support unicode_symbols in input source;
wenzelm
parents: 69857
diff changeset
   618
      unicode_symbols: Boolean,
70625
1ae987cc052f support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
wenzelm
parents: 69920
diff changeset
   619
      share_common_data: Boolean,
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   620
      progress: Progress)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   621
    {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   622
      val loaded_theories =
70649
9a40720750dc clarified signature;
wenzelm
parents: 70648
diff changeset
   623
        for (node_name <- theories)
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   624
        yield {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   625
          val path = node_name.path
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   626
          if (!node_name.is_theory) error("Not a theory file: " + path)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   627
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   628
          progress.expose_interrupt()
69920
79c8ff387ed1 support unicode_symbols in input source;
wenzelm
parents: 69857
diff changeset
   629
          val text0 = File.read(path)
79c8ff387ed1 support unicode_symbols in input source;
wenzelm
parents: 69857
diff changeset
   630
          val text = if (unicode_symbols) Symbol.decode(text0) else text0
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   631
          val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   632
          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
   633
        }
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   634
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   635
      val loaded = loaded_theories.length
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   636
      if (loaded > 1) progress.echo("Loading " + loaded + " theories ...")
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   637
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   638
      state.change(st =>
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   639
        {
70649
9a40720750dc clarified signature;
wenzelm
parents: 70648
diff changeset
   640
          val (doc_blobs1, st1) = st.insert_required(id, theories).update_blobs(files)
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   641
          val theory_edits =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   642
            for (theory <- loaded_theories)
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   643
            yield {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   644
              val node_name = theory.node_name
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   645
              val theory1 = theory.required(st1.is_required(node_name))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   646
              val edits = theory1.node_edits(st1.theories.get(node_name))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   647
              (edits, (node_name, theory1))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   648
            }
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   649
          val file_edits =
70649
9a40720750dc clarified signature;
wenzelm
parents: 70648
diff changeset
   650
            for { node_name <- files if doc_blobs1.changed(node_name) }
69562
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   651
            yield st1.blob_edits(node_name, st.blobs.get(node_name))
636b3c03a61a include loaded_files as doc_blobs (without purging);
wenzelm
parents: 69538
diff changeset
   652
70625
1ae987cc052f support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
wenzelm
parents: 69920
diff changeset
   653
          session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten,
1ae987cc052f support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
wenzelm
parents: 69920
diff changeset
   654
            share_common_data = share_common_data)
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   655
          st1.update_theories(theory_edits.map(_._2))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   656
        })
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   657
    }
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   658
70649
9a40720750dc clarified signature;
wenzelm
parents: 70648
diff changeset
   659
    def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name])
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   660
    {
70649
9a40720750dc clarified signature;
wenzelm
parents: 70648
diff changeset
   661
      state.change(_.unload_theories(session, id, theories))
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   662
    }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   663
70698
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   664
    def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name])
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   665
    {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   666
      state.change(st =>
70698
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   667
        st.unload_theories(session, id, theories).purge_theories(session, theories)._2
93aa546ffbac proper clean_theories wrt. dynamic dep_graph;
wenzelm
parents: 70697
diff changeset
   668
      )
69012
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   669
    }
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   670
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   671
    def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   672
      : (List[Document.Node.Name], List[Document.Node.Name]) =
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   673
    {
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   674
      state.change_result(st => st.purge_theories(session, nodes getOrElse st.theory_graph.keys))
c91d14ab065f clarified modules;
wenzelm
parents: 68986
diff changeset
   675
    }
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   676
  }
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   677
}