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