src/Pure/System/session.scala
changeset 48870 4accee106f0f
parent 48794 8d2a026e576b
child 48884 963b50ec6d73
     1.1 --- a/src/Pure/System/session.scala	Tue Aug 21 11:00:54 2012 +0200
     1.2 +++ b/src/Pure/System/session.scala	Tue Aug 21 12:15:25 2012 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  }
     1.5  
     1.6  
     1.7 -class Session(val thy_load: Thy_Load = new Thy_Load())
     1.8 +class Session(val thy_load: Thy_Load)
     1.9  {
    1.10    /* global flags */
    1.11  
    1.12 @@ -108,7 +108,7 @@
    1.13            val prev = previous.get_finished
    1.14            val (doc_edits, version) =
    1.15              Timing.timeit("Thy_Syntax.text_edits", timing) {
    1.16 -              Thy_Syntax.text_edits(base_syntax, prev, text_edits)
    1.17 +              Thy_Syntax.text_edits(thy_load.base_syntax, prev, text_edits)
    1.18              }
    1.19            version_result.fulfill(version)
    1.20            sender ! Change(doc_edits, prev, version)
    1.21 @@ -125,8 +125,6 @@
    1.22  
    1.23    /* global state */
    1.24  
    1.25 -  @volatile private var base_syntax = Outer_Syntax.init()
    1.26 -
    1.27    private val syslog = Volatile(Queue.empty[XML.Elem])
    1.28    def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
    1.29  
    1.30 @@ -145,7 +143,7 @@
    1.31    def recent_syntax(): Outer_Syntax =
    1.32    {
    1.33      val version = current_state().recent_finished.version.get_finished
    1.34 -    if (version.is_init) base_syntax
    1.35 +    if (version.is_init) thy_load.base_syntax
    1.36      else version.syntax
    1.37    }
    1.38    def get_recent_syntax(): Option[Outer_Syntax] =
    1.39 @@ -162,7 +160,7 @@
    1.40    def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
    1.41    {
    1.42      val header1 =
    1.43 -      if (thy_load.is_loaded(name.theory))
    1.44 +      if (thy_load.loaded_theories(name.theory))
    1.45          header.error("Attempt to update loaded theory " + quote(name.theory))
    1.46        else header
    1.47      (name, Document.Node.Deps(header1))
    1.48 @@ -171,7 +169,7 @@
    1.49  
    1.50    /* actor messages */
    1.51  
    1.52 -  private case class Start(dirs: List[Path], logic: String, args: List[String])
    1.53 +  private case class Start(args: List[String])
    1.54    private case object Cancel_Execution
    1.55    private case class Edit(edits: List[Document.Edit_Text])
    1.56    private case class Change(
    1.57 @@ -377,15 +375,9 @@
    1.58        receiveWithin(delay_commands_changed.flush_timeout) {
    1.59          case TIMEOUT => delay_commands_changed.flush()
    1.60  
    1.61 -        case Start(dirs, name, args) if prover.isEmpty =>
    1.62 +        case Start(args) if prover.isEmpty =>
    1.63            if (phase == Session.Inactive || phase == Session.Failed) {
    1.64              phase = Session.Startup
    1.65 -
    1.66 -            // FIXME static init in main constructor
    1.67 -            val content = Build.session_content(dirs, name).check_errors
    1.68 -            thy_load.register_thys(content.loaded_theories)
    1.69 -            base_syntax = content.syntax
    1.70 -
    1.71              prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
    1.72            }
    1.73  
    1.74 @@ -440,8 +432,8 @@
    1.75  
    1.76    /* actions */
    1.77  
    1.78 -  def start(dirs: List[Path], name: String, args: List[String])
    1.79 -  { session_actor ! Start(dirs, name, args) }
    1.80 +  def start(args: List[String])
    1.81 +  { session_actor ! Start(args) }
    1.82  
    1.83    def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
    1.84