expose more bad cases;
authorwenzelm
Tue, 08 Apr 2014 22:24:00 +0200
changeset 56476 dd596c2b5897
parent 56475 710dee42b3d0
child 56477 57b5c8db55f1
expose more bad cases;
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)