src/Pure/PIDE/headless.scala
changeset 69548 892b68f932f9
parent 69532 16779868de1f
child 69550 faf547d2834c
     1.1 --- a/src/Pure/PIDE/headless.scala	Sat Dec 29 14:58:51 2018 +0100
     1.2 +++ b/src/Pure/PIDE/headless.scala	Sat Dec 29 16:11:24 2018 +0100
     1.3 @@ -16,47 +16,6 @@
     1.4  {
     1.5    /** session **/
     1.6  
     1.7 -  def start_session(
     1.8 -    options: Options,
     1.9 -    session_name: String,
    1.10 -    session_dirs: List[Path] = Nil,
    1.11 -    include_sessions: List[String] = Nil,
    1.12 -    session_base: Option[Sessions.Base] = None,
    1.13 -    print_mode: List[String] = Nil,
    1.14 -    progress: Progress = No_Progress,
    1.15 -    log: Logger = No_Logger): Session =
    1.16 -  {
    1.17 -    val base =
    1.18 -      session_base getOrElse
    1.19 -        Sessions.base_info(options, session_name, include_sessions = include_sessions,
    1.20 -          progress = progress, dirs = session_dirs).check_base
    1.21 -    val resources = new Resources(base, log = log)
    1.22 -    val session = new Session(session_name, options, resources)
    1.23 -
    1.24 -    val session_error = Future.promise[String]
    1.25 -    var session_phase: Session.Consumer[Session.Phase] = null
    1.26 -    session_phase =
    1.27 -      Session.Consumer(getClass.getName) {
    1.28 -        case Session.Ready =>
    1.29 -          session.phase_changed -= session_phase
    1.30 -          session_error.fulfill("")
    1.31 -        case Session.Terminated(result) if !result.ok =>
    1.32 -          session.phase_changed -= session_phase
    1.33 -          session_error.fulfill("Session start failed: return code " + result.rc)
    1.34 -        case _ =>
    1.35 -      }
    1.36 -    session.phase_changed += session_phase
    1.37 -
    1.38 -    progress.echo("Starting session " + session_name + " ...")
    1.39 -    Isabelle_Process.start(session, options,
    1.40 -      logic = session_name, dirs = session_dirs, modes = print_mode)
    1.41 -
    1.42 -    session_error.join match {
    1.43 -      case "" => session
    1.44 -      case msg => session.stop(); error(msg)
    1.45 -    }
    1.46 -  }
    1.47 -
    1.48    private def stable_snapshot(
    1.49      state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
    1.50    {
    1.51 @@ -330,6 +289,23 @@
    1.52  
    1.53    object Resources
    1.54    {
    1.55 +    def apply(base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
    1.56 +      new Resources(base_info, log = log)
    1.57 +
    1.58 +    def make(
    1.59 +      options: Options,
    1.60 +      session_name: String,
    1.61 +      session_dirs: List[Path] = Nil,
    1.62 +      include_sessions: List[String] = Nil,
    1.63 +      progress: Progress = No_Progress,
    1.64 +      log: Logger = No_Logger): Resources =
    1.65 +    {
    1.66 +      val base_info =
    1.67 +        Sessions.base_info(options, session_name, dirs = session_dirs,
    1.68 +          include_sessions = include_sessions, progress = progress)
    1.69 +      apply(base_info, log = log)
    1.70 +    }
    1.71 +
    1.72      final class Theory private[Headless](
    1.73        val node_name: Document.Node.Name,
    1.74        val node_header: Document.Node.Header,
    1.75 @@ -450,11 +426,48 @@
    1.76      }
    1.77    }
    1.78  
    1.79 -  class Resources(session_base: Sessions.Base, log: Logger = No_Logger)
    1.80 -    extends isabelle.Resources(session_base, log = log)
    1.81 +  class Resources private[Headless](
    1.82 +      val session_base_info: Sessions.Base_Info,
    1.83 +      log: Logger = No_Logger)
    1.84 +    extends isabelle.Resources(session_base_info.check_base, log = log)
    1.85    {
    1.86      resources =>
    1.87  
    1.88 +
    1.89 +    /* session */
    1.90 +
    1.91 +    def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =
    1.92 +    {
    1.93 +      val options = session_base_info.options
    1.94 +      val session = new Session(session_base_info.session, options, resources)
    1.95 +
    1.96 +      val session_error = Future.promise[String]
    1.97 +      var session_phase: Session.Consumer[Session.Phase] = null
    1.98 +      session_phase =
    1.99 +        Session.Consumer(getClass.getName) {
   1.100 +          case Session.Ready =>
   1.101 +            session.phase_changed -= session_phase
   1.102 +            session_error.fulfill("")
   1.103 +          case Session.Terminated(result) if !result.ok =>
   1.104 +            session.phase_changed -= session_phase
   1.105 +            session_error.fulfill("Session start failed: return code " + result.rc)
   1.106 +          case _ =>
   1.107 +        }
   1.108 +      session.phase_changed += session_phase
   1.109 +
   1.110 +      progress.echo("Starting session " + session_base_info.session + " ...")
   1.111 +      Isabelle_Process.start(session, options,
   1.112 +        logic = session_base_info.session, dirs = session_base_info.dirs, modes = print_mode)
   1.113 +
   1.114 +      session_error.join match {
   1.115 +        case "" => session
   1.116 +        case msg => session.stop(); error(msg)
   1.117 +      }
   1.118 +    }
   1.119 +
   1.120 +
   1.121 +    /* theories */
   1.122 +
   1.123      private val state = Synchronized(Resources.State())
   1.124  
   1.125      def load_theories(