src/Pure/PIDE/command.scala
changeset 68114 ce7f35406f37
parent 68101 0699a0bacc50
child 68306 d575281e18d0
equal deleted inserted replaced
68113:c925f53fd1f6 68114:ce7f35406f37
   289       copy(status = st :: status)
   289       copy(status = st :: status)
   290 
   290 
   291     private def add_result(entry: Results.Entry): State =
   291     private def add_result(entry: Results.Entry): State =
   292       copy(results = results + entry)
   292       copy(results = results + entry)
   293 
   293 
   294     def add_export(entry: Exports.Entry): State =
   294     def add_export(entry: Exports.Entry): Option[State] =
   295       copy(exports = exports + entry)
   295       if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry))
       
   296       else None
   296 
   297 
   297     private def add_markup(
   298     private def add_markup(
   298       status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
   299       status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
   299     {
   300     {
   300       val markups1 =
   301       val markups1 =