src/Pure/PIDE/document.scala
changeset 68114 ce7f35406f37
parent 68101 0699a0bacc50
child 68299 0b5a23477911
equal deleted inserted replaced
68113:c925f53fd1f6 68114:ce7f35406f37
   723 
   723 
   724     def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) =
   724     def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) =
   725     {
   725     {
   726       execs.get(id) match {
   726       execs.get(id) match {
   727         case Some(st) =>
   727         case Some(st) =>
   728           val new_st = st.add_export(entry)
   728           st.add_export(entry) match {
   729           (new_st, copy(execs = execs + (id -> new_st)))
   729             case Some(new_st) => (new_st, copy(execs = execs + (id -> new_st)))
       
   730             case None => fail
       
   731           }
   730         case None =>
   732         case None =>
   731           commands.get(id) match {
   733           commands.get(id) match {
   732             case Some(st) =>
   734             case Some(st) =>
   733               val new_st = st.add_export(entry)
   735               st.add_export(entry) match {
   734               (new_st, copy(commands = commands + (id -> new_st)))
   736                 case Some(new_st) => (new_st, copy(commands = commands + (id -> new_st)))
       
   737                 case None => fail
       
   738               }
   735             case None => fail
   739             case None => fail
   736           }
   740           }
   737       }
   741       }
   738     }
   742     }
   739 
   743