src/Pure/Thy/thy_resources.scala
author wenzelm
Sun Sep 02 21:22:52 2018 +0200 (15 months ago ago)
changeset 68883 3653b3ad729e
parent 68771 7e1978b9a4d1
child 68884 9b97d0b20d95
permissions -rw-r--r--
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
     1 /*  Title:      Pure/Thy/thy_resources.scala
     2     Author:     Makarius
     3 
     4 PIDE resources for theory files: load/unload theories via PIDE document updates.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{File => JFile}
    11 
    12 
    13 object 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, Document_Status.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_check_delay: Double = 0.5
    75   val default_nodes_status_delay: Double = -1.0
    76 
    77 
    78   class Session private[Thy_Resources](
    79     session_name: String,
    80     session_options: Options,
    81     override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
    82   {
    83     session =>
    84 
    85     val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
    86     val tmp_dir_name: String = File.path(tmp_dir).implode
    87 
    88     override def toString: String = session_name
    89 
    90     override def stop(): Process_Result =
    91     {
    92       try { super.stop() }
    93       finally { Isabelle_System.rm_tree(tmp_dir) }
    94     }
    95 
    96 
    97     /* theories */
    98 
    99     def use_theories(
   100       theories: List[String],
   101       qualifier: String = Sessions.DRAFT,
   102       master_dir: String = "",
   103       check_delay: Time = Time.seconds(default_check_delay),
   104       check_limit: Int = 0,
   105       nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
   106       id: UUID = UUID(),
   107       progress: Progress = No_Progress): Theories_Result =
   108     {
   109       val dep_theories =
   110         resources.load_theories(session, id, theories, qualifier = qualifier,
   111           master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
   112       val dep_theories_set = dep_theories.toSet
   113 
   114       val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
   115 
   116       val result = Future.promise[Theories_Result]
   117 
   118       def check_state(beyond_limit: Boolean = false)
   119       {
   120         val state = session.current_state()
   121         state.stable_tip_version match {
   122           case Some(version) =>
   123             if (beyond_limit ||
   124                 dep_theories.forall(name =>
   125                   state.node_consolidated(version, name) ||
   126                   nodes_status_update.value._1.is_terminated(name)))
   127             {
   128               val nodes =
   129                 for (name <- dep_theories)
   130                 yield (name -> Document_Status.Node_Status.make(state, version, name))
   131               try { result.fulfill(new Theories_Result(state, version, nodes)) }
   132               catch { case _: IllegalStateException => }
   133             }
   134           case None =>
   135         }
   136       }
   137 
   138       val check_progress =
   139       {
   140         var check_count = 0
   141         Event_Timer.request(Time.now(), repeat = Some(check_delay))
   142           {
   143             if (progress.stopped) result.cancel
   144             else {
   145               check_count += 1
   146               check_state(check_limit > 0 && check_count > check_limit)
   147             }
   148           }
   149       }
   150 
   151       val theories_progress = Synchronized(Set.empty[Document.Node.Name])
   152 
   153       val delay_nodes_status =
   154         Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
   155           val (nodes_status, names) = nodes_status_update.value
   156           progress.nodes_status(names.map(name => (name -> nodes_status(name))))
   157         }
   158 
   159       val consumer =
   160         Session.Consumer[Session.Commands_Changed](getClass.getName) {
   161           case changed =>
   162             if (changed.nodes.exists(dep_theories_set)) {
   163               val snapshot = session.snapshot()
   164               val state = snapshot.state
   165               val version = snapshot.version
   166 
   167               nodes_status_update.change(
   168                 { case upd @ (nodes_status, _) =>
   169                     val domain =
   170                       if (nodes_status.is_empty) dep_theories_set
   171                       else changed.nodes.iterator.filter(dep_theories_set).toSet
   172                     val upd1 =
   173                       nodes_status.update(resources.session_base, state, version,
   174                         domain = Some(domain), trim = changed.assignment).getOrElse(upd)
   175                     if (nodes_status_delay >= Time.zero && upd != upd1)
   176                       delay_nodes_status.invoke
   177 
   178                     upd1
   179                 })
   180 
   181               val check_theories =
   182                 (for {
   183                   command <- changed.commands.iterator
   184                   if dep_theories_set(command.node_name) && command.potentially_initialized
   185                 } yield command.node_name).toSet
   186 
   187               if (check_theories.nonEmpty) {
   188                 val initialized =
   189                   theories_progress.change_result(theories =>
   190                   {
   191                     val initialized =
   192                       (check_theories -- theories).toList.filter(name =>
   193                         Document_Status.Node_Status.make(state, version, name).initialized)
   194                     (initialized, theories ++ initialized)
   195                   })
   196                 initialized.map(_.theory).sorted.foreach(progress.theory("", _))
   197               }
   198 
   199               check_state()
   200             }
   201         }
   202 
   203       try {
   204         session.commands_changed += consumer
   205         result.join_result
   206         check_progress.cancel
   207         session.commands_changed -= consumer
   208       }
   209       finally {
   210         resources.unload_theories(session, id, dep_theories)
   211       }
   212 
   213       result.join
   214     }
   215 
   216     def purge_theories(
   217         theories: List[String],
   218         qualifier: String = Sessions.DRAFT,
   219         master_dir: String = "",
   220         all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
   221       resources.purge_theories(session, theories = theories, qualifier = qualifier,
   222         master_dir = proper_string(master_dir) getOrElse tmp_dir_name, all = all)
   223   }
   224 
   225 
   226   /* internal state */
   227 
   228   sealed case class State(
   229     required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
   230     theories: Map[Document.Node.Name, Theory] = Map.empty)
   231   {
   232     def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
   233 
   234     def insert_required(id: UUID, names: List[Document.Node.Name]): State =
   235       copy(required = (required /: names)(_.insert(_, id)))
   236 
   237     def remove_required(id: UUID, names: List[Document.Node.Name]): State =
   238       copy(required = (required /: names)(_.remove(_, id)))
   239 
   240     def update_theories(update: List[(Document.Node.Name, Theory)]): State =
   241       copy(theories =
   242         (theories /: update)({ case (thys, (name, thy)) =>
   243           thys.get(name) match {
   244             case Some(thy1) if thy1 == thy => thys
   245             case _ => thys + (name -> thy)
   246           }
   247         }))
   248 
   249     def remove_theories(remove: List[Document.Node.Name]): State =
   250     {
   251       require(remove.forall(name => !is_required(name)))
   252       copy(theories = theories -- remove)
   253     }
   254 
   255     lazy val theories_graph: Graph[Document.Node.Name, Unit] =
   256     {
   257       val entries =
   258         for ((name, theory) <- theories.toList)
   259         yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
   260       Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
   261     }
   262   }
   263 
   264   final class Theory private[Thy_Resources](
   265     val node_name: Document.Node.Name,
   266     val node_header: Document.Node.Header,
   267     val text: String,
   268     val node_required: Boolean)
   269   {
   270     override def toString: String = node_name.toString
   271 
   272     def node_perspective: Document.Node.Perspective_Text =
   273       Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
   274 
   275     def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
   276       List(node_name -> Document.Node.Deps(node_header),
   277         node_name -> Document.Node.Edits(text_edits),
   278         node_name -> node_perspective)
   279 
   280     def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
   281     {
   282       val (text_edits, old_required) =
   283         if (old.isEmpty) (Text.Edit.inserts(0, text), false)
   284         else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
   285 
   286       if (text_edits.isEmpty && node_required == old_required) Nil
   287       else make_edits(text_edits)
   288     }
   289 
   290     def purge_edits: List[Document.Edit_Text] =
   291       make_edits(Text.Edit.removes(0, text))
   292 
   293     def required(required: Boolean): Theory =
   294       if (required == node_required) this
   295       else new Theory(node_name, node_header, text, required)
   296   }
   297 }
   298 
   299 class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
   300   extends Resources(session_base, log = log)
   301 {
   302   resources =>
   303 
   304   private val state = Synchronized(Thy_Resources.State())
   305 
   306   def load_theories(
   307     session: Session,
   308     id: UUID,
   309     theories: List[String],
   310     qualifier: String,
   311     master_dir: String,
   312     progress: Progress): List[Document.Node.Name] =
   313   {
   314     val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
   315     val dependencies = resources.dependencies(import_names, progress = progress).check_errors
   316     val dep_theories = dependencies.theories
   317 
   318     val loaded_theories =
   319       for (node_name <- dep_theories)
   320       yield {
   321         val path = node_name.path
   322         if (!node_name.is_theory) error("Not a theory file: " + path)
   323 
   324         progress.expose_interrupt()
   325         val text = File.read(path)
   326         val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
   327         new Thy_Resources.Theory(node_name, node_header, text, true)
   328       }
   329 
   330     state.change(st =>
   331       {
   332         val st1 = st.insert_required(id, dep_theories)
   333         val theory_edits =
   334           for (theory <- loaded_theories)
   335           yield {
   336             val node_name = theory.node_name
   337             val theory1 = theory.required(st1.is_required(node_name))
   338             val edits = theory1.node_edits(st1.theories.get(node_name))
   339             (edits, (node_name, theory1))
   340           }
   341         session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   342         st1.update_theories(theory_edits.map(_._2))
   343       })
   344 
   345     dep_theories
   346   }
   347 
   348   def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
   349   {
   350     state.change(st =>
   351       {
   352         val st1 = st.remove_required(id, dep_theories)
   353         val theory_edits =
   354           for {
   355             node_name <- dep_theories
   356             theory <- st1.theories.get(node_name)
   357           }
   358           yield {
   359             val theory1 = theory.required(st1.is_required(node_name))
   360             val edits = theory1.node_edits(Some(theory))
   361             (edits, (node_name, theory1))
   362           }
   363         session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   364         st1.update_theories(theory_edits.map(_._2))
   365       })
   366   }
   367 
   368   def purge_theories(session: Session,
   369     theories: List[String],
   370     qualifier: String,
   371     master_dir: String,
   372     all: Boolean): (List[Document.Node.Name], List[Document.Node.Name]) =
   373   {
   374     val nodes = theories.map(import_name(qualifier, master_dir, _))
   375 
   376     state.change_result(st =>
   377       {
   378         val graph = st.theories_graph
   379         val all_nodes = graph.topological_order
   380 
   381         val purge =
   382           (if (all) all_nodes else nodes.filter(graph.defined(_))).
   383             filterNot(st.is_required(_)).toSet
   384 
   385         val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet
   386         val (retained, purged) = all_nodes.partition(retain)
   387 
   388         val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
   389         session.update(Document.Blobs.empty, purge_edits)
   390 
   391         ((purged, retained), st.remove_theories(purged))
   392       })
   393   }
   394 }