src/Pure/System/session.scala
author wenzelm
Tue, 06 Sep 2011 11:25:27 +0200
changeset 44734 7313e2db3d39
parent 44733 329320fc88df
child 44775 27930cf6f0f7
permissions -rw-r--r--
more specific message channels to avoid potential bottle-neck of raw_messages;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 35013
diff changeset
     1
/*  Title:      Pure/System/session.scala
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 35013
diff changeset
     2
    Author:     Makarius
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
     3
    Options:    :folding=explicit:collapseFolds=1:
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 35013
diff changeset
     4
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
     5
Main Isabelle/Scala session, potentially with running prover process.
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 35013
diff changeset
     6
*/
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
     7
34871
e596a0b71f3c incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents: 34859
diff changeset
     8
package isabelle
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
     9
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
    10
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43443
diff changeset
    11
import java.lang.System
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
    12
import java.util.{Timer, TimerTask}
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    13
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
    14
import scala.collection.mutable
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
    15
import scala.actors.TIMEOUT
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    16
import scala.actors.Actor._
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    17
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
    18
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    19
object Session
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    20
{
34813
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    21
  /* events */
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    22
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    23
  //{{{
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    24
  case object Global_Settings
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    25
  case object Perspective
38849
2f198d107aef session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
wenzelm
parents: 38848
diff changeset
    26
  case object Assignment
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
    27
  case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    28
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    29
  sealed abstract class Phase
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    30
  case object Inactive extends Phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    31
  case object Startup extends Phase  // transient
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    32
  case object Failed extends Phase
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    33
  case object Ready extends Phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    34
  case object Shutdown extends Phase  // transient
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    35
  //}}}
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    36
}
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    37
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    38
44574
24444588fddd actual auto loading of required files;
wenzelm
parents: 44573
diff changeset
    39
class Session(thy_load: Thy_Load)
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    40
{
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    41
  /* real time parameters */  // FIXME properties or settings (!?)
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    42
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
    43
  val message_delay = Time.seconds(0.01)  // prover messages
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    44
  val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    45
  val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    46
  val update_delay = Time.seconds(0.5)  // GUI layout updates
44573
51f8895b9ad9 some dialog for auto loading of required files (still inactive);
wenzelm
parents: 44484
diff changeset
    47
  val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
    48
  val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
    49
  val prune_size = 0  // size of retained history
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    50
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    51
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    52
  /* pervasive event buses */
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    53
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    54
  val global_settings = new Event_Bus[Session.Global_Settings.type]
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    55
  val perspective = new Event_Bus[Session.Perspective.type]
38849
2f198d107aef session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
wenzelm
parents: 38848
diff changeset
    56
  val assignments = new Event_Bus[Session.Assignment.type]
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    57
  val commands_changed = new Event_Bus[Session.Commands_Changed]
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    58
  val phase_changed = new Event_Bus[Session.Phase]
44734
7313e2db3d39 more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents: 44733
diff changeset
    59
  val syslog_messages = new Event_Bus[Isabelle_Process.Result]
7313e2db3d39 more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents: 44733
diff changeset
    60
  val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
    61
  val raw_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    62
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    63
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    64
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    65
  /** buffered command changes (delay_first discipline) **/
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    66
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    67
  //{{{
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    68
  private case object Stop
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    69
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    70
  private val (_, commands_changed_buffer) =
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    71
    Simple_Thread.actor("commands_changed_buffer", daemon = true)
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    72
  {
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    73
    var finished = false
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    74
    while (!finished) {
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    75
      receive {
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    76
        case Stop => finished = true; reply(())
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    77
        case changed: Session.Commands_Changed => commands_changed.event(changed)
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    78
        case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    79
      }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    80
    }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    81
  }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    82
  //}}}
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    83
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    84
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    85
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    86
  /** main protocol actor **/
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    87
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
    88
  /* global state */
43644
ea08ce1c314b tuned signature;
wenzelm
parents: 43553
diff changeset
    89
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    90
  @volatile var verbose: Boolean = false
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    91
43695
5130dfe1b7be simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents: 43673
diff changeset
    92
  @volatile private var syntax = new Outer_Syntax
38569
9d480f6a2589 tuned signatures;
wenzelm
parents: 38446
diff changeset
    93
  def current_syntax(): Outer_Syntax = syntax
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    94
39626
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
    95
  @volatile private var reverse_syslog = List[XML.Elem]()
39629
08eb2730a8a1 tuned signature;
wenzelm
parents: 39626
diff changeset
    96
  def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
39626
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
    97
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    98
  @volatile private var _phase: Session.Phase = Session.Inactive
39633
26a28110ece5 simplified Session.Phase;
wenzelm
parents: 39630
diff changeset
    99
  private def phase_=(new_phase: Session.Phase)
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   100
  {
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   101
    _phase = new_phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   102
    phase_changed.event(new_phase)
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   103
  }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   104
  def phase = _phase
43553
df80747342cb proper tokens only if session is ready;
wenzelm
parents: 43520
diff changeset
   105
  def is_ready: Boolean = phase == Session.Ready
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   106
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   107
  private val global_state = new Volatile(Document.State.init)
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 43718
diff changeset
   108
  def current_state(): Document.State = global_state()
34816
d33312514220 maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents: 34815
diff changeset
   109
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   110
  def snapshot(name: Document.Node.Name, pending_edits: List[Text.Edit]): Document.Snapshot =
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 43718
diff changeset
   111
    global_state().snapshot(name, pending_edits)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   112
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   113
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   114
  /* theory files */
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   115
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   116
  def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
44442
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   117
  {
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   118
    def norm_import(s: String): String =
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   119
    {
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   120
      val thy_name = Thy_Header.base_name(s)
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   121
      if (thy_load.is_loaded(thy_name)) thy_name
44616
4beeaf2a226d tuned signature;
wenzelm
parents: 44615
diff changeset
   122
      else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s)))
