src/Pure/Thy/sessions.scala
changeset 70875 c1597167563e
parent 70874 60b1eda998f3
child 70876 9cde8c4ea5a5
equal deleted inserted replaced
70874:60b1eda998f3 70875:c1597167563e
   491           val other_name = info.name + "_requirements(" + ancestor.get + ")"
   491           val other_name = info.name + "_requirements(" + ancestor.get + ")"
   492           (other_name,
   492           (other_name,
   493             List(
   493             List(
   494               make_info(info.options,
   494               make_info(info.options,
   495                 dir_selected = false,
   495                 dir_selected = false,
   496                 dir = info.dir,
   496                 dir = Path.explode("$ISABELLE_TMP_PREFIX"),
   497                 chapter = info.chapter,
   497                 chapter = info.chapter,
   498                 Session_Entry(
   498                 Session_Entry(
   499                   pos = info.pos,
   499                   pos = info.pos,
   500                   name = other_name,
   500                   name = other_name,
   501                   groups = info.groups,
   501                   groups = info.groups,