src/Pure/PIDE/document.scala
changeset 68114 ce7f35406f37
parent 68101 0699a0bacc50
child 68299 0b5a23477911
--- 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
           }
       }