src/Pure/Thy/thy_resources.scala
author wenzelm
Sun, 03 Jun 2018 20:37:16 +0200
changeset 68365 f9379279f98c
parent 68330 d7920eb7de54
child 68694 03e104be99af
permissions -rw-r--r--
clarified signature: prefer Document.Snapshot;
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,
wenzelm
parents: 67888
diff changeset
    61
    val nodes: List[(Document.Node.Name, Protocol.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
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    74
  class Session private[Thy_Resources](
67945
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
    75
    session_name: String,
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
    76
    session_options: Options,
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
    77
    override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    78
  {
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    79
    session =>
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    80
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    81
    val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
67946
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
    82
    val tmp_dir_name: String = File.path(tmp_dir).implode
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    83
67945
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
    84
    override def toString: String = session_name
984c3dc46cc0 tuned output;
wenzelm
parents: 67943
diff changeset
    85
67925
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    86
    override def stop(): Process_Result =
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    87
    {
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    88
      try { super.stop() }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    89
      finally { Isabelle_System.rm_tree(tmp_dir) }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    90
    }
74dce5658d4c provide tmp_dir for server session;
wenzelm
parents: 67923
diff changeset
    91
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
    92
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
    93
    /* theories */
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
    94
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
    95
    def use_theories(
67940
b4e80f062fbf clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents: 67939
diff changeset
    96
      theories: List[String],
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
    97
      qualifier: String = Sessions.DRAFT,
67881
812ed06dadec interruptible exploration of dependencies;
wenzelm
parents: 67879
diff changeset
    98
      master_dir: String = "",
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
    99
      id: UUID = UUID(),
67881
812ed06dadec interruptible exploration of dependencies;
wenzelm
parents: 67879
diff changeset
   100
      progress: Progress = No_Progress): Theories_Result =
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   101
    {
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   102
      val dep_theories =
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   103
        resources.load_theories(session, id, theories, qualifier = qualifier,
67946
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
   104
          master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   105
67879
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
   106
      val result = Future.promise[Theories_Result]
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   107
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   108
      def check_state
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   109
      {
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   110
        val state = session.current_state()
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   111
        state.stable_tip_version match {
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   112
          case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) =>
67889
wenzelm
parents: 67888
diff changeset
   113
            val nodes =
wenzelm
parents: 67888
diff changeset
   114
              for (name <- dep_theories)
68321
daca5f2a0c90 tuned signature;
wenzelm
parents: 68319
diff changeset
   115
              yield (name -> Protocol.node_status(state, version, name))
68365
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68330
diff changeset
   116
            try { result.fulfill(new Theories_Result(state, version, nodes)) }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   117
            catch { case _: IllegalStateException => }
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   118
          case _ =>
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   119
        }
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   120
      }
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   121
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   122
      val check_progress =
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   123
        Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   124
          { if (progress.stopped) result.cancel else check_state }
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   125
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   126
      val theories_progress = Synchronized(Set.empty[Document.Node.Name])
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   127
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   128
      val consumer =
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   129
        Session.Consumer[Session.Commands_Changed](getClass.getName) {
68330
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   130
          case changed =>
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   131
            if (dep_theories.exists(changed.nodes)) {
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   132
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   133
              val check_theories =
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   134
                (for (command <- changed.commands.iterator if command.potentially_initialized)
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   135
                  yield command.node_name).toSet
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   136
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   137
              if (check_theories.nonEmpty) {
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   138
                val snapshot = session.snapshot()
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   139
                val initialized =
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   140
                  theories_progress.change_result(theories =>
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   141
                  {
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   142
                    val initialized =
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   143
                      (check_theories -- theories).toList.filter(name =>
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   144
                        Protocol.node_status(snapshot.state, snapshot.version, name).initialized)
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   145
                    (initialized, theories ++ initialized)
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   146
                  })
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   147
                initialized.map(_.theory).sorted.foreach(progress.theory("", _))
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   148
              }
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   149
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   150
              check_state
d7920eb7de54 report theory progress via PIDE node status;
wenzelm
parents: 68321
diff changeset
   151
            }
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   152
        }
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   153
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   154
      try {
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   155
        session.commands_changed += consumer
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   156
        result.join_result
67894
fee080c4045f more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents: 67893
diff changeset
   157
        check_progress.cancel
67892
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   158
        session.commands_changed -= consumer
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   159
      }
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   160
      finally {
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   161
        resources.unload_theories(session, id, dep_theories)
25e2b621bdcb more interruptible use_theories;
wenzelm
parents: 67889
diff changeset
   162
      }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   163
67879
e4903b803b8b clarified signature;
wenzelm
parents: 67877
diff changeset
   164
      result.join
67064
fb487246ef4f synchronous use_theories, based on consolidated_state;
wenzelm
parents: 67063
diff changeset
   165
    }
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   166
67939
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   167
    def purge_theories(
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   168
        theories: List[String],
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   169
        qualifier: String = Sessions.DRAFT,
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   170
        master_dir: String = "",
67943
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67940
diff changeset
   171
        all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
67939
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   172
      resources.purge_theories(session, theories = theories, qualifier = qualifier,
67946
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
   173
        master_dir = proper_string(master_dir) getOrElse tmp_dir_name, all = all)
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
   174
  }
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
   175
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
   176
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   177
  /* internal state */
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   178
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   179
  sealed case class State(
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   180
    required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   181
    theories: Map[Document.Node.Name, Theory] = Map.empty)
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   182
  {
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   183
    def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   184
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   185
    def insert_required(id: UUID, names: List[Document.Node.Name]): State =
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   186
      copy(required = (required /: names)(_.insert(_, id)))
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   187
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   188
    def remove_required(id: UUID, names: List[Document.Node.Name]): State =
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   189
      copy(required = (required /: names)(_.remove(_, id)))
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   190
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   191
    def update_theories(update: List[(Document.Node.Name, Theory)]): State =
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   192
      copy(theories =
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   193
        (theories /: update)({ case (thys, (name, thy)) =>
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   194
          thys.get(name) match {
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   195
            case Some(thy1) if thy1 == thy => thys
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   196
            case _ => thys + (name -> thy)
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   197
          }
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   198
        }))
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   199
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   200
    def remove_theories(remove: List[Document.Node.Name]): State =
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   201
    {
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   202
      require(remove.forall(name => !is_required(name)))
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   203
      copy(theories = theories -- remove)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   204
    }
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   205
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   206
    lazy val theories_graph: Graph[Document.Node.Name, Unit] =
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   207
    {
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   208
      val entries =
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   209
        for ((name, theory) <- theories.toList)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   210
        yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   211
      Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   212
    }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   213
  }
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   214
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   215
  final class Theory private[Thy_Resources](
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   216
    val node_name: Document.Node.Name,
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   217
    val node_header: Document.Node.Header,
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   218
    val text: String,
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   219
    val node_required: Boolean)
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   220
  {
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   221
    override def toString: String = node_name.toString
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   222
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   223
    def node_perspective: Document.Node.Perspective_Text =
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   224
      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
   225
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   226
    def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   227
      List(node_name -> Document.Node.Deps(node_header),
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   228
        node_name -> Document.Node.Edits(text_edits),
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   229
        node_name -> node_perspective)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   230
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   231
    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   232
    {
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   233
      val (text_edits, old_required) =
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   234
        if (old.isEmpty) (Text.Edit.inserts(0, text), false)
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   235
        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
   236
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   237
      if (text_edits.isEmpty && node_required == old_required) Nil
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   238
      else make_edits(text_edits)
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   239
    }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   240
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   241
    def purge_edits: List[Document.Edit_Text] =
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   242
      make_edits(Text.Edit.removes(0, text))
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   243
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   244
    def required(required: Boolean): Theory =
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   245
      if (required == node_required) this
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   246
      else new Theory(node_name, node_header, text, required)
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   247
  }
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   248
}
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   249
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   250
class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   251
  extends Resources(session_base, log = log)
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   252
{
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   253
  resources =>
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   254
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   255
  private val state = Synchronized(Thy_Resources.State())
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   256
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   257
  def load_theories(
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   258
    session: Session,
67885
839a624aabb9 prefer typed UUID;
wenzelm
parents: 67884
diff changeset
   259
    id: UUID,
67940
b4e80f062fbf clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents: 67939
diff changeset
   260
    theories: List[String],
67946
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
   261
    qualifier: String,
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
   262
    master_dir: String,
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
   263
    progress: Progress): List[Document.Node.Name] =
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   264
  {
67940
b4e80f062fbf clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents: 67939
diff changeset
   265
    val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
67881
812ed06dadec interruptible exploration of dependencies;
wenzelm
parents: 67879
diff changeset
   266
    val dependencies = resources.dependencies(import_names, progress = progress).check_errors
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   267
    val dep_theories = dependencies.theories
67888
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   268
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   269
    val loaded_theories =
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   270
      for (node_name <- dep_theories)
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   271
      yield {
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   272
        val path = node_name.path
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   273
        if (!node_name.is_theory) error("Not a theory file: " + path)
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   274
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   275
        progress.expose_interrupt()
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   276
        val text = File.read(path)
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   277
        val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   278
        new Thy_Resources.Theory(node_name, node_header, text, true)
3bf62a6e50e7 more interruptible;
wenzelm
parents: 67887
diff changeset
   279
      }
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   280
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   281
    state.change(st =>
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   282
      {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   283
        val st1 = st.insert_required(id, dep_theories)
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   284
        val theory_edits =
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   285
          for (theory <- loaded_theories)
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   286
          yield {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   287
            val node_name = theory.node_name
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   288
            val theory1 = theory.required(st1.is_required(node_name))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   289
            val edits = theory1.node_edits(st1.theories.get(node_name))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   290
            (edits, (node_name, theory1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   291
          }
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   292
        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   293
        st1.update_theories(theory_edits.map(_._2))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   294
      })
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   295
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   296
    dep_theories
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   297
  }
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   298
67887
a4d5342898b1 unload_theories: actually observe required state;
wenzelm
parents: 67885
diff changeset
   299
  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
   300
  {
67893
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   301
    state.change(st =>
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   302
      {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   303
        val st1 = st.remove_required(id, dep_theories)
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   304
        val theory_edits =
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   305
          for {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   306
            node_name <- dep_theories
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   307
            theory <- st1.theories.get(node_name)
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   308
          }
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   309
          yield {
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   310
            val theory1 = theory.required(st1.is_required(node_name))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   311
            val edits = theory1.node_edits(Some(theory))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   312
            (edits, (node_name, theory1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   313
          }
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   314
        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   315
        st1.update_theories(theory_edits.map(_._2))
c854e50c2114 synchronized Session.update;
wenzelm
parents: 67892
diff changeset
   316
      })
67884
43af581d7d8e unload_theories after consolidation -- reset node_required;
wenzelm
parents: 67883
diff changeset
   317
  }
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   318
67939
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   319
  def purge_theories(session: Session,
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   320
    theories: List[String],
67946
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
   321
    qualifier: String,
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
   322
    master_dir: String,
e1e57c288e45 session tmp_dir is default master_dir;
wenzelm
parents: 67945
diff changeset
   323
    all: Boolean): (List[Document.Node.Name], List[Document.Node.Name]) =
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   324
  {
67939
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   325
    val nodes = theories.map(import_name(qualifier, master_dir, _))
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   326
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   327
    state.change_result(st =>
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   328
      {
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   329
        val graph = st.theories_graph
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   330
        val all_nodes = graph.topological_order
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   331
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   332
        val purge =
67939
544a7a21298e clarified signature -- more like use_theories;
wenzelm
parents: 67936
diff changeset
   333
          (if (all) all_nodes else nodes.filter(graph.defined(_))).
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   334
            filterNot(st.is_required(_)).toSet
67943
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67940
diff changeset
   335
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67940
diff changeset
   336
        val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67940
diff changeset
   337
        val (retained, purged) = all_nodes.partition(retain)
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   338
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   339
        val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   340
        session.update(Document.Blobs.empty, purge_edits)
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   341
67943
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67940
diff changeset
   342
        ((purged, retained), st.remove_theories(purged))
67936
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   343
      })
141a93b93aa6 support for purge_theories;
wenzelm
parents: 67925
diff changeset
   344
  }
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   345
}