44442
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   123
    }
44616
4beeaf2a226d tuned signature;
wenzelm
parents: 44615
diff changeset
   124
    def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))
44442
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   125
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   126
    val header1: Document.Node_Header =
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   127
      header match {
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   128
        case Exn.Res(Thy_Header(thy_name, _, _))
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   129
        if (thy_load.is_loaded(thy_name)) =>
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   130
          Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   131
        case _ => Document.Node.norm_header(norm_import, norm_use, header)
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   132
      }
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   133
    (name, Document.Node.Header(header1))
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   134
  }
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   135
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   136
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   137
  /* actor messages */
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   138
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   139
  private case class Start(timeout: Time, args: List[String])
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   140
  private case object Interrupt
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   141
  private case class Init_Node(name: Document.Node.Name,
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   142
    header: Document.Node_Header, perspective: Text.Perspective, text: String)
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   143
  private case class Edit_Node(name: Document.Node.Name,
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   144
    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   145
  private case class Change_Node(
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   146
    name: Document.Node.Name,
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   147
    doc_edits: List[Document.Edit_Command],
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   148
    previous: Document.Version,
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   149
    version: Document.Version)
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   150
  private case class Messages(msgs: List[Isabelle_Process.Message])
41534
f36cb6f233bd less verbosity;
wenzelm
parents: 40848
diff changeset
   151
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39528
diff changeset
   152
  private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
38639
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   153
  {
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43647
diff changeset
   154
    val this_actor = self
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   155
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   156
    var prune_next = System.currentTimeMillis() + prune_delay.ms
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   157
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   158
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   159
    /* buffered prover messages */
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   160
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   161
    object receiver
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   162
    {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   163
      private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   164
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   165
      def flush(): Unit = synchronized {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   166
        if (!buffer.isEmpty) {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   167
          val msgs = buffer.toList
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   168
          this_actor ! Messages(msgs)
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   169
          buffer = new mutable.ListBuffer[Isabelle_Process.Message]
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   170
        }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   171
      }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   172
      def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   173
        buffer += msg
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   174
        msg match {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   175
          case result: Isabelle_Process.Result if result.is_raw => flush()
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   176
          case _ =>
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   177
        }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   178
      }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   179
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   180
      private val timer = new Timer("session_actor.receiver", true)
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   181
      timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   182
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   183
      def cancel() { timer.cancel() }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   184
    }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   185
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   186
    var prover: Option[Isabelle_Process with Isar_Document] = None
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   187
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   188
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   189
    /* delayed command changes */
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   190
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   191
    object commands_changed_delay
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   192
    {
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   193
      private var changed_nodes: Set[Document.Node.Name] = Set.empty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   194
      private var changed_commands: Set[Command] = Set.empty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   195
      private def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   196
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   197
      private var flush_time: Option[Long] = None
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   198
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   199
      def flush_timeout: Long =
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   200
        flush_time match {
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   201
          case None => 5000L
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   202
          case Some(time) => (time - System.currentTimeMillis()) max 0
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   203
        }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   204
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   205
      def flush()
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   206
      {
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   207
        if (changed)
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   208
          commands_changed_buffer ! Session.Commands_Changed(changed_nodes, changed_commands)
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   209
        changed_nodes = Set.empty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   210
        changed_commands = Set.empty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   211
        flush_time = None
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   212
      }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   213
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   214
      def invoke(command: Command)
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   215
      {
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   216
        changed_nodes += command.node_name
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   217
        changed_commands += command
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   218
        val now = System.currentTimeMillis()
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   219
        flush_time match {
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   220
          case None => flush_time = Some(now + output_delay.ms)
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   221
          case Some(time) => if (now >= time) flush()
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   222
        }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   223
      }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   224
    }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   225
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   226
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   227
    /* perspective */
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   228
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   229
    def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   230
    {
44475
709e1d671483 tuned signature;
wenzelm
parents: 44446
diff changeset
   231
      val previous = global_state().tip_version
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   232
      val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   233
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   234
      val text_edits: List[Document.Edit_Text] =
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   235
        List((name, Document.Node.Perspective(text_perspective)))
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   236
      val change =
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   237
        global_state.change_yield(
44446
f9334afb6945 misc tuning and simplification;
wenzelm
parents: 44442
diff changeset
   238
          _.continue_history(Future.value(previous), text_edits, Future.value(version)))
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   239
44477
086bb1083552 maintain last_execs assignment on Scala side;
wenzelm
parents: 44476
diff changeset
   240
      val assignment = global_state().the_assignment(previous).check_finished
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   241
      global_state.change(_.define_version(version, assignment))
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44475
diff changeset
   242
      global_state.change_yield(_.assign(version.id, Document.no_assign))
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   243
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   244
      prover.get.update_perspective(previous.id, version.id, name, perspective)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   245
    }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   246
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   247
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   248
    /* incoming edits */
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   249
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   250
    def handle_edits(name: Document.Node.Name,
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 44383
diff changeset
   251
        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   252
    //{{{
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   253
    {
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   254
      val syntax = current_syntax()
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 43718
diff changeset
   255
      val previous = global_state().history.tip.version
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44183
diff changeset
   256
44612
990ac978854c explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents: 44608
diff changeset
   257
      prover.get.cancel_execution()
990ac978854c explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents: 44608
diff changeset
   258
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   259
      val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44183
diff changeset
   260
      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   261
      val change =
44446
f9334afb6945 misc tuning and simplification;
wenzelm
parents: 44442
diff changeset
   262
        global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   263
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   264
      result.map {
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   265
        case (doc_edits, _) =>
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   266
          assignments.await { global_state().is_assigned(previous.get_finished) }
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   267
          this_actor ! Change_Node(name, doc_edits, previous.join, change.version.join)
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   268
      }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   269
    }
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   270
    //}}}
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   271
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   272
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   273
    /* exec state assignment */
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   274
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44475
diff changeset
   275
    def handle_assign(id: Document.Version_ID, assign: Document.Assign)
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   276
    //{{{
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   277
    {
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44475
diff changeset
   278
      val cmds = global_state.change_yield(_.assign(id, assign))
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   279
      for (cmd <- cmds) commands_changed_delay.invoke(cmd)
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   280
      assignments.event(Session.Assignment)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   281
    }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   282
    //}}}
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   283
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   284
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   285
    /* removed versions */
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   286
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   287
    def handle_removed(removed: List[Document.Version_ID])
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   288
    //{{{
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   289
    {
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   290
      global_state.change(_.removed_versions(removed))
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   291
    }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   292
    //}}}
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   293
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   294
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   295
    /* resulting changes */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   296
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   297
    def handle_change(change: Change_Node)
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   298
    //{{{
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   299
    {
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   300
      val previous = change.previous
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   301
      val version = change.version
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   302
      val name = change.name
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   303
      val doc_edits = change.doc_edits
38366
fea82d1add74 simplified/clarified Change: transition prev --edits--> result, based on futures;
wenzelm
parents: 38365
diff changeset
   304
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   305
      def id_command(command: Command)
43720
wenzelm
parents: 43719
diff changeset
   306
      {
44582
479c07072992 tuned signature;
wenzelm
parents: 44574
diff changeset
   307
        if (!global_state().defined_command(command.id)) {
43720
wenzelm
parents: 43719
diff changeset
   308
          global_state.change(_.define_command(command))
44644
317e4962dd0f clarified define_command: store name as structural information;
wenzelm
parents: 44616
diff changeset
   309
          prover.get.define_command(command)
43720
wenzelm
parents: 43719
diff changeset
   310
        }
wenzelm
parents: 43719
diff changeset
   311
      }
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   312
      doc_edits foreach {
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   313
        case (_, edit) =>
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   314
          edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   315
      }
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   316
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   317
      val assignment = global_state().the_assignment(previous).check_finished
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   318
      global_state.change(_.define_version(version, assignment))
44481
bb42bc831570 tuned signature;
wenzelm
parents: 44479
diff changeset
   319
      prover.get.update(previous.id, version.id, doc_edits)
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   320
    }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   321
    //}}}
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   322
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   323
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   324
    /* prover results */
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   325
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   326
    def handle_result(result: Isabelle_Process.Result)
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   327
    //{{{
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   328
    {
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   329
      def bad_result(result: Isabelle_Process.Result)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   330
      {
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   331
        if (verbose)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   332
          System.err.println("Ignoring prover result: " + result.message.toString)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   333
      }
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   334
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38639
diff changeset
   335
      result.properties match {
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   336
        case Position.Id(state_id) if !result.is_raw =>
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   337
          try {
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   338
            val st = global_state.change_yield(_.accumulate(state_id, result.message))
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   339
            commands_changed_delay.invoke(st.command)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   340
          }
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   341
          catch {
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   342
            case _: Document.State.Fail => bad_result(result)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   343
          }
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
   344
        case Markup.Assign_Execs if result.is_raw =>
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
   345
          XML.content(result.body).mkString match {
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
   346
            case Isar_Document.Assign(id, assign) =>
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
   347
              try { handle_assign(id, assign) }
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
   348
              catch { case _: Document.State.Fail => bad_result(result) }
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
   349
            case _ => bad_result(result)
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
   350
          }
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   351
          // FIXME separate timeout event/message!?
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   352
          if (prover.isDefined && System.currentTimeMillis() > prune_next) {
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   353
            val old_versions = global_state.change_yield(_.prune_history(prune_size))
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   354
            if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   355
            prune_next = System.currentTimeMillis() + prune_delay.ms
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   356
          }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   357
        case Markup.Removed_Versions if result.is_raw =>
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   358
          XML.content(result.body).mkString match {
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   359
            case Isar_Document.Removed(removed) =>
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   360
              try { handle_removed(removed) }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   361
              catch { case _: Document.State.Fail => bad_result(result) }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   362
            case _ => bad_result(result)
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   363
          }
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   364
        case Markup.Invoke_Scala(name, id) if result.is_raw =>
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   365
          Future.fork {
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   366
            val arg = XML.content(result.body).mkString
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   367
            val (tag, res) = Invoke_Scala.method(name, arg)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   368
            prover.get.invoke_scala(id, tag, res)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   369
          }
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 44225
diff changeset
   370
        case Markup.Cancel_Scala(id) =>
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 44225
diff changeset
   371
          System.err.println("cancel_scala " + id)  // FIXME cancel JVM task
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38639
diff changeset
   372
        case _ =>
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   373
          if (result.is_syslog) {
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   374
            reverse_syslog ::= result.message
40533
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 40479
diff changeset
   375
            if (result.is_ready) {
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   376
              // FIXME move to ML side (!?)
40533
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 40479
diff changeset
   377
              syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 40479
diff changeset
   378
              syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 40479
diff changeset
   379
              phase = Session.Ready
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 40479
diff changeset
   380
            }
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   381
            else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
39696
f4da0428dc78 more informative Session.Phase;
wenzelm
parents: 39633
diff changeset
   382
            else if (result.is_exit) phase = Session.Inactive
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   383
          }
39626
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
   384
          else if (result.is_stdout) { }
39625
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39593
diff changeset
   385
          else if (result.is_status) {
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   386
            result.body match {
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   387
              case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   388
              case List(Keyword.Keyword_Decl(name)) => syntax += name
44574
24444588fddd actual auto loading of required files;
wenzelm
parents: 44573
diff changeset
   389
              case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
39625
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39593
diff changeset
   390
              case _ => bad_result(result)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   391
            }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   392
          }
39625
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39593
diff changeset
   393
          else bad_result(result)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   394
      }
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   395
    }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   396
    //}}}
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   397
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   398
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   399
    /* main loop */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   400
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   401
    //{{{
38639
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   402
    var finished = false
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   403
    while (!finished) {
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   404
      receiveWithin(commands_changed_delay.flush_timeout) {
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   405
        case TIMEOUT => commands_changed_delay.flush()
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   406
43649
a912f0b02359 eliminated null;
wenzelm
parents: 43648
diff changeset
   407
        case Start(timeout, args) if prover.isEmpty =>
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   408
          if (phase == Session.Inactive || phase == Session.Failed) {
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   409
            phase = Session.Startup
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   410
            prover =
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   411
              Some(new Isabelle_Process(timeout, receiver.invoke _, args:_*) with Isar_Document)
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   412
          }
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   413
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   414
        case Stop =>
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   415
          if (phase == Session.Ready) {
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   416
            global_state.change(_ => Document.State.init)  // FIXME event bus!?
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   417
            phase = Session.Shutdown
43649
a912f0b02359 eliminated null;
wenzelm
parents: 43648
diff changeset
   418
            prover.get.terminate
43717
c3ddb5537a2f more precise treatment of prover definedness;
wenzelm
parents: 43716
diff changeset
   419
            prover = None
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   420
            phase = Session.Inactive
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   421
          }
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   422
          finished = true
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   423
          receiver.cancel()
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   424
          reply(())
38850
5c3e5c548f12 session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;
wenzelm
parents: 38849
diff changeset
   425
43717
c3ddb5537a2f more precise treatment of prover definedness;
wenzelm
parents: 43716
diff changeset
   426
        case Interrupt if prover.isDefined =>
c3ddb5537a2f more precise treatment of prover definedness;
wenzelm
parents: 43716
diff changeset
   427
          prover.get.interrupt
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   428
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   429
        case Init_Node(name, header, perspective, text) if prover.isDefined =>
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   430
          // FIXME compare with existing node
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   431
          handle_edits(name, header,
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   432
            List(Document.Node.Clear(),
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   433
              Document.Node.Edits(List(Text.Edit.insert(0, text))),
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   434
              Document.Node.Perspective(perspective)))
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   435
          reply(())
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   436
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   437
        case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
44484
470f2ee5950e tuned Session.edit_node: update_perspective based on last_exec_offset;
wenzelm
parents: 44481
diff changeset
   438
          if (text_edits.isEmpty && global_state().tip_stable &&
470f2ee5950e tuned Session.edit_node: update_perspective based on last_exec_offset;
wenzelm
parents: 44481
diff changeset
   439
              perspective.range.stop <= global_state().last_exec_offset(name))
470f2ee5950e tuned Session.edit_node: update_perspective based on last_exec_offset;
wenzelm
parents: 44481
diff changeset
   440
            update_perspective(name, perspective)
470f2ee5950e tuned Session.edit_node: update_perspective based on last_exec_offset;
wenzelm
parents: 44481
diff changeset
   441
          else
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   442
            handle_edits(name, header,
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   443
              List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
43718
4a4ca9e4a14b clarified propagation of node name and header;
wenzelm
parents: 43717
diff changeset
   444
          reply(())
4a4ca9e4a14b clarified propagation of node name and header;
wenzelm
parents: 43717
diff changeset
   445
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   446
        case change: Change_Node if prover.isDefined =>
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   447
          handle_change(change)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   448
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   449
        case Messages(msgs) =>
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   450
          msgs foreach {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   451
            case input: Isabelle_Process.Input =>
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   452
              raw_messages.event(input)
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43720
diff changeset
   453
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   454
            case result: Isabelle_Process.Result =>
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   455
              handle_result(result)
44734
7313e2db3d39 more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents: 44733
diff changeset
   456
              if (result.is_syslog) syslog_messages.event(result)
7313e2db3d39 more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents: 44733
diff changeset
   457
              if (result.is_stdout) raw_output_messages.event(result)
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   458
              raw_messages.event(result)
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   459
          }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   460
43717
c3ddb5537a2f more precise treatment of prover definedness;
wenzelm
parents: 43716
diff changeset
   461
        case bad => System.err.println("session_actor: ignoring bad message " + bad)
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   462
      }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   463
    }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   464
    //}}}
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   465
  }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   466
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   467
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   468
  /* actions */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   469
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40566
diff changeset
   470
  def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   471
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   472
  def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   473
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   474
  def interrupt() { session_actor ! Interrupt }
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43647
diff changeset
   475
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   476
  def init_node(name: Document.Node.Name,
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   477
    header: Document.Node_Header, perspective: Text.Perspective, text: String)
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   478
  { session_actor !? Init_Node(name, header, perspective, text) }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   479
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   480
  def edit_node(name: Document.Node.Name,
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   481
    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   482
  { session_actor !? Edit_Node(name, header, perspective, edits) }
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   483
}