disallow theory name "ROOT";
authorwenzelm
Sat Dec 16 16:57:06 2017 +0100 (17 months ago)
changeset 6721699815211970c
parent 67215 03d0c958d65a
child 67217 53867014e299
disallow theory name "ROOT";
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Sat Dec 16 16:46:01 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sat Dec 16 16:57:06 2017 +0100
     1.3 @@ -456,7 +456,12 @@
     1.4        val session_options = options ++ entry.options
     1.5  
     1.6        val theories =
     1.7 -        entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
     1.8 +        entry.theories.map({ case (opts, thys) =>
     1.9 +          (session_options ++ opts,
    1.10 +            thys.map({ case ((thy, pos), _) =>
    1.11 +              if (thy == Sessions.root_name)
    1.12 +                error("Bad theory name " + quote(thy) + Position.here(pos))
    1.13 +              else (thy, pos) })) })
    1.14  
    1.15        val global_theories =
    1.16          for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }