src/Pure/System/session.scala
changeset 37849 4f9de312cc23
parent 37689 628eabe2213a
child 38150 67fc24df3721
     1.1 --- a/src/Pure/System/session.scala	Mon Jul 19 08:59:43 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Mon Jul 19 22:19:18 2010 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4    /* events */
     1.5  
     1.6    case object Global_Settings
     1.7 +  case object Perspective
     1.8  
     1.9  
    1.10    /* managed entities */
    1.11 @@ -32,12 +33,25 @@
    1.12  
    1.13  class Session(system: Isabelle_System)
    1.14  {
    1.15 +  /* real time parameters */  // FIXME properties or settings (!?)
    1.16 +
    1.17 +  // user input (e.g. text edits, cursor movement)
    1.18 +  val input_delay = 300
    1.19 +
    1.20 +  // prover output (markup, common messages)
    1.21 +  val output_delay = 100
    1.22 +
    1.23 +  // GUI layout updates
    1.24 +  val update_delay = 500
    1.25 +
    1.26 +
    1.27    /* pervasive event buses */
    1.28  
    1.29    val global_settings = new Event_Bus[Session.Global_Settings.type]
    1.30    val raw_results = new Event_Bus[Isabelle_Process.Result]
    1.31    val raw_output = new Event_Bus[Isabelle_Process.Result]
    1.32    val commands_changed = new Event_Bus[Command_Set]
    1.33 +  val perspective = new Event_Bus[Session.Perspective.type]
    1.34  
    1.35  
    1.36    /* unique ids */
    1.37 @@ -263,7 +277,7 @@
    1.38      {
    1.39        val now = currentTime
    1.40        flush_time match {
    1.41 -        case None => flush_time = Some(now + 100)   // FIXME output_delay property
    1.42 +        case None => flush_time = Some(now + output_delay)
    1.43          case Some(time) => if (now >= time) flush()
    1.44        }
    1.45      }