# HG changeset patch
# User wenzelm
# Date 1525772861 -7200
# Node ID ce7f35406f37f0885f12e456f5198717b1048091
# Parent  c925f53fd1f6a13098250d16e400dd073909ec90
more robust: self-export only;

diff -r c925f53fd1f6 -r ce7f35406f37 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue May 08 11:36:33 2018 +0200
+++ b/src/Pure/PIDE/command.scala	Tue May 08 11:47:41 2018 +0200
@@ -291,8 +291,9 @@
     private def add_result(entry: Results.Entry): State =
       copy(results = results + entry)
 
-    def add_export(entry: Exports.Entry): State =
-      copy(exports = exports + entry)
+    def add_export(entry: Exports.Entry): Option[State] =
+      if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry))
+      else None
 
     private def add_markup(
       status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
diff -r c925f53fd1f6 -r ce7f35406f37 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue May 08 11:36:33 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Tue May 08 11:47:41 2018 +0200
@@ -725,13 +725,17 @@
     {
       execs.get(id) match {
         case Some(st) =>
-          val new_st = st.add_export(entry)
-          (new_st, copy(execs = execs + (id -> new_st)))
+          st.add_export(entry) match {
+            case Some(new_st) => (new_st, copy(execs = execs + (id -> new_st)))
+            case None => fail
+          }
         case None =>
           commands.get(id) match {
             case Some(st) =>
-              val new_st = st.add_export(entry)
-              (new_st, copy(commands = commands + (id -> new_st)))
+              st.add_export(entry) match {
+                case Some(new_st) => (new_st, copy(commands = commands + (id -> new_st)))
+                case None => fail
+              }
             case None => fail
           }
       }