expose more bad cases;
authorwenzelm
Tue Apr 08 22:24:00 2014 +0200 (2014-04-08)
changeset 56476dd596c2b5897
parent 56475 710dee42b3d0
child 56477 57b5c8db55f1
expose more bad cases;
src/Pure/PIDE/command.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Apr 08 22:01:08 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Apr 08 22:24:00 2014 +0200
     1.3 @@ -198,7 +198,13 @@
     1.4                            state.add_markup(false, target_name, info)
     1.5                          case None => bad(); state
     1.6                        }
     1.7 -                    case None => /* FIXME bad(); */ state
     1.8 +                    case None =>
     1.9 +                      chunk_name match {
    1.10 +                        // FIXME workaround for static positions stemming from batch build
    1.11 +                        case Text.Chunk.File(name) if name.endsWith(".thy") =>
    1.12 +                        case _ => bad()
    1.13 +                      }
    1.14 +                      state
    1.15                    }
    1.16  
    1.17                  case XML.Elem(Markup(name, atts), args)