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