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