src/Pure/Thy/thy_resources.scala
author wenzelm
Sat Mar 24 22:45:06 2018 +0100 (13 months ago)
changeset 67948 83902fff6243
parent 67946 e1e57c288e45
child 68106 a514e29db980
permissions -rw-r--r--
clarified 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@67879
    58
  sealed case class Theories_Result(
wenzelm@67883
    59
    val state: Document.State,
wenzelm@67889
    60
    val version: Document.Version,
wenzelm@67889
    61
    val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
wenzelm@67879
    62
  {
wenzelm@67883
    63
    def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
wenzelm@67897
    64
wenzelm@67897
    65
    def messages(node_name: Document.Node.Name): List[(XML.Tree, Position.T)] =
wenzelm@67897
    66
    {
wenzelm@67897
    67
      val node = version.nodes(node_name)
wenzelm@67897
    68
      (for {
wenzelm@67897
    69
        (command, start) <-
wenzelm@67897
    70
          Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
wenzelm@67897
    71
        pos = command.span.keyword_pos(start).position(command.span.name)
wenzelm@67897
    72
        (_, tree) <- state.command_results(version, command).iterator
wenzelm@67897
    73
       } yield (tree, pos)).toList
wenzelm@67897
    74
    }
wenzelm@67879
    75
  }
wenzelm@67879
    76
wenzelm@67063
    77
  class Session private[Thy_Resources](
wenzelm@67945
    78
    session_name: String,
wenzelm@67064
    79
    session_options: Options,
wenzelm@67064
    80
    override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
wenzelm@67063
    81
  {
wenzelm@67063
    82
    session =>
wenzelm@67063
    83
wenzelm@67925
    84
    val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
wenzelm@67946
    85
    val tmp_dir_name: String = File.path(tmp_dir).implode
wenzelm@67925
    86
wenzelm@67945
    87
    override def toString: String = session_name
wenzelm@67945
    88
wenzelm@67925
    89
    override def stop(): Process_Result =
wenzelm@67925
    90
    {
wenzelm@67925
    91
      try { super.stop() }
wenzelm@67925
    92
      finally { Isabelle_System.rm_tree(tmp_dir) }
wenzelm@67925
    93
    }
wenzelm@67925
    94
wenzelm@67936
    95
wenzelm@67936
    96
    /* theories */
wenzelm@67936
    97
wenzelm@67064
    98
    def use_theories(
wenzelm@67940
    99
      theories: List[String],
wenzelm@67064
   100
      qualifier: String = Sessions.DRAFT,
wenzelm@67881
   101
      master_dir: String = "",
wenzelm@67885
   102
      id: UUID = UUID(),
wenzelm@67881
   103
      progress: Progress = No_Progress): Theories_Result =
wenzelm@67064
   104
    {
wenzelm@67887
   105
      val dep_theories =
wenzelm@67884
   106
        resources.load_theories(session, id, theories, qualifier = qualifier,
wenzelm@67946
   107
          master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
wenzelm@67064
   108
wenzelm@67879
   109
      val result = Future.promise[Theories_Result]
wenzelm@67064
   110
wenzelm@67064
   111
      def check_state
wenzelm@67064
   112
      {
wenzelm@67064
   113
        val state = session.current_state()
wenzelm@67064
   114
        state.stable_tip_version match {
wenzelm@67887
   115
          case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) =>
wenzelm@67889
   116
            val nodes =
wenzelm@67889
   117
              for (name <- dep_theories)
wenzelm@67889
   118
              yield (name -> Protocol.node_status(state, version, name, version.nodes(name)))
wenzelm@67889
   119
            try { result.fulfill(Theories_Result(state, version, nodes)) }
wenzelm@67064
   120
            catch { case _: IllegalStateException => }
wenzelm@67064
   121
          case _ =>
wenzelm@67064
   122
        }
wenzelm@67064
   123
      }
wenzelm@67064
   124
wenzelm@67894
   125
      val check_progress =
wenzelm@67894
   126
        Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
wenzelm@67894
   127
          { if (progress.stopped) result.cancel else check_state }
wenzelm@67894
   128
wenzelm@67064
   129
      val consumer =
wenzelm@67064
   130
        Session.Consumer[Session.Commands_Changed](getClass.getName) {
wenzelm@67887
   131
          case changed => if (dep_theories.exists(changed.nodes)) check_state
wenzelm@67064
   132
        }
wenzelm@67064
   133
wenzelm@67892
   134
      try {
wenzelm@67892
   135
        session.commands_changed += consumer
wenzelm@67892
   136
        result.join_result
wenzelm@67894
   137
        check_progress.cancel
wenzelm@67892
   138
        session.commands_changed -= consumer
wenzelm@67892
   139
      }
wenzelm@67892
   140
      finally {
wenzelm@67892
   141
        resources.unload_theories(session, id, dep_theories)
wenzelm@67892
   142
      }
wenzelm@67884
   143
wenzelm@67879
   144
      result.join
wenzelm@67064
   145
    }
wenzelm@67936
   146
wenzelm@67939
   147
    def purge_theories(
wenzelm@67939
   148
        theories: List[String],
wenzelm@67939
   149
        qualifier: String = Sessions.DRAFT,
wenzelm@67939
   150
        master_dir: String = "",
wenzelm@67943
   151
        all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
wenzelm@67939
   152
      resources.purge_theories(session, theories = theories, qualifier = qualifier,
wenzelm@67946
   153
        master_dir = proper_string(master_dir) getOrElse tmp_dir_name, all = all)
wenzelm@67063
   154
  }
wenzelm@67063
   155
wenzelm@67061
   156
wenzelm@67054
   157
  /* internal state */
wenzelm@67054
   158
wenzelm@67884
   159
  sealed case class State(
wenzelm@67887
   160
    required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
wenzelm@67887
   161
    theories: Map[Document.Node.Name, Theory] = Map.empty)
wenzelm@67884
   162
  {
wenzelm@67887
   163
    def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
wenzelm@67887
   164
wenzelm@67887
   165
    def insert_required(id: UUID, names: List[Document.Node.Name]): State =
wenzelm@67887
   166
      copy(required = (required /: names)(_.insert(_, id)))
wenzelm@67887
   167
wenzelm@67887
   168
    def remove_required(id: UUID, names: List[Document.Node.Name]): State =
wenzelm@67887
   169
      copy(required = (required /: names)(_.remove(_, id)))
wenzelm@67887
   170
wenzelm@67887
   171
    def update_theories(update: List[(Document.Node.Name, Theory)]): State =
wenzelm@67887
   172
      copy(theories =
wenzelm@67887
   173
        (theories /: update)({ case (thys, (name, thy)) =>
wenzelm@67887
   174
          thys.get(name) match {
wenzelm@67887
   175
            case Some(thy1) if thy1 == thy => thys
wenzelm@67887
   176
            case _ => thys + (name -> thy)
wenzelm@67887
   177
          }
wenzelm@67887
   178
        }))
wenzelm@67936
   179
wenzelm@67936
   180
    def remove_theories(remove: List[Document.Node.Name]): State =
wenzelm@67936
   181
    {
wenzelm@67936
   182
      require(remove.forall(name => !is_required(name)))
wenzelm@67936
   183
      copy(theories = theories -- remove)
wenzelm@67936
   184
    }
wenzelm@67936
   185
wenzelm@67936
   186
    lazy val theories_graph: Graph[Document.Node.Name, Unit] =
wenzelm@67936
   187
    {
wenzelm@67936
   188
      val entries =
wenzelm@67936
   189
        for ((name, theory) <- theories.toList)
wenzelm@67936
   190
        yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
wenzelm@67936
   191
      Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
wenzelm@67936
   192
    }
wenzelm@67884
   193
  }
wenzelm@67058
   194
wenzelm@67058
   195
  final class Theory private[Thy_Resources](
wenzelm@67058
   196
    val node_name: Document.Node.Name,
wenzelm@67058
   197
    val node_header: Document.Node.Header,
wenzelm@67884
   198
    val text: String,
wenzelm@67884
   199
    val node_required: Boolean)
wenzelm@67056
   200
  {
wenzelm@67058
   201
    override def toString: String = node_name.toString
wenzelm@67058
   202
wenzelm@67058
   203
    def node_perspective: Document.Node.Perspective_Text =
wenzelm@67884
   204
      Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
wenzelm@67058
   205
wenzelm@67936
   206
    def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
wenzelm@67936
   207
      List(node_name -> Document.Node.Deps(node_header),
wenzelm@67936
   208
        node_name -> Document.Node.Edits(text_edits),
wenzelm@67936
   209
        node_name -> node_perspective)
wenzelm@67936
   210
wenzelm@67058
   211
    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
wenzelm@67058
   212
    {
wenzelm@67884
   213
      val (text_edits, old_required) =
wenzelm@67884
   214
        if (old.isEmpty) (Text.Edit.inserts(0, text), false)
wenzelm@67884
   215
        else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
wenzelm@67058
   216
wenzelm@67884
   217
      if (text_edits.isEmpty && node_required == old_required) Nil
wenzelm@67936
   218
      else make_edits(text_edits)
wenzelm@67058
   219
    }
wenzelm@67884
   220
wenzelm@67936
   221
    def purge_edits: List[Document.Edit_Text] =
wenzelm@67936
   222
      make_edits(Text.Edit.removes(0, text))
wenzelm@67936
   223
wenzelm@67887
   224
    def required(required: Boolean): Theory =
wenzelm@67887
   225
      if (required == node_required) this
wenzelm@67887
   226
      else new Theory(node_name, node_header, text, required)
wenzelm@67056
   227
  }
wenzelm@67054
   228
}
wenzelm@67054
   229
wenzelm@67056
   230
class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
wenzelm@67054
   231
  extends Resources(session_base, log = log)
wenzelm@67054
   232
{
wenzelm@67056
   233
  resources =>
wenzelm@67056
   234
wenzelm@67054
   235
  private val state = Synchronized(Thy_Resources.State())
wenzelm@67056
   236
wenzelm@67056
   237
  def load_theories(
wenzelm@67056
   238
    session: Session,
wenzelm@67885
   239
    id: UUID,
wenzelm@67940
   240
    theories: List[String],
wenzelm@67946
   241
    qualifier: String,
wenzelm@67946
   242
    master_dir: String,
wenzelm@67946
   243
    progress: Progress): List[Document.Node.Name] =
wenzelm@67056
   244
  {
wenzelm@67940
   245
    val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
wenzelm@67881
   246
    val dependencies = resources.dependencies(import_names, progress = progress).check_errors
wenzelm@67887
   247
    val dep_theories = dependencies.theories
wenzelm@67888
   248
wenzelm@67888
   249
    val loaded_theories =
wenzelm@67888
   250
      for (node_name <- dep_theories)
wenzelm@67888
   251
      yield {
wenzelm@67888
   252
        val path = node_name.path
wenzelm@67888
   253
        if (!node_name.is_theory) error("Not a theory file: " + path)
wenzelm@67888
   254
wenzelm@67888
   255
        progress.expose_interrupt()
wenzelm@67888
   256
        val text = File.read(path)
wenzelm@67888
   257
        val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
wenzelm@67888
   258
        new Thy_Resources.Theory(node_name, node_header, text, true)
wenzelm@67888
   259
      }
wenzelm@67056
   260
wenzelm@67893
   261
    state.change(st =>
wenzelm@67893
   262
      {
wenzelm@67893
   263
        val st1 = st.insert_required(id, dep_theories)
wenzelm@67893
   264
        val theory_edits =
wenzelm@67893
   265
          for (theory <- loaded_theories)
wenzelm@67893
   266
          yield {
wenzelm@67893
   267
            val node_name = theory.node_name
wenzelm@67893
   268
            val theory1 = theory.required(st1.is_required(node_name))
wenzelm@67893
   269
            val edits = theory1.node_edits(st1.theories.get(node_name))
wenzelm@67893
   270
            (edits, (node_name, theory1))
wenzelm@67893
   271
          }
wenzelm@67893
   272
        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
wenzelm@67893
   273
        st1.update_theories(theory_edits.map(_._2))
wenzelm@67893
   274
      })
wenzelm@67056
   275
wenzelm@67887
   276
    dep_theories
wenzelm@67056
   277
  }
wenzelm@67884
   278
wenzelm@67887
   279
  def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
wenzelm@67884
   280
  {
wenzelm@67893
   281
    state.change(st =>
wenzelm@67893
   282
      {
wenzelm@67893
   283
        val st1 = st.remove_required(id, dep_theories)
wenzelm@67893
   284
        val theory_edits =
wenzelm@67893
   285
          for {
wenzelm@67893
   286
            node_name <- dep_theories
wenzelm@67893
   287
            theory <- st1.theories.get(node_name)
wenzelm@67893
   288
          }
wenzelm@67893
   289
          yield {
wenzelm@67893
   290
            val theory1 = theory.required(st1.is_required(node_name))
wenzelm@67893
   291
            val edits = theory1.node_edits(Some(theory))
wenzelm@67893
   292
            (edits, (node_name, theory1))
wenzelm@67893
   293
          }
wenzelm@67893
   294
        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
wenzelm@67893
   295
        st1.update_theories(theory_edits.map(_._2))
wenzelm@67893
   296
      })
wenzelm@67884
   297
  }
wenzelm@67936
   298
wenzelm@67939
   299
  def purge_theories(session: Session,
wenzelm@67939
   300
    theories: List[String],
wenzelm@67946
   301
    qualifier: String,
wenzelm@67946
   302
    master_dir: String,
wenzelm@67946
   303
    all: Boolean): (List[Document.Node.Name], List[Document.Node.Name]) =
wenzelm@67936
   304
  {
wenzelm@67939
   305
    val nodes = theories.map(import_name(qualifier, master_dir, _))
wenzelm@67939
   306
wenzelm@67936
   307
    state.change_result(st =>
wenzelm@67936
   308
      {
wenzelm@67936
   309
        val graph = st.theories_graph
wenzelm@67936
   310
        val all_nodes = graph.topological_order
wenzelm@67936
   311
wenzelm@67936
   312
        val purge =
wenzelm@67939
   313
          (if (all) all_nodes else nodes.filter(graph.defined(_))).
wenzelm@67936
   314
            filterNot(st.is_required(_)).toSet
wenzelm@67943
   315
wenzelm@67943
   316
        val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet
wenzelm@67943
   317
        val (retained, purged) = all_nodes.partition(retain)
wenzelm@67936
   318
wenzelm@67936
   319
        val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
wenzelm@67936
   320
        session.update(Document.Blobs.empty, purge_edits)
wenzelm@67936
   321
wenzelm@67943
   322
        ((purged, retained), st.remove_theories(purged))
wenzelm@67936
   323
      })
wenzelm@67936
   324
  }
wenzelm@67054
   325
}