more robust: self-export only;
authorwenzelm
Tue May 08 11:47:41 2018 +0200 (15 months ago ago)
changeset 68119ce7f35406f37
parent 68118 c925f53fd1f6
child 68120 23c6ae3dd3a0
more robust: self-export only;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
     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 =
     2.1 --- a/src/Pure/PIDE/document.scala	Tue May 08 11:36:33 2018 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Tue May 08 11:47:41 2018 +0200
     2.3 @@ -725,13 +725,17 @@
     2.4      {
     2.5        execs.get(id) match {
     2.6          case Some(st) =>
     2.7 -          val new_st = st.add_export(entry)
     2.8 -          (new_st, copy(execs = execs + (id -> new_st)))
     2.9 +          st.add_export(entry) match {
    2.10 +            case Some(new_st) => (new_st, copy(execs = execs + (id -> new_st)))
    2.11 +            case None => fail
    2.12 +          }
    2.13          case None =>
    2.14            commands.get(id) match {
    2.15              case Some(st) =>
    2.16 -              val new_st = st.add_export(entry)
    2.17 -              (new_st, copy(commands = commands + (id -> new_st)))
    2.18 +              st.add_export(entry) match {
    2.19 +                case Some(new_st) => (new_st, copy(commands = commands + (id -> new_st)))
    2.20 +                case None => fail
    2.21 +              }
    2.22              case None => fail
    2.23            }
    2.24        }