author | wenzelm |
Tue, 08 Apr 2014 22:24:00 +0200 | |
changeset 56476 | dd596c2b5897 |
parent 56475 | 710dee42b3d0 |
child 56477 | 57b5c8db55f1 |
--- 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)