# HG changeset patch
# User wenzelm
# Date 1396988640 -7200
# Node ID dd596c2b58977ca4ada64744c5e9feca6a78bb62
# Parent  710dee42b3d08adc26f32a73b3ab2a485a966200
expose more bad cases;

diff -r 710dee42b3d0 -r dd596c2b5897 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Apr 08 22:01:08 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Apr 08 22:24:00 2014 +0200
@@ -198,7 +198,13 @@
                           state.add_markup(false, target_name, info)
                         case None => bad(); state
                       }
-                    case None => /* FIXME bad(); */ state
+                    case None =>
+                      chunk_name match {
+                        // FIXME workaround for static positions stemming from batch build
+                        case Text.Chunk.File(name) if name.endsWith(".thy") =>
+                        case _ => bad()
+                      }
+                      state
                   }
 
                 case XML.Elem(Markup(name, atts), args)