equal
deleted
inserted
replaced
20 object Session |
20 object Session |
21 { |
21 { |
22 /* events */ |
22 /* events */ |
23 |
23 |
24 //{{{ |
24 //{{{ |
25 case object Global_Settings |
25 case object Global_Options |
26 case object Caret_Focus |
26 case object Caret_Focus |
27 case class Raw_Edits(edits: List[Document.Edit_Text]) |
27 case class Raw_Edits(edits: List[Document.Edit_Text]) |
28 case class Commands_Changed( |
28 case class Commands_Changed( |
29 assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) |
29 assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) |
30 |
30 |
55 def syslog_limit: Int = 100 |
55 def syslog_limit: Int = 100 |
56 |
56 |
57 |
57 |
58 /* pervasive event buses */ |
58 /* pervasive event buses */ |
59 |
59 |
60 val global_settings = new Event_Bus[Session.Global_Settings.type] |
60 val global_options = new Event_Bus[Session.Global_Options.type] |
61 val caret_focus = new Event_Bus[Session.Caret_Focus.type] |
61 val caret_focus = new Event_Bus[Session.Caret_Focus.type] |
62 val raw_edits = new Event_Bus[Session.Raw_Edits] |
62 val raw_edits = new Event_Bus[Session.Raw_Edits] |
63 val commands_changed = new Event_Bus[Session.Commands_Changed] |
63 val commands_changed = new Event_Bus[Session.Commands_Changed] |
64 val phase_changed = new Event_Bus[Session.Phase] |
64 val phase_changed = new Event_Bus[Session.Phase] |
65 val syslog_messages = new Event_Bus[Isabelle_Process.Output] |
65 val syslog_messages = new Event_Bus[Isabelle_Process.Output] |