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;
     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     private sealed case class Use_Theories_State(
   100       last_update: Time = Time.now(),
   101       nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
   102       already_initialized: Set[Document.Node.Name] = Set.empty)
   103     {
   104       def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
   105         copy(last_update = Time.now(), nodes_status = new_nodes_status)
   106 
   107       def watchdog(watchdog_timeout: Time): Boolean =
   108         watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
   109 
   110       def initialized_theories(
   111         state: Document.State,
   112         version: Document.Version,
   113         new_theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) =
   114       {
   115         val initialized =
   116           for {
   117             name <- new_theories
   118             if !already_initialized(name) &&
   119               Document_Status.Node_Status.make(state, version, name).initialized
   120           } yield name
   121         (initialized, copy(already_initialized = already_initialized ++ initialized))
   122       }
   123     }
   124 
   125     def use_theories(
   126       theories: List[String],
   127       qualifier: String = Sessions.DRAFT,
   128       master_dir: String = "",
   129       check_delay: Time = Time.seconds(default_check_delay),
   130       check_limit: Int = 0,
   131       watchdog_timeout: Time = Time.zero,
   132       nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
   133       id: UUID = UUID(),
   134       progress: Progress = No_Progress): Theories_Result =
   135     {
   136       val dep_theories =
   137       {
   138         val master = proper_string(master_dir) getOrElse tmp_dir_name
   139         val import_names =
   140           theories.map(thy => resources.import_name(qualifier, master, thy) -> Position.none)
   141         resources.dependencies(import_names, progress = progress).check_errors.theories
   142       }
   143       val dep_theories_set = dep_theories.toSet
   144 
   145       val use_theories_state = Synchronized(Use_Theories_State())
   146       val result = Future.promise[Theories_Result]
   147 
   148       def check_state(beyond_limit: Boolean = false)
   149       {
   150         val state = session.current_state()
   151         state.stable_tip_version match {
   152           case Some(version) =>
   153             val st = use_theories_state.value
   154             if (beyond_limit || st.watchdog(watchdog_timeout) ||
   155                 dep_theories.forall(name =>
   156                   state.node_consolidated(version, name) ||
   157                   st.nodes_status.quasi_consolidated(name)))
   158             {
   159               val nodes =
   160                 for (name <- dep_theories)
   161                 yield (name -> Document_Status.Node_Status.make(state, version, name))
   162               try { result.fulfill(new Theories_Result(state, version, nodes)) }
   163               catch { case _: IllegalStateException => }
   164             }
   165           case None =>
   166         }
   167       }
   168 
   169       val check_progress =
   170       {
   171         var check_count = 0
   172         Event_Timer.request(Time.now(), repeat = Some(check_delay))
   173           {
   174             if (progress.stopped) result.cancel
   175             else {
   176               check_count += 1
   177               check_state(check_limit > 0 && check_count > check_limit)
   178             }
   179           }
   180       }
   181 
   182       val consumer =
   183       {
   184         val delay_nodes_status =
   185           Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
   186             progress.nodes_status(use_theories_state.value.nodes_status)
   187           }
   188 
   189         Session.Consumer[Session.Commands_Changed](getClass.getName) {
   190           case changed =>
   191             if (changed.nodes.exists(dep_theories_set)) {
   192               val snapshot = session.snapshot()
   193               val state = snapshot.state
   194               val version = snapshot.version
   195 
   196               val theory_percentages =
   197                 use_theories_state.change_result(st =>
   198                   {
   199                     val domain =
   200                       if (st.nodes_status.is_empty) dep_theories_set
   201                       else changed.nodes.iterator.filter(dep_theories_set).toSet
   202 
   203                     val (nodes_status_changed, nodes_status1) =
   204                       st.nodes_status.update(resources.session_base, state, version,
   205                         domain = Some(domain), trim = changed.assignment)
   206 
   207                     if (nodes_status_delay >= Time.zero && nodes_status_changed) {
   208                       delay_nodes_status.invoke
   209                     }
   210 
   211                     val progress_percentage =
   212                       (for {
   213                         (name, node_status) <- nodes_status1.present.iterator
   214                         if changed.nodes.contains(name)
   215                         p1 = node_status.percentage
   216                         if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
   217                       } yield (name.theory, p1)).toList
   218 
   219                     (progress_percentage, st.update(nodes_status1))
   220                   })
   221 
   222               val check_theories =
   223                 (for {
   224                   command <- changed.commands.iterator
   225                   if dep_theories_set(command.node_name) && command.potentially_initialized
   226                 } yield command.node_name).toList
   227 
   228               if (check_theories.nonEmpty) {
   229                 val initialized =
   230                   use_theories_state.change_result(
   231                     _.initialized_theories(state, version, check_theories))
   232                 initialized.map(_.theory).sorted.foreach(progress.theory("", _))
   233               }
   234 
   235               for ((theory, percentage) <- theory_percentages)
   236                 progress.theory_percentage("", theory, percentage)
   237 
   238               check_state()
   239             }
   240         }
   241       }
   242 
   243       try {
   244         session.commands_changed += consumer
   245         resources.load_theories(session, id, dep_theories, progress)
   246         result.join_result
   247         check_progress.cancel
   248       }
   249       finally {
   250         session.commands_changed -= consumer
   251         resources.unload_theories(session, id, dep_theories)
   252       }
   253 
   254       result.join
   255     }
   256 
   257     def purge_theories(
   258       theories: List[String],
   259       qualifier: String = Sessions.DRAFT,
   260       master_dir: String = "",
   261       all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
   262     {
   263       val master = proper_string(master_dir) getOrElse tmp_dir_name
   264       val nodes = if (all) None else Some(theories.map(resources.import_name(qualifier, master, _)))
   265       resources.purge_theories(session, nodes)
   266     }
   267   }
   268 
   269 
   270   /* internal state */
   271 
   272   sealed case class State(
   273     required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
   274     theories: Map[Document.Node.Name, Theory] = Map.empty)
   275   {
   276     def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
   277 
   278     def insert_required(id: UUID, names: List[Document.Node.Name]): State =
   279       copy(required = (required /: names)(_.insert(_, id)))
   280 
   281     def remove_required(id: UUID, names: List[Document.Node.Name]): State =
   282       copy(required = (required /: names)(_.remove(_, id)))
   283 
   284     def update_theories(update: List[(Document.Node.Name, Theory)]): State =
   285       copy(theories =
   286         (theories /: update)({ case (thys, (name, thy)) =>
   287           thys.get(name) match {
   288             case Some(thy1) if thy1 == thy => thys
   289             case _ => thys + (name -> thy)
   290           }
   291         }))
   292 
   293     def remove_theories(remove: List[Document.Node.Name]): State =
   294     {
   295       require(remove.forall(name => !is_required(name)))
   296       copy(theories = theories -- remove)
   297     }
   298 
   299     lazy val theories_graph: Graph[Document.Node.Name, Unit] =
   300     {
   301       val entries =
   302         for ((name, theory) <- theories.toList)
   303         yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
   304       Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
   305     }
   306   }
   307 
   308   final class Theory private[Thy_Resources](
   309     val node_name: Document.Node.Name,
   310     val node_header: Document.Node.Header,
   311     val text: String,
   312     val node_required: Boolean)
   313   {
   314     override def toString: String = node_name.toString
   315 
   316     def node_perspective: Document.Node.Perspective_Text =
   317       Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
   318 
   319     def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
   320       List(node_name -> Document.Node.Deps(node_header),
   321         node_name -> Document.Node.Edits(text_edits),
   322         node_name -> node_perspective)
   323 
   324     def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
   325     {
   326       val (text_edits, old_required) =
   327         if (old.isEmpty) (Text.Edit.inserts(0, text), false)
   328         else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
   329 
   330       if (text_edits.isEmpty && node_required == old_required) Nil
   331       else make_edits(text_edits)
   332     }
   333 
   334     def purge_edits: List[Document.Edit_Text] =
   335       make_edits(Text.Edit.removes(0, text))
   336 
   337     def required(required: Boolean): Theory =
   338       if (required == node_required) this
   339       else new Theory(node_name, node_header, text, required)
   340   }
   341 }
   342 
   343 class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
   344   extends Resources(session_base, log = log)
   345 {
   346   resources =>
   347 
   348   private val state = Synchronized(Thy_Resources.State())
   349 
   350   def load_theories(
   351     session: Session,
   352     id: UUID,
   353     dep_theories: List[Document.Node.Name],
   354     progress: Progress)
   355   {
   356 
   357     val loaded_theories =
   358       for (node_name <- dep_theories)
   359       yield {
   360         val path = node_name.path
   361         if (!node_name.is_theory) error("Not a theory file: " + path)
   362 
   363         progress.expose_interrupt()
   364         val text = File.read(path)
   365         val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
   366         new Thy_Resources.Theory(node_name, node_header, text, true)
   367       }
   368 
   369     state.change(st =>
   370       {
   371         val st1 = st.insert_required(id, dep_theories)
   372         val theory_edits =
   373           for (theory <- loaded_theories)
   374           yield {
   375             val node_name = theory.node_name
   376             val theory1 = theory.required(st1.is_required(node_name))
   377             val edits = theory1.node_edits(st1.theories.get(node_name))
   378             (edits, (node_name, theory1))
   379           }
   380         session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   381         st1.update_theories(theory_edits.map(_._2))
   382       })
   383   }
   384 
   385   def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
   386   {
   387     state.change(st =>
   388       {
   389         val st1 = st.remove_required(id, dep_theories)
   390         val theory_edits =
   391           for {
   392             node_name <- dep_theories
   393             theory <- st1.theories.get(node_name)
   394           }
   395           yield {
   396             val theory1 = theory.required(st1.is_required(node_name))
   397             val edits = theory1.node_edits(Some(theory))
   398             (edits, (node_name, theory1))
   399           }
   400         session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   401         st1.update_theories(theory_edits.map(_._2))
   402       })
   403   }
   404 
   405   def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
   406     : (List[Document.Node.Name], List[Document.Node.Name]) =
   407   {
   408     state.change_result(st =>
   409       {
   410         val graph = st.theories_graph
   411         val all_nodes = graph.topological_order
   412 
   413         val purge =
   414           (if (nodes.isEmpty) all_nodes else nodes.get.filter(graph.defined(_))).
   415             filterNot(st.is_required(_)).toSet
   416 
   417         val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet
   418         val (retained, purged) = all_nodes.partition(retain)
   419 
   420         val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
   421         session.update(Document.Blobs.empty, purge_edits)
   422 
   423         ((purged, retained), st.remove_theories(purged))
   424       })
   425   }
   426 }