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