clarified management of (single) session;
authorwenzelm
Thu Jul 30 14:02:19 2015 +0200 (2015-07-30)
changeset 608356512bb0b1ff4
parent 60834 781f1168d31e
child 60836 c5db501da8e4
clarified management of (single) session;
proper Debugger.Update events;
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/Tools/debugger.scala
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Thu Jul 30 11:39:30 2015 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Thu Jul 30 14:02:19 2015 +0200
     1.3 @@ -16,9 +16,10 @@
     1.4  object Resources
     1.5  {
     1.6    def thy_path(path: Path): Path = path.ext("thy")
     1.7 +
     1.8 +  val empty: Resources = new Resources(Set.empty, Map.empty, Outer_Syntax.empty)
     1.9  }
    1.10  
    1.11 -
    1.12  class Resources(
    1.13    val loaded_theories: Set[String],
    1.14    val known_theories: Map[String, Document.Node.Name],
     2.1 --- a/src/Pure/PIDE/session.scala	Thu Jul 30 11:39:30 2015 +0200
     2.2 +++ b/src/Pure/PIDE/session.scala	Thu Jul 30 14:02:19 2015 +0200
     2.3 @@ -203,7 +203,7 @@
     2.4    val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
     2.5    val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
     2.6    val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
     2.7 -  val debugger_events = new Session.Outlet[Debugger.Event.type](dispatcher)
     2.8 +  val debugger_updates = new Session.Outlet[Debugger.Update](dispatcher)
     2.9  
    2.10    val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck!
    2.11  
     3.1 --- a/src/Pure/Tools/debugger.scala	Thu Jul 30 11:39:30 2015 +0200
     3.2 +++ b/src/Pure/Tools/debugger.scala	Thu Jul 30 14:02:19 2015 +0200
     3.3 @@ -11,7 +11,8 @@
     3.4  {
     3.5    /* global state */
     3.6  
     3.7 -  case class State(
     3.8 +  sealed case class State(
     3.9 +    session: Session = new Session(Resources.empty),
    3.10      output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
    3.11    {
    3.12      def add_output(name: String, entry: Command.Results.Entry): State =
    3.13 @@ -22,42 +23,36 @@
    3.14    def current_state(): State = global_state.value
    3.15  
    3.16  
    3.17 -  /* GUI interaction */
    3.18 -
    3.19 -  case object Event
    3.20 -
    3.21 -
    3.22 -  /* manager thread */
    3.23 +  /* protocol handler */
    3.24  
    3.25 -  private lazy val manager: Consumer_Thread[Any] =
    3.26 -    Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)(
    3.27 -      consume = (arg: Any) =>
    3.28 -      {
    3.29 -        // FIXME
    3.30 -        true
    3.31 -      },
    3.32 -      finish = () =>
    3.33 -      {
    3.34 -        // FIXME
    3.35 -      }
    3.36 -    )
    3.37 -
    3.38 -
    3.39 -  /* protocol handler */
    3.40 +  sealed case class Update(thread_names: Set[String])
    3.41  
    3.42    class Handler extends Session.Protocol_Handler
    3.43    {
    3.44 +    private var updated = Set.empty[String]
    3.45 +    private val delay_update =
    3.46 +      Simple_Thread.delay_first(current_state().session.output_delay) {
    3.47 +        current_state().session.debugger_updates.post(Update(updated))
    3.48 +        updated = Set.empty
    3.49 +      }
    3.50 +    private def update(name: String)
    3.51 +    {
    3.52 +      updated += name
    3.53 +      delay_update.invoke()
    3.54 +    }
    3.55 +
    3.56      private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    3.57      {
    3.58        msg.properties match {
    3.59 -        case Markup.Debugger_Output(name) =>
    3.60 +        case Markup.Debugger_Output(thread_name) =>
    3.61            val msg_body =
    3.62              prover.xml_cache.body(
    3.63                YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes)))
    3.64            msg_body match {
    3.65              case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
    3.66                val message = XML.Elem(Markup(Markup.message(name), props), body)
    3.67 -              global_state.change(_.add_output(name, i -> message))
    3.68 +              global_state.change(_.add_output(thread_name, i -> message))
    3.69 +              update(thread_name)
    3.70                true
    3.71              case _ => false
    3.72            }
    3.73 @@ -65,11 +60,6 @@
    3.74        }
    3.75      }
    3.76  
    3.77 -    override def stop(prover: Prover)
    3.78 -    {
    3.79 -      manager.shutdown()
    3.80 -    }
    3.81 -
    3.82      val functions =
    3.83        Map(Markup.DEBUGGER_OUTPUT -> debugger_output _)
    3.84    }
    3.85 @@ -77,12 +67,15 @@
    3.86  
    3.87    /* protocol commands */
    3.88  
    3.89 -  def init(session: Session): Unit =
    3.90 -    session.protocol_command("Debugger.init")
    3.91 +  def init(new_session: Session)
    3.92 +  {
    3.93 +    global_state.change(_.copy(session = new_session))
    3.94 +    current_state().session.protocol_command("Debugger.init")
    3.95 +  }
    3.96  
    3.97 -  def cancel(session: Session, name: String): Unit =
    3.98 -    session.protocol_command("Debugger.cancel", name)
    3.99 +  def cancel(name: String): Unit =
   3.100 +    current_state().session.protocol_command("Debugger.cancel", name)
   3.101  
   3.102 -  def input(session: Session, name: String, msg: String*): Unit =
   3.103 -    session.protocol_command("Debugger.input", (name :: msg.toList):_*)
   3.104 +  def input(name: String, msg: String*): Unit =
   3.105 +    current_state().session.protocol_command("Debugger.input", (name :: msg.toList):_*)
   3.106  }
     4.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Jul 30 11:39:30 2015 +0200
     4.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Jul 30 14:02:19 2015 +0200
     4.3 @@ -109,23 +109,25 @@
     4.4    private val main =
     4.5      Session.Consumer[Any](getClass.getName) {
     4.6        case _: Session.Global_Options =>
     4.7 +        Debugger.init(PIDE.session)
     4.8          GUI_Thread.later { handle_resize() }
     4.9  
    4.10 -      case Debugger.Event =>
    4.11 +      case _: Debugger.Update =>
    4.12          GUI_Thread.later { handle_update() }
    4.13      }
    4.14  
    4.15    override def init()
    4.16    {
    4.17      PIDE.session.global_options += main
    4.18 -    PIDE.session.debugger_events += main
    4.19 +    PIDE.session.debugger_updates += main
    4.20 +    Debugger.init(PIDE.session)
    4.21      handle_update()
    4.22    }
    4.23  
    4.24    override def exit()
    4.25    {
    4.26      PIDE.session.global_options -= main
    4.27 -    PIDE.session.debugger_events -= main
    4.28 +    PIDE.session.debugger_updates -= main
    4.29      delay_resize.revoke()
    4.30    }
    4.31  
     5.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Jul 30 11:39:30 2015 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Jul 30 14:02:19 2015 +0200
     5.3 @@ -21,6 +21,12 @@
     5.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
     5.5  
     5.6  
     5.7 +object JEdit_Resources
     5.8 +{
     5.9 +  val empty: JEdit_Resources =
    5.10 +    new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty)
    5.11 +}
    5.12 +
    5.13  class JEdit_Resources(
    5.14      loaded_theories: Set[String],
    5.15      known_theories: Map[String, Document.Node.Name],
    5.16 @@ -119,4 +125,3 @@
    5.17      if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
    5.18    }
    5.19  }
    5.20 -
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Jul 30 11:39:30 2015 +0200
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Jul 30 14:02:19 2015 +0200
     6.3 @@ -36,8 +36,7 @@
     6.4    @volatile var startup_notified = false
     6.5  
     6.6    @volatile var plugin: Plugin = null
     6.7 -  @volatile var session: Session =
     6.8 -    new Session(new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty))
     6.9 +  @volatile var session: Session = new Session(JEdit_Resources.empty)
    6.10  
    6.11    def options_changed() { plugin.options_changed() }
    6.12    def deps_changed() { plugin.deps_changed() }