src/Pure/Thy/thy_resources.scala
author wenzelm
Wed, 05 Sep 2018 20:29:23 +0200
changeset 68915 634768c0bd22
parent 68914 51bd9e9501fb
child 68916 2a1583baaaa0
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/thy_resources.scala
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     3
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
     4
PIDE resources for theory files: load/unload theories via PIDE document updates.
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
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    12
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    13
object Thy_Resources
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    14
{
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    15
  /* PIDE session */
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    16
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    17
  def start_session(
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    18
    options: Options,
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    19
    session_name: String,
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    20
    session_dirs: List[Path] = Nil,
67948
83902fff6243 clarified signature;
wenzelm
parents: 67946
diff changeset
    21
    include_sessions: List[String] = Nil,
67062
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    22
    session_base: Option[Sessions.Base] = None,
67869
8cb4fef58379 support for "session_start";
wenzelm
parents: 67852
diff changeset
    23
    print_mode: List[String] = Nil,
8cb4fef58379 support for "session_start";
wenzelm
parents: 67852
diff changeset
    24
    progress: Progress = No_Progress,
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    25
    log: Logger = No_Logger): Session =
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    26
  {
67062
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    27
    val base =
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    28
      session_base getOrElse
67948
83902fff6243 clarified signature;
wenzelm
parents: 67946
diff changeset
    29
        Sessions.base_info(options, session_name, include_sessions = include_sessions,
83902fff6243 clarified signature;
wenzelm
parents: 67946
diff changeset
    30
          progress = progress, dirs = session_dirs).check_base
67062
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    31
    val resources = new Thy_Resources(base, log = log)
67945
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
    32
    val session = new Session(session_name, options, resources)
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    33
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    34
    val session_error = Future.promise[String]
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    35
    var session_phase: Session.Consumer[Session.Phase] = null
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    36
    session_phase =
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    37
      Session.Consumer(getClass.getName) {
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    38
        case Session.Ready =>
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    39
          session.phase_changed -= session_phase
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    40
          session_error.fulfill("")
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    41
        case Session.Terminated(result) if !result.ok =>
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    42
          session.phase_changed -= session_phase
67869
8cb4fef58379 support for "session_start";
wenzelm
parents: 67852
diff changeset
    43
          session_error.fulfill("Session start failed: return code " + result.rc)
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    44
        case _ =>
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    45
      }
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    46
    session.phase_changed += session_phase
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    47
67877
ff12c4556e2f tuned message;
wenzelm
parents: 67869
diff changeset
    48
    progress.echo("Starting " + session_name + " ...")
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    49
    Isabelle_Process.start(session, options,
67869
8cb4fef58379 support for "session_start";
wenzelm
parents: 67852
diff changeset
    50
      logic = session_name, dirs = session_dirs, modes = print_mode)
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    51
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    52
    session_error.join match {
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    53
      case "" => session
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    54
      case msg => session.stop(); error(msg)
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    55
    }
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    56
  }
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    57
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68330
diff changeset
    58
  class Theories_Result private[Thy_Resources](
67883
171e7735ce25 support for "use_theories";
wenzelm
parents: 67881
diff changeset
    59
    val state: Document.State,
67889
wenzelm
parents: 67888
diff changeset
    60
    val version: Document.Version,
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 68694
diff changeset
    61
    val nodes: List[(Document.Node.Name, Document_Status.Node_Status)])
67879
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
    62
  {
68319
2e168460a9c3 more operations;
wenzelm
parents: 68106
diff changeset
    63
    def node_names: List[Document.Node.Name] = nodes.map(_._1)
67883
171e7735ce25 support for "use_theories";
wenzelm
parents: 67881
diff changeset
    64
    def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
67897
a5b9d1f51b04 output result messages;
wenzelm
parents: 67894
diff changeset
    65
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68330
diff changeset
    66
    def snapshot(node_name: Document.Node.Name): Document.Snapshot =
67897
a5b9d1f51b04 output result messages;
wenzelm
parents: 67894
diff changeset
    67
    {
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68330
diff changeset
    68
      val snapshot = state.snapshot(node_name)
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68330
diff changeset
    69
      assert(version.id == snapshot.version.id)
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68330
diff changeset
    70
      snapshot
68106
a514e29db980 return exports as result for Isabelle server;
wenzelm
parents: 67948
diff changeset
    71
    }
67879
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
    72
  }
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
    73
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
    74
  val default_check_delay: Double = 0.5
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
    75
  val default_nodes_status_delay: Double = -1.0
68694
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
    76
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
    77
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    78
  class Session private[Thy_Resources](
67945
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
    79
    session_name: String,
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
    80
    session_options: Options,
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
    81
    override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    82
  {
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    83
    session =>
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    84
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    85
    val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
67946
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
    86
    val tmp_dir_name: String = File.path(tmp_dir).implode
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    87
67945
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
    88
    override def toString: String = session_name
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
    89
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    90
    override def stop(): Process_Result =
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    91
    {
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    92
      try { super.stop() }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    93
      finally { Isabelle_System.rm_tree(tmp_dir) }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    94
    }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    95
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
    96
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
    97
    /* theories */
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
    98
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
    99
    private sealed case class Use_Theories_State(
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   100
      last_update: Time = Time.now(),
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   101
      nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   102
      already_initialized: Set[Document.Node.Name] = Set.empty)
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   103
    {
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   104
      def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   105
        copy(last_update = Time.now(), nodes_status = new_nodes_status)
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   106
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   107
      def watchdog(watchdog_timeout: Time): Boolean =
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   108
        watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   109
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   110
      def initialized_theories(
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   111
        state: Document.State,
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   112
        version: Document.Version,
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   113
        new_theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) =
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   114
      {
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   115
        val initialized =
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   116
          for {
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   117
            name <- new_theories
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   118
            if !already_initialized(name) &&
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   119
              Document_Status.Node_Status.make(state, version, name).initialized
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   120
          } yield name
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   121
        (initialized, copy(already_initialized = already_initialized ++ initialized))
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   122
      }
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   123
    }
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   124
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   125
    def use_theories(
67940
b4e80f062fbf clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents: 67939
diff changeset
   126
      theories: List[String],
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   127
      qualifier: String = Sessions.DRAFT,
67881
812ed06dadec interruptible exploration of dependencies;
wenzelm
parents: 67879
diff changeset
   128
      master_dir: String = "",
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   129
      check_delay: Time = Time.seconds(default_check_delay),
68694
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   130
      check_limit: Int = 0,
68908
abc338d25640 support for watchdog_timeout;
wenzelm
parents: 68907
diff changeset
   131
      watchdog_timeout: Time = Time.zero,
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   132
      nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   133
      id: UUID = UUID(),
67881
812ed06dadec interruptible exploration of dependencies;
wenzelm
parents: 67879
diff changeset
   134
      progress: Progress = No_Progress): Theories_Result =
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   135
    {
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   136
      val dep_theories =
68894
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   137
      {
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   138
        val master = proper_string(master_dir) getOrElse tmp_dir_name
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   139
        val import_names =
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   140
          theories.map(thy => resources.import_name(qualifier, master, thy) -> Position.none)
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   141
        resources.dependencies(import_names, progress = progress).check_errors.theories
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   142
      }
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   143
      val dep_theories_set = dep_theories.toSet
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   144
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   145
      val use_theories_state = Synchronized(Use_Theories_State())
67879
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
   146
      val result = Future.promise[Theories_Result]
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   147
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
   148
      def check_state(beyond_limit: Boolean = false)
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   149
      {
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   150
        val state = session.current_state()
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   151
        state.stable_tip_version match {
68694
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   152
          case Some(version) =>
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   153
            val st = use_theories_state.value
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   154
            if (beyond_limit || st.watchdog(watchdog_timeout) ||
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   155
                dep_theories.forall(name =>
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   156
                  state.node_consolidated(version, name) ||
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   157
                  st.nodes_status.quasi_consolidated(name)))
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   158
            {
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
   159
              val nodes =
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   160
                for (name <- dep_theories)
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 68694
diff changeset
   161
                yield (name -> Document_Status.Node_Status.make(state, version, name))
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
   162
              try { result.fulfill(new Theories_Result(state, version, nodes)) }
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   163
              catch { case _: IllegalStateException => }
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   164
            }
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   165
          case None =>
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   166
        }
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   167
      }
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   168
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   169
      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
   170
      {
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   171
        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
   172
        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
   173
          {
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   174
            if (progress.stopped) result.cancel
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   175
            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
   176
              check_count += 1
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   177
              check_state(check_limit > 0 && check_count > check_limit)
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   178
            }
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   179
          }
03e104be99af added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents: 68365
diff changeset
   180
      }
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   181
68906
wenzelm
parents: 68905
diff changeset
   182
      val consumer =
wenzelm
parents: 68905
diff changeset
   183
      {
wenzelm
parents: 68905
diff changeset
   184
        val delay_nodes_status =
wenzelm
parents: 68905
diff changeset
   185
          Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   186
            progress.nodes_status(use_theories_state.value.nodes_status)
68906
wenzelm
parents: 68905
diff changeset
   187
          }
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   188
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   189
        Session.Consumer[Session.Commands_Changed](getClass.getName) {
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   190
          case changed =>
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   191
            if (changed.nodes.exists(dep_theories_set)) {
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   192
              val snapshot = session.snapshot()
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   193
              val state = snapshot.state
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   194
              val version = snapshot.version
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   195
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   196
              val theory_percentages =
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   197
                use_theories_state.change_result(st =>
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   198
                  {
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   199
                    val domain =
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   200
                      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
   201
                      else changed.nodes.iterator.filter(dep_theories_set).toSet
68899
b15b03c13dbb more detailed progress;
wenzelm
parents: 68894
diff changeset
   202
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   203
                    val (nodes_status_changed, nodes_status1) =
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   204
                      st.nodes_status.update(resources.session_base, state, version,
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   205
                        domain = Some(domain), trim = changed.assignment)
68899
b15b03c13dbb more detailed progress;
wenzelm
parents: 68894
diff changeset
   206
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   207
                    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
   208
                      delay_nodes_status.invoke
68899
b15b03c13dbb more detailed progress;
wenzelm
parents: 68894
diff changeset
   209
                    }
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68771
diff changeset
   210
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   211
                    val progress_percentage =
68905
90a6b714aca3 tuned -- prefer immutable data;
wenzelm
parents: 68904
diff changeset
   212
                      (for {
68904
09151c54aaac tuned signature;
wenzelm
parents: 68903
diff changeset
   213
                        (name, node_status) <- nodes_status1.present.iterator
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   214
                        if changed.nodes.contains(name)
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   215
                        p1 = node_status.percentage
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   216
                        if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
68905
90a6b714aca3 tuned -- prefer immutable data;
wenzelm
parents: 68904
diff changeset
   217
                      } yield (name.theory, p1)).toList
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   218
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   219
                    (progress_percentage, st.update(nodes_status1))
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   220
                  })
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   221
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   222
              val check_theories =
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   223
                (for {
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   224
                  command <- changed.commands.iterator
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68758
diff changeset
   225
                  if dep_theories_set(command.node_name) && command.potentially_initialized
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   226
                } yield command.node_name).toList
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   227
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   228
              if (check_theories.nonEmpty) {
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   229
                val initialized =
68914
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   230
                  use_theories_state.change_result(
51bd9e9501fb clarified Use_Theories_State;
wenzelm
parents: 68908
diff changeset
   231
                    _.initialized_theories(state, version, check_theories))
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   232
                initialized.map(_.theory).sorted.foreach(progress.theory("", _))
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   233
              }
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   234
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   235
              for ((theory, percentage) <- theory_percentages)
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   236
                progress.theory_percentage("", theory, percentage)
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68899
diff changeset
   237
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
   238
              check_state()
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   239
            }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   240
        }
68906
wenzelm
parents: 68905
diff changeset
   241
      }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   242
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   243
      try {
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   244
        session.commands_changed += consumer
68894
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   245
        resources.load_theories(session, id, dep_theories, progress)
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   246
        result.join_result
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   247
        check_progress.cancel
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   248
      }
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   249
      finally {
68907
wenzelm
parents: 68906
diff changeset
   250
        session.commands_changed -= consumer
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   251
        resources.unload_theories(session, id, dep_theories)
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   252
      }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   253
67879
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
   254
      result.join
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   255
    }
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   256
67939
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   257
    def purge_theories(
68915
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   258
      theories: List[String],
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   259
      qualifier: String = Sessions.DRAFT,
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   260
      master_dir: String = "",
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   261
      all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   262
    {
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   263
      val master = proper_string(master_dir) getOrElse tmp_dir_name
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   264
      val nodes = if (all) None else Some(theories.map(resources.import_name(qualifier, master, _)))
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   265
      resources.purge_theories(session, nodes)
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   266
    }
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
   267
  }
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
   268
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
   269
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   270
  /* internal state */
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   271
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   272
  sealed case class State(
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   273
    required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   274
    theories: Map[Document.Node.Name, Theory] = Map.empty)
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   275
  {
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   276
    def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   277
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   278
    def insert_required(id: UUID, names: List[Document.Node.Name]): State =
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   279
      copy(required = (required /: names)(_.insert(_, id)))
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   280
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   281
    def remove_required(id: UUID, names: List[Document.Node.Name]): State =
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   282
      copy(required = (required /: names)(_.remove(_, id)))
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   283
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   284
    def update_theories(update: List[(Document.Node.Name, Theory)]): State =
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   285
      copy(theories =
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   286
        (theories /: update)({ case (thys, (name, thy)) =>
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   287
          thys.get(name) match {
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   288
            case Some(thy1) if thy1 == thy => thys
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   289
            case _ => thys + (name -> thy)
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   290
          }
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   291
        }))
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   292
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   293
    def remove_theories(remove: List[Document.Node.Name]): State =
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   294
    {
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   295
      require(remove.forall(name => !is_required(name)))
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   296
      copy(theories = theories -- remove)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   297
    }
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   298
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   299
    lazy val theories_graph: Graph[Document.Node.Name, Unit] =
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   300
    {
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   301
      val entries =
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   302
        for ((name, theory) <- theories.toList)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   303
        yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   304
      Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   305
    }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   306
  }
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   307
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   308
  final class Theory private[Thy_Resources](
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   309
    val node_name: Document.Node.Name,
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   310
    val node_header: Document.Node.Header,
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   311
    val text: String,
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   312
    val node_required: Boolean)
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   313
  {
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   314
    override def toString: String = node_name.toString
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   315
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   316
    def node_perspective: Document.Node.Perspective_Text =
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   317
      Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   318
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   319
    def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   320
      List(node_name -> Document.Node.Deps(node_header),
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   321
        node_name -> Document.Node.Edits(text_edits),
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   322
        node_name -> node_perspective)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   323
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   324
    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   325
    {
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   326
      val (text_edits, old_required) =
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   327
        if (old.isEmpty) (Text.Edit.inserts(0, text), false)
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   328
        else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   329
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   330
      if (text_edits.isEmpty && node_required == old_required) Nil
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   331
      else make_edits(text_edits)
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   332
    }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   333
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   334
    def purge_edits: List[Document.Edit_Text] =
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   335
      make_edits(Text.Edit.removes(0, text))
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   336
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   337
    def required(required: Boolean): Theory =
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   338
      if (required == node_required) this
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   339
      else new Theory(node_name, node_header, text, required)
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   340
  }
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   341
}
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   342
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   343
class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   344
  extends Resources(session_base, log = log)
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   345
{
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   346
  resources =>
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   347
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   348
  private val state = Synchronized(Thy_Resources.State())
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   349
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   350
  def load_theories(
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   351
    session: Session,
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   352
    id: UUID,
68894
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   353
    dep_theories: List[Document.Node.Name],
1dbdad1b57a5 more robust: load_theories after consumer is installed;
wenzelm
parents: 68888
diff changeset
   354
    progress: Progress)
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   355
  {
67888
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   356
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   357
    val loaded_theories =
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   358
      for (node_name <- dep_theories)
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   359
      yield {
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   360
        val path = node_name.path
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   361
        if (!node_name.is_theory) error("Not a theory file: " + path)
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   362
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   363
        progress.expose_interrupt()
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   364
        val text = File.read(path)
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   365
        val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   366
        new Thy_Resources.Theory(node_name, node_header, text, true)
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   367
      }
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   368
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   369
    state.change(st =>
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   370
      {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   371
        val st1 = st.insert_required(id, dep_theories)
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   372
        val theory_edits =
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   373
          for (theory <- loaded_theories)
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   374
          yield {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   375
            val node_name = theory.node_name
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   376
            val theory1 = theory.required(st1.is_required(node_name))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   377
            val edits = theory1.node_edits(st1.theories.get(node_name))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   378
            (edits, (node_name, theory1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   379
          }
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   380
        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   381
        st1.update_theories(theory_edits.map(_._2))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   382
      })
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   383
  }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   384
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   385
  def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   386
  {
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   387
    state.change(st =>
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   388
      {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   389
        val st1 = st.remove_required(id, dep_theories)
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   390
        val theory_edits =
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   391
          for {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   392
            node_name <- dep_theories
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   393
            theory <- st1.theories.get(node_name)
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   394
          }
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   395
          yield {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   396
            val theory1 = theory.required(st1.is_required(node_name))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   397
            val edits = theory1.node_edits(Some(theory))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   398
            (edits, (node_name, theory1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   399
          }
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   400
        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   401
        st1.update_theories(theory_edits.map(_._2))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   402
      })
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   403
  }
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   404
68915
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   405
  def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   406
    : (List[Document.Node.Name], List[Document.Node.Name]) =
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   407
  {
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   408
    state.change_result(st =>
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   409
      {
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   410
        val graph = st.theories_graph
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   411
        val all_nodes = graph.topological_order
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   412
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   413
        val purge =
68915
634768c0bd22 tuned signature;
wenzelm
parents: 68914
diff changeset
   414
          (if (nodes.isEmpty) all_nodes else nodes.get.filter(graph.defined(_))).
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   415
            filterNot(st.is_required(_)).toSet
67943
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67940
diff changeset
   416
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67940
diff changeset
   417
        val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67940
diff changeset
   418
        val (retained, purged) = all_nodes.partition(retain)
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   419
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   420
        val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   421
        session.update(Document.Blobs.empty, purge_edits)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   422
67943
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67940
diff changeset
   423
        ((purged, retained), st.remove_theories(purged))
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   424
      })
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   425
  }
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   426
}