1/*  Title:      Pure/Thy/thy_resources.scala
2    Author:     Makarius
3
4PIDE resources for theory files: load/unload theories via PIDE document updates.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile}
11
12
13object Thy_Resources
14{
15  /* PIDE session */
16
17  def start_session(
18    options: Options,
19    session_name: String,
20    session_dirs: List[Path] = Nil,
21    include_sessions: List[String] = Nil,
22    session_base: Option[Sessions.Base] = None,
23    print_mode: List[String] = Nil,
24    progress: Progress = No_Progress,
25    log: Logger = No_Logger): Session =
26  {
27    val base =
28      session_base getOrElse
29        Sessions.base_info(options, session_name, include_sessions = include_sessions,
30          progress = progress, dirs = session_dirs).check_base
31    val resources = new Thy_Resources(base, log = log)
32    val session = new Session(session_name, options, resources)
33
34    val session_error = Future.promise[String]
35    var session_phase: Session.Consumer[Session.Phase] = null
36    session_phase =
37      Session.Consumer(getClass.getName) {
38        case Session.Ready =>
39          session.phase_changed -= session_phase
40          session_error.fulfill("")
41        case Session.Terminated(result) if !result.ok =>
42          session.phase_changed -= session_phase
43          session_error.fulfill("Session start failed: return code " + result.rc)
44        case _ =>
45      }
46    session.phase_changed += session_phase
47
48    progress.echo("Starting " + session_name + " ...")
49    Isabelle_Process.start(session, options,
50      logic = session_name, dirs = session_dirs, modes = print_mode)
51
52    session_error.join match {
53      case "" => session
54      case msg => session.stop(); error(msg)
55    }
56  }
57
58  class Theories_Result private[Thy_Resources](
59    val state: Document.State,
60    val version: Document.Version,
61    val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
62  {
63    def node_names: List[Document.Node.Name] = nodes.map(_._1)
64    def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
65
66    def snapshot(node_name: Document.Node.Name): Document.Snapshot =
67    {
68      val snapshot = state.snapshot(node_name)
69      assert(version.id == snapshot.version.id)
70      snapshot
71    }
72  }
73
74  val default_use_theories_check_delay: Double = 0.5
75
76
77  class Session private[Thy_Resources](
78    session_name: String,
79    session_options: Options,
80    override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
81  {
82    session =>
83
84    val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
85    val tmp_dir_name: String = File.path(tmp_dir).implode
86
87    override def toString: String = session_name
88
89    override def stop(): Process_Result =
90    {
91      try { super.stop() }
92      finally { Isabelle_System.rm_tree(tmp_dir) }
93    }
94
95
96    /* theories */
97
98    def use_theories(
99      theories: List[String],
100      qualifier: String = Sessions.DRAFT,
101      master_dir: String = "",
102      check_delay: Time = Time.seconds(default_use_theories_check_delay),
103      check_limit: Int = 0,
104      id: UUID = UUID(),
105      progress: Progress = No_Progress): Theories_Result =
106    {
107      val dep_theories =
108        resources.load_theories(session, id, theories, qualifier = qualifier,
109          master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
110
111      val result = Future.promise[Theories_Result]
112
113      def check_state(beyond_limit: Boolean = false)
114      {
115        val state = session.current_state()
116        state.stable_tip_version match {
117          case Some(version) =>
118            if (beyond_limit || dep_theories.forall(state.node_consolidated(version, _))) {
119              val nodes =
120                for (name <- dep_theories)
121                yield (name -> Protocol.node_status(state, version, name))
122              try { result.fulfill(new Theories_Result(state, version, nodes)) }
123              catch { case _: IllegalStateException => }
124            }
125          case None =>
126        }
127      }
128
129      val check_progress =
130      {
131        var check_count = 0
132        Event_Timer.request(Time.now(), repeat = Some(check_delay))
133          {
134            if (progress.stopped) result.cancel
135            else {
136              check_count += 1
137              check_state(check_limit > 0 && check_count > check_limit)
138            }
139          }
140      }
141
142      val theories_progress = Synchronized(Set.empty[Document.Node.Name])
143
144      val consumer =
145        Session.Consumer[Session.Commands_Changed](getClass.getName) {
146          case changed =>
147            if (dep_theories.exists(changed.nodes)) {
148
149              val check_theories =
150                (for (command <- changed.commands.iterator if command.potentially_initialized)
151                  yield command.node_name).toSet
152
153              if (check_theories.nonEmpty) {
154                val snapshot = session.snapshot()
155                val initialized =
156                  theories_progress.change_result(theories =>
157                  {
158                    val initialized =
159                      (check_theories -- theories).toList.filter(name =>
160                        Protocol.node_status(snapshot.state, snapshot.version, name).initialized)
161                    (initialized, theories ++ initialized)
162                  })
163                initialized.map(_.theory).sorted.foreach(progress.theory("", _))
164              }
165
166              check_state()
167            }
168        }
169
170      try {
171        session.commands_changed += consumer
172        result.join_result
173        check_progress.cancel
174        session.commands_changed -= consumer
175      }
176      finally {
177        resources.unload_theories(session, id, dep_theories)
178      }
179
180      result.join
181    }
182
183    def purge_theories(
184        theories: List[String],
185        qualifier: String = Sessions.DRAFT,
186        master_dir: String = "",
187        all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
188      resources.purge_theories(session, theories = theories, qualifier = qualifier,
189        master_dir = proper_string(master_dir) getOrElse tmp_dir_name, all = all)
190  }
191
192
193  /* internal state */
194
195  sealed case class State(
196    required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
197    theories: Map[Document.Node.Name, Theory] = Map.empty)
198  {
199    def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
200
201    def insert_required(id: UUID, names: List[Document.Node.Name]): State =
202      copy(required = (required /: names)(_.insert(_, id)))
203
204    def remove_required(id: UUID, names: List[Document.Node.Name]): State =
205      copy(required = (required /: names)(_.remove(_, id)))
206
207    def update_theories(update: List[(Document.Node.Name, Theory)]): State =
208      copy(theories =
209        (theories /: update)({ case (thys, (name, thy)) =>
210          thys.get(name) match {
211            case Some(thy1) if thy1 == thy => thys
212            case _ => thys + (name -> thy)
213          }
214        }))
215
216    def remove_theories(remove: List[Document.Node.Name]): State =
217    {
218      require(remove.forall(name => !is_required(name)))
219      copy(theories = theories -- remove)
220    }
221
222    lazy val theories_graph: Graph[Document.Node.Name, Unit] =
223    {
224      val entries =
225        for ((name, theory) <- theories.toList)
226        yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
227      Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
228    }
229  }
230
231  final class Theory private[Thy_Resources](
232    val node_name: Document.Node.Name,
233    val node_header: Document.Node.Header,
234    val text: String,
235    val node_required: Boolean)
236  {
237    override def toString: String = node_name.toString
238
239    def node_perspective: Document.Node.Perspective_Text =
240      Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
241
242    def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
243      List(node_name -> Document.Node.Deps(node_header),
244        node_name -> Document.Node.Edits(text_edits),
245        node_name -> node_perspective)
246
247    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
248    {
249      val (text_edits, old_required) =
250        if (old.isEmpty) (Text.Edit.inserts(0, text), false)
251        else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
252
253      if (text_edits.isEmpty && node_required == old_required) Nil
254      else make_edits(text_edits)
255    }
256
257    def purge_edits: List[Document.Edit_Text] =
258      make_edits(Text.Edit.removes(0, text))
259
260    def required(required: Boolean): Theory =
261      if (required == node_required) this
262      else new Theory(node_name, node_header, text, required)
263  }
264}
265
266class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
267  extends Resources(session_base, log = log)
268{
269  resources =>
270
271  private val state = Synchronized(Thy_Resources.State())
272
273  def load_theories(
274    session: Session,
275    id: UUID,
276    theories: List[String],
277    qualifier: String,
278    master_dir: String,
279    progress: Progress): List[Document.Node.Name] =
280  {
281    val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
282    val dependencies = resources.dependencies(import_names, progress = progress).check_errors
283    val dep_theories = dependencies.theories
284
285    val loaded_theories =
286      for (node_name <- dep_theories)
287      yield {
288        val path = node_name.path
289        if (!node_name.is_theory) error("Not a theory file: " + path)
290
291        progress.expose_interrupt()
292        val text = File.read(path)
293        val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
294        new Thy_Resources.Theory(node_name, node_header, text, true)
295      }
296
297    state.change(st =>
298      {
299        val st1 = st.insert_required(id, dep_theories)
300        val theory_edits =
301          for (theory <- loaded_theories)
302          yield {
303            val node_name = theory.node_name
304            val theory1 = theory.required(st1.is_required(node_name))
305            val edits = theory1.node_edits(st1.theories.get(node_name))
306            (edits, (node_name, theory1))
307          }
308        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
309        st1.update_theories(theory_edits.map(_._2))
310      })
311
312    dep_theories
313  }
314
315  def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
316  {
317    state.change(st =>
318      {
319        val st1 = st.remove_required(id, dep_theories)
320        val theory_edits =
321          for {
322            node_name <- dep_theories
323            theory <- st1.theories.get(node_name)
324          }
325          yield {
326            val theory1 = theory.required(st1.is_required(node_name))
327            val edits = theory1.node_edits(Some(theory))
328            (edits, (node_name, theory1))
329          }
330        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
331        st1.update_theories(theory_edits.map(_._2))
332      })
333  }
334
335  def purge_theories(session: Session,
336    theories: List[String],
337    qualifier: String,
338    master_dir: String,
339    all: Boolean): (List[Document.Node.Name], List[Document.Node.Name]) =
340  {
341    val nodes = theories.map(import_name(qualifier, master_dir, _))
342
343    state.change_result(st =>
344      {
345        val graph = st.theories_graph
346        val all_nodes = graph.topological_order
347
348        val purge =
349          (if (all) all_nodes else nodes.filter(graph.defined(_))).
350            filterNot(st.is_required(_)).toSet
351
352        val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet
353        val (retained, purged) = all_nodes.partition(retain)
354
355        val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
356        session.update(Document.Blobs.empty, purge_edits)
357
358        ((purged, retained), st.remove_theories(purged))
359      })
360  }
361}
362