src/Pure/PIDE/command.scala
changeset 68119 ce7f35406f37
parent 68104 0699a0bacc50
child 68307 d575281e18d0
     1.1 --- a/src/Pure/PIDE/command.scala	Tue May 08 11:36:33 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue May 08 11:47:41 2018 +0200
     1.3 @@ -291,8 +291,9 @@
     1.4      private def add_result(entry: Results.Entry): State =
     1.5        copy(results = results + entry)
     1.6  
     1.7 -    def add_export(entry: Exports.Entry): State =
     1.8 -      copy(exports = exports + entry)
     1.9 +    def add_export(entry: Exports.Entry): Option[State] =
    1.10 +      if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry))
    1.11 +      else None
    1.12  
    1.13      private def add_markup(
    1.14        status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =