src/Pure/Thy/thy_resources.scala
author wenzelm
Sat Mar 24 21:14:49 2018 +0100 (14 months ago)
changeset 67946 e1e57c288e45
parent 67945 984c3dc46cc0
child 67948 83902fff6243
permissions -rw-r--r--
session tmp_dir is default master_dir;
     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(session_name, 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_name: String,
    77     session_options: Options,
    78     override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
    79   {
    80     session =>
    81 
    82     val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
    83     val tmp_dir_name: String = File.path(tmp_dir).implode
    84 
    85     override def toString: String = session_name
    86 
    87     override def stop(): Process_Result =
    88     {
    89       try { super.stop() }
    90       finally { Isabelle_System.rm_tree(tmp_dir) }
    91     }
    92 
    93 
    94     /* theories */
    95 
    96     def use_theories(
    97       theories: List[String],
    98       qualifier: String = Sessions.DRAFT,
    99       master_dir: String = "",
   100       id: UUID = UUID(),
   101       progress: Progress = No_Progress): Theories_Result =
   102     {
   103       val dep_theories =
   104         resources.load_theories(session, id, theories, qualifier = qualifier,
   105           master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
   106 
   107       val result = Future.promise[Theories_Result]
   108 
   109       def check_state
   110       {
   111         val state = session.current_state()
   112         state.stable_tip_version match {
   113           case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) =>
   114             val nodes =
   115               for (name <- dep_theories)
   116               yield (name -> Protocol.node_status(state, version, name, version.nodes(name)))
   117             try { result.fulfill(Theories_Result(state, version, nodes)) }
   118             catch { case _: IllegalStateException => }
   119           case _ =>
   120         }
   121       }
   122 
   123       val check_progress =
   124         Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
   125           { if (progress.stopped) result.cancel else check_state }
   126 
   127       val consumer =
   128         Session.Consumer[Session.Commands_Changed](getClass.getName) {
   129           case changed => if (dep_theories.exists(changed.nodes)) check_state
   130         }
   131 
   132       try {
   133         session.commands_changed += consumer
   134         result.join_result
   135         check_progress.cancel
   136         session.commands_changed -= consumer
   137       }
   138       finally {
   139         resources.unload_theories(session, id, dep_theories)
   140       }
   141 
   142       result.join
   143     }
   144 
   145     def purge_theories(
   146         theories: List[String],
   147         qualifier: String = Sessions.DRAFT,
   148         master_dir: String = "",
   149         all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
   150       resources.purge_theories(session, theories = theories, qualifier = qualifier,
   151         master_dir = proper_string(master_dir) getOrElse tmp_dir_name, all = all)
   152   }
   153 
   154 
   155   /* internal state */
   156 
   157   sealed case class State(
   158     required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
   159     theories: Map[Document.Node.Name, Theory] = Map.empty)
   160   {
   161     def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
   162 
   163     def insert_required(id: UUID, names: List[Document.Node.Name]): State =
   164       copy(required = (required /: names)(_.insert(_, id)))
   165 
   166     def remove_required(id: UUID, names: List[Document.Node.Name]): State =
   167       copy(required = (required /: names)(_.remove(_, id)))
   168 
   169     def update_theories(update: List[(Document.Node.Name, Theory)]): State =
   170       copy(theories =
   171         (theories /: update)({ case (thys, (name, thy)) =>
   172           thys.get(name) match {
   173             case Some(thy1) if thy1 == thy => thys
   174             case _ => thys + (name -> thy)
   175           }
   176         }))
   177 
   178     def remove_theories(remove: List[Document.Node.Name]): State =
   179     {
   180       require(remove.forall(name => !is_required(name)))
   181       copy(theories = theories -- remove)
   182     }
   183 
   184     lazy val theories_graph: Graph[Document.Node.Name, Unit] =
   185     {
   186       val entries =
   187         for ((name, theory) <- theories.toList)
   188         yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
   189       Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
   190     }
   191   }
   192 
   193   final class Theory private[Thy_Resources](
   194     val node_name: Document.Node.Name,
   195     val node_header: Document.Node.Header,
   196     val text: String,
   197     val node_required: Boolean)
   198   {
   199     override def toString: String = node_name.toString
   200 
   201     def node_perspective: Document.Node.Perspective_Text =
   202       Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
   203 
   204     def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
   205       List(node_name -> Document.Node.Deps(node_header),
   206         node_name -> Document.Node.Edits(text_edits),
   207         node_name -> node_perspective)
   208 
   209     def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
   210     {
   211       val (text_edits, old_required) =
   212         if (old.isEmpty) (Text.Edit.inserts(0, text), false)
   213         else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
   214 
   215       if (text_edits.isEmpty && node_required == old_required) Nil
   216       else make_edits(text_edits)
   217     }
   218 
   219     def purge_edits: List[Document.Edit_Text] =
   220       make_edits(Text.Edit.removes(0, text))
   221 
   222     def required(required: Boolean): Theory =
   223       if (required == node_required) this
   224       else new Theory(node_name, node_header, text, required)
   225   }
   226 }
   227 
   228 class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
   229   extends Resources(session_base, log = log)
   230 {
   231   resources =>
   232 
   233   private val state = Synchronized(Thy_Resources.State())
   234 
   235   def load_theories(
   236     session: Session,
   237     id: UUID,
   238     theories: List[String],
   239     qualifier: String,
   240     master_dir: String,
   241     progress: Progress): List[Document.Node.Name] =
   242   {
   243     val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
   244     val dependencies = resources.dependencies(import_names, progress = progress).check_errors
   245     val dep_theories = dependencies.theories
   246 
   247     val loaded_theories =
   248       for (node_name <- dep_theories)
   249       yield {
   250         val path = node_name.path
   251         if (!node_name.is_theory) error("Not a theory file: " + path)
   252 
   253         progress.expose_interrupt()
   254         val text = File.read(path)
   255         val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
   256         new Thy_Resources.Theory(node_name, node_header, text, true)
   257       }
   258 
   259     state.change(st =>
   260       {
   261         val st1 = st.insert_required(id, dep_theories)
   262         val theory_edits =
   263           for (theory <- loaded_theories)
   264           yield {
   265             val node_name = theory.node_name
   266             val theory1 = theory.required(st1.is_required(node_name))
   267             val edits = theory1.node_edits(st1.theories.get(node_name))
   268             (edits, (node_name, theory1))
   269           }
   270         session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   271         st1.update_theories(theory_edits.map(_._2))
   272       })
   273 
   274     dep_theories
   275   }
   276 
   277   def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
   278   {
   279     state.change(st =>
   280       {
   281         val st1 = st.remove_required(id, dep_theories)
   282         val theory_edits =
   283           for {
   284             node_name <- dep_theories
   285             theory <- st1.theories.get(node_name)
   286           }
   287           yield {
   288             val theory1 = theory.required(st1.is_required(node_name))
   289             val edits = theory1.node_edits(Some(theory))
   290             (edits, (node_name, theory1))
   291           }
   292         session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   293         st1.update_theories(theory_edits.map(_._2))
   294       })
   295   }
   296 
   297   def purge_theories(session: Session,
   298     theories: List[String],
   299     qualifier: String,
   300     master_dir: String,
   301     all: Boolean): (List[Document.Node.Name], List[Document.Node.Name]) =
   302   {
   303     val nodes = theories.map(import_name(qualifier, master_dir, _))
   304 
   305     state.change_result(st =>
   306       {
   307         val graph = st.theories_graph
   308         val all_nodes = graph.topological_order
   309 
   310         val purge =
   311           (if (all) all_nodes else nodes.filter(graph.defined(_))).
   312             filterNot(st.is_required(_)).toSet
   313 
   314         val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet
   315         val (retained, purged) = all_nodes.partition(retain)
   316 
   317         val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
   318         session.update(Document.Blobs.empty, purge_edits)
   319 
   320         ((purged, retained), st.remove_theories(purged))
   321       })
   322   }
   323 }