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