diff -r 6e739225dd8a -r 9e8f30bfbdca src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Aug 14 10:44:03 2012 +0200 +++ b/src/Pure/System/session.scala Tue Aug 14 11:37:58 2012 +0200 @@ -171,7 +171,7 @@ /* actor messages */ - private case class Start(logic: String, args: List[String]) + private case class Start(dirs: List[Path], logic: String, args: List[String]) private case object Cancel_Execution private case class Edit(edits: List[Document.Edit_Text]) private case class Change( @@ -377,12 +377,12 @@ receiveWithin(delay_commands_changed.flush_timeout) { case TIMEOUT => delay_commands_changed.flush() - case Start(name, args) if prover.isEmpty => + case Start(dirs, name, args) if prover.isEmpty => if (phase == Session.Inactive || phase == Session.Failed) { phase = Session.Startup // FIXME static init in main constructor - val content = Build.session_content(name) + val content = Build.session_content(dirs, name) thy_load.register_thys(content.loaded_theories) base_syntax = content.syntax @@ -440,7 +440,8 @@ /* actions */ - def start(name: String, args: List[String]) { session_actor ! Start(name, args) } + def start(dirs: List[Path], name: String, args: List[String]) + { session_actor ! Start(dirs, name, args) } def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }