src/Pure/System/session.scala
author wenzelm
Fri, 20 Apr 2012 20:29:44 +0200
changeset 47629 645163d3b964
parent 47390 580c37559354
child 47653 4605d4341b8b
permissions -rw-r--r--
simplified internal actor protocol;
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
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
    15
import scala.collection.immutable.Queue
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
    16
import scala.actors.TIMEOUT
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    17
import scala.actors.Actor._
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    18
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
    19
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    20
object Session
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    21
{
34813
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    22
  /* events */
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    23
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    24
  //{{{
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    25
  case object Global_Settings
44805
48a5c104d434 clarified terminology;
wenzelm
parents: 44775
diff changeset
    26
  case object Caret_Focus
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
    27
  case class Commands_Changed(
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
    28
    assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    29
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    30
  sealed abstract class Phase
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    31
  case object Inactive extends Phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    32
  case object Startup extends Phase  // transient
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    33
  case object Failed extends Phase
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    34
  case object Ready extends Phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    35
  case object Shutdown extends Phase  // transient
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    36
  //}}}
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    37
}
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    38
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    39
46739
6024353549ca clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
wenzelm
parents: 46737
diff changeset
    40
class Session(thy_load: Thy_Load = new Thy_Load)
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    41
{
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
    42
  /* tuning parameters */  // FIXME properties or settings (!?)
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    43
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
    44
  val message_delay = Time.seconds(0.01)  // prover messages
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    45
  val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    46
  val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    47
  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
    48
  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
    49
  val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
    50
  val prune_size = 0  // size of retained history
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
    51
  val syslog_limit = 100
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    52
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    53
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    54
  /* pervasive event buses */
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    55
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    56
  val global_settings = new Event_Bus[Session.Global_Settings.type]
44805
48a5c104d434 clarified terminology;
wenzelm
parents: 44775
diff changeset
    57
  val caret_focus = new Event_Bus[Session.Caret_Focus.type]
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    58
  val commands_changed = new Event_Bus[Session.Commands_Changed]
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    59
  val phase_changed = new Event_Bus[Session.Phase]
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
    60
  val syslog_messages = new Event_Bus[Isabelle_Process.Output]
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
    61
  val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
    62
  val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    63
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    64
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    65
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    66
  /** 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
    67
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    68
  //{{{
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    69
  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
    70
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    71
  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
    72
    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
    73
  {
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    74
    var finished = false
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    75
    while (!finished) {
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    76
      receive {
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    77
        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
    78
        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
    79
        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
    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
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    86
  /** pipelined change parsing **/
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    87
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    88
  //{{{
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    89
  private case class Text_Edits(
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    90
    previous: Future[Document.Version],
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    91
    text_edits: List[Document.Edit_Text],
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    92
    version_result: Promise[Document.Version])
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    93
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    94
  private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    95
  {
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    96
    var finished = false
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    97
    while (!finished) {
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    98
      receive {
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    99
        case Stop => finished = true; reply(())
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   100
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   101
        case Text_Edits(previous, text_edits, version_result) =>
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   102
          val prev = previous.get_finished
46942
f5c2d66faa04 basic support for outer syntax keywords in theory header;
wenzelm
parents: 46941
diff changeset
   103
          val (doc_edits, version) = Thy_Syntax.text_edits(prover_syntax, prev, text_edits)
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   104
          version_result.fulfill(version)
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   105
          sender ! Change(doc_edits, prev, version)
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   106
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   107
        case bad => System.err.println("change_parser: ignoring bad message " + bad)
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   108
      }
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   109
    }
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   110
  }
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   111
  //}}}
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   112
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   113
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   114
  /** main protocol actor **/
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   115
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   116
  /* global state */
43644
ea08ce1c314b tuned signature;
wenzelm
parents: 43553
diff changeset
   117
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   118
  @volatile var verbose: Boolean = false
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   119
46941
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46774
diff changeset
   120
  @volatile private var prover_syntax =
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46774
diff changeset
   121
    Outer_Syntax.init() +
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46774
diff changeset
   122
      // FIXME avoid hardwired stuff!?
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46774
diff changeset
   123
      ("hence", Keyword.PRF_ASM_GOAL, "then have") +
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46774
diff changeset
   124
      ("thus", Keyword.PRF_ASM_GOAL, "then show")
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   125
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   126
  private val syslog = Volatile(Queue.empty[XML.Elem])
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   127
  def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
39626
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
   128
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   129
  @volatile private var _phase: Session.Phase = Session.Inactive
39633
26a28110ece5 simplified Session.Phase;
wenzelm
parents: 39630
diff changeset
   130
  private def phase_=(new_phase: Session.Phase)
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   131
  {
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   132
    _phase = new_phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   133
    phase_changed.event(new_phase)
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   134
  }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   135
  def phase = _phase
43553
df80747342cb proper tokens only if session is ready;
wenzelm
parents: 43520
diff changeset
   136
  def is_ready: Boolean = phase == Session.Ready
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   137
45248
3b7b64b194ee class Volatile as abstract datatype;
wenzelm
parents: 45158
diff changeset
   138
  private val global_state = Volatile(Document.State.init)
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 43718
diff changeset
   139
  def current_state(): Document.State = global_state()
46944
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   140
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   141
  def recent_syntax(): Outer_Syntax =
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   142
  {
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   143
    val version = current_state().recent_finished.version.get_finished
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   144
    if (version.is_init) prover_syntax
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   145
    else version.syntax
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   146
  }
34816
d33312514220 maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents: 34815
diff changeset
   147
44960
640c2b957f16 graph traversal in topological order;
wenzelm
parents: 44953
diff changeset
   148
  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
640c2b957f16 graph traversal in topological order;
wenzelm
parents: 44953
diff changeset
   149
      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 43718
diff changeset
   150
    global_state().snapshot(name, pending_edits)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   151
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   152
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   153
  /* theory files */
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   154
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   155
  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
   156
  {
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   157
    val header1: Document.Node_Header =
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   158
      header match {
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46687
diff changeset
   159
        case Exn.Res(_) if (thy_load.is_loaded(name.theory)) =>
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46687
diff changeset
   160
          Exn.Exn(ERROR("Attempt to update loaded theory " + quote(name.theory)))
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46687
diff changeset
   161
        case _ => header
44442
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   162
      }
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   163
    (name, Document.Node.Header(header1))
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   164
  }
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   165
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   166
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   167
  /* actor messages */
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   168
45158
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45076
diff changeset
   169
  private case class Start(timeout: Time, args: List[String])
44775
27930cf6f0f7 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents: 44734
diff changeset
   170
  private case object Cancel_Execution
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   171
  private case class Edit(edits: List[Document.Edit_Text])
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   172
  private case class Change(
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   173
    doc_edits: List[Document.Edit_Command],
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   174
    previous: Document.Version,
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   175
    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
   176
  private case class Messages(msgs: List[Isabelle_Process.Message])
41534
f36cb6f233bd less verbosity;
wenzelm
parents: 40848
diff changeset
   177
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39528
diff changeset
   178
  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
   179
  {
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43647
diff changeset
   180
    val this_actor = self
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   181
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   182
    var prune_next = System.currentTimeMillis() + prune_delay.ms
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   183
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   184
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
   185
    /* 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
   186
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
    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
   188
    {
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
   189
      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
   190
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
   191
      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
   192
        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
   193
          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
   194
          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
   195
          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
   196
        }
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
   197
      }
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
   198
      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
   199
        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
   200
        msg match {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   201
          case output: Isabelle_Process.Output =>
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   202
            if (output.is_syslog)
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   203
              syslog >> (queue =>
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   204
                {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   205
                  val queue1 = queue.enqueue(output.message)
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   206
                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   207
                })
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   208
            if (output.is_protocol) flush()
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
   209
          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
   210
        }
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
   211
      }
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
   212
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
   213
      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
   214
      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
   215
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
   216
      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
   217
    }
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
   218
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   219
    var prover: Option[Isabelle_Process with Protocol] = None
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
   220
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
   221
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   222
    /* delayed command changes */
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   223
46570
wenzelm
parents: 46196
diff changeset
   224
    object delay_commands_changed
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   225
    {
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   226
      private var changed_assignment: Boolean = false
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   227
      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
   228
      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
   229
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   230
      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
   231
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   232
      def flush_timeout: Long =
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   233
        flush_time match {
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   234
          case None => 5000L
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   235
          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
   236
        }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   237
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   238
      def flush()
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   239
      {
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   240
        if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   241
          commands_changed_buffer !
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   242
            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   243
        changed_assignment = false
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   244
        changed_nodes = Set.empty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   245
        changed_commands = Set.empty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   246
        flush_time = None
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   247
      }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   248
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   249
      def invoke(assign: Boolean, commands: List[Command])
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   250
      {
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   251
        changed_assignment |= assign
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   252
        for (command <- commands) {
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   253
          changed_nodes += command.node_name
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   254
          changed_commands += command
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   255
        }
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   256
        val now = System.currentTimeMillis()
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   257
        flush_time match {
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   258
          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
   259
          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
   260
        }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   261
      }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   262
    }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   263
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   264
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   265
    /* resulting changes */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   266
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   267
    def handle_change(change: Change)
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   268
    //{{{
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   269
    {
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   270
      val previous = change.previous
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   271
      val version = change.version
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   272
      val doc_edits = change.doc_edits
38366
fea82d1add74 simplified/clarified Change: transition prev --edits--> result, based on futures;
wenzelm
parents: 38365
diff changeset
   273
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   274
      def id_command(command: Command)
43720
wenzelm
parents: 43719
diff changeset
   275
      {
44582
479c07072992 tuned signature;
wenzelm
parents: 44574
diff changeset
   276
        if (!global_state().defined_command(command.id)) {
46687
7e47ae85e161 tuned signature (in accordance with ML);
wenzelm
parents: 46682
diff changeset
   277
          global_state >> (_.define_command(command))
44644
317e4962dd0f clarified define_command: store name as structural information;
wenzelm
parents: 44616
diff changeset
   278
          prover.get.define_command(command)
43720
wenzelm
parents: 43719
diff changeset
   279
        }
wenzelm
parents: 43719
diff changeset
   280
      }
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   281
      doc_edits foreach {
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   282
        case (_, edit) =>
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   283
          edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   284
      }
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   285
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   286
      val assignment = global_state().the_assignment(previous).check_finished
46687
7e47ae85e161 tuned signature (in accordance with ML);
wenzelm
parents: 46682
diff changeset
   287
      global_state >> (_.define_version(version, assignment))
44481
bb42bc831570 tuned signature;
wenzelm
parents: 44479
diff changeset
   288
      prover.get.update(previous.id, version.id, doc_edits)
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   289
    }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   290
    //}}}
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   291
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   292
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   293
    /* prover output */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   294
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   295
    def handle_output(output: Isabelle_Process.Output)
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   296
    //{{{
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   297
    {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   298
      def bad_output(output: Isabelle_Process.Output)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   299
      {
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   300
        if (verbose)
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   301
          System.err.println("Ignoring prover output: " + output.message.toString)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   302
      }
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   303
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   304
      output.properties match {
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   305
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   306
        case Position.Id(state_id) if !output.is_protocol =>
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   307
          try {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   308
            val st = global_state >>> (_.accumulate(state_id, output.message))
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   309
            delay_commands_changed.invoke(false, List(st.command))
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   310
          }
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   311
          catch {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   312
            case _: Document.State.Fail => bad_output(output)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   313
          }
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   314
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   315
        case Isabelle_Markup.Assign_Execs if output.is_protocol =>
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   316
          XML.content(output.body).mkString match {
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   317
            case Protocol.Assign(id, assign) =>
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   318
              try {
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   319
                val cmds = global_state >>> (_.assign(id, assign))
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   320
                delay_commands_changed.invoke(true, cmds)
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   321
              }
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   322
              catch { case _: Document.State.Fail => bad_output(output) }
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   323
            case _ => bad_output(output)
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
   324
          }
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   325
          // FIXME separate timeout event/message!?
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   326
          if (prover.isDefined && System.currentTimeMillis() > prune_next) {
46687
7e47ae85e161 tuned signature (in accordance with ML);
wenzelm
parents: 46682
diff changeset
   327
            val old_versions = global_state >>> (_.prune_history(prune_size))
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   328
            if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   329
            prune_next = System.currentTimeMillis() + prune_delay.ms
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   330
          }
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   331
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   332
        case Isabelle_Markup.Removed_Versions if output.is_protocol =>
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   333
          XML.content(output.body).mkString match {
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   334
            case Protocol.Removed(removed) =>
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   335
              try {
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   336
                global_state >> (_.removed_versions(removed))
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   337
              }
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   338
              catch { case _: Document.State.Fail => bad_output(output) }
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   339
            case _ => bad_output(output)
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   340
          }
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   341
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   342
        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   343
          Future.fork {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   344
            val arg = XML.content(output.body).mkString
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   345
            val (tag, res) = Invoke_Scala.method(name, arg)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   346
            prover.get.invoke_scala(id, tag, res)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   347
          }
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   348
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   349
        case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
46121
30a69cd8a9a0 prefer raw_message for protocol implementation;
wenzelm
parents: 46120
diff changeset
   350
          System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   351
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   352
        case Isabelle_Markup.Ready if output.is_protocol =>
46121
30a69cd8a9a0 prefer raw_message for protocol implementation;
wenzelm
parents: 46120
diff changeset
   353
            phase = Session.Ready
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   354
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   355
        case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   356
          thy_load.register_thy(name)
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   357
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   358
        case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol =>
46941
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46774
diff changeset
   359
          prover_syntax += (name, kind)
46123
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   360
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   361
        case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
46941
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46774
diff changeset
   362
          prover_syntax += name
46123
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   363
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38639
diff changeset
   364
        case _ =>
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   365
          if (output.is_exit && phase == Session.Startup) phase = Session.Failed
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   366
          else if (output.is_exit) phase = Session.Inactive
47390
580c37559354 init message not bad;
wenzelm
parents: 47346
diff changeset
   367
          else if (output.is_init || output.is_stdout) { }
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   368
          else bad_output(output)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   369
      }
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   370
    }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   371
    //}}}
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   372
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   373
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   374
    /* main loop */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   375
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   376
    //{{{
38639
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   377
    var finished = false
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   378
    while (!finished) {
46570
wenzelm
parents: 46196
diff changeset
   379
      receiveWithin(delay_commands_changed.flush_timeout) {
wenzelm
parents: 46196
diff changeset
   380
        case TIMEOUT => delay_commands_changed.flush()
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   381
45158
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45076
diff changeset
   382
        case Start(timeout, args) if prover.isEmpty =>
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   383
          if (phase == Session.Inactive || phase == Session.Failed) {
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   384
            phase = Session.Startup
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   385
            prover = Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Protocol)
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   386
          }
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   387
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   388
        case Stop =>
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   389
          if (phase == Session.Ready) {
46687
7e47ae85e161 tuned signature (in accordance with ML);
wenzelm
parents: 46682
diff changeset
   390
            global_state >> (_ => Document.State.init)  // FIXME event bus!?
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   391
            phase = Session.Shutdown
43649
a912f0b02359 eliminated null;
wenzelm
parents: 43648
diff changeset
   392
            prover.get.terminate
43717
c3ddb5537a2f more precise treatment of prover definedness;
wenzelm
parents: 43716
diff changeset
   393
            prover = None
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   394
            phase = Session.Inactive
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   395
          }
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   396
          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
   397
          receiver.cancel()
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   398
          reply(())
38850
5c3e5c548f12 session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;
wenzelm
parents: 38849
diff changeset
   399
44775
27930cf6f0f7 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents: 44734
diff changeset
   400
        case Cancel_Execution if prover.isDefined =>
27930cf6f0f7 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents: 44734
diff changeset
   401
          prover.get.cancel_execution()
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   402
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   403
        case Edit(edits) if prover.isDefined =>
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   404
          prover.get.discontinue_execution()
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   405
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   406
          val previous = global_state().history.tip.version
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   407
          val version = Future.promise[Document.Version]
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   408
          val change = global_state >>> (_.continue_history(previous, edits, version))
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   409
          change_parser ! Text_Edits(previous, edits, version)
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   410
43718
4a4ca9e4a14b clarified propagation of node name and header;
wenzelm
parents: 43717
diff changeset
   411
          reply(())
4a4ca9e4a14b clarified propagation of node name and header;
wenzelm
parents: 43717
diff changeset
   412
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
   413
        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
   414
          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
   415
            case input: Isabelle_Process.Input =>
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   416
              all_messages.event(input)
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43720
diff changeset
   417
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   418
            case output: Isabelle_Process.Output =>
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   419
              handle_output(output)
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   420
              if (output.is_syslog) syslog_messages.event(output)
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   421
              if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   422
              all_messages.event(output)
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
          }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   424
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   425
        case change: Change
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   426
        if prover.isDefined && global_state().is_assigned(change.previous) =>
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   427
          handle_change(change)
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   428
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   429
        case bad if !bad.isInstanceOf[Change] =>
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   430
          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
   431
      }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   432
    }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   433
    //}}}
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   434
  }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   435
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   436
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   437
  /* actions */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   438
45158
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45076
diff changeset
   439
  def start(timeout: Time, args: List[String])
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45076
diff changeset
   440
  { session_actor ! Start(timeout, args) }
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   441
45158
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45076
diff changeset
   442
  def start(args: List[String]) { start (Time.seconds(25), args) }
45076
dd803d319d5b tuned signature;
wenzelm
parents: 45075
diff changeset
   443
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   444
  def stop() { commands_changed_buffer !? Stop; change_parser !? 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
   445
44775
27930cf6f0f7 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents: 44734
diff changeset
   446
  def cancel_execution() { session_actor ! Cancel_Execution }
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43647
diff changeset
   447
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   448
  def edit(edits: List[Document.Edit_Text])
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   449
  { session_actor !? Edit(edits) }
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   450
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   451
  def init_node(name: Document.Node.Name,
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   452
    header: Document.Node_Header, perspective: Text.Perspective, text: String)
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   453
  {
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   454
    edit(List(header_edit(name, header),
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   455
      name -> Document.Node.Clear(),    // FIXME diff wrt. existing node
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   456
      name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   457
      name -> Document.Node.Perspective(perspective)))
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   458
  }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   459
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   460
  def edit_node(name: Document.Node.Name,
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   461
    header: Document.Node_Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   462
  {
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   463
    edit(List(header_edit(name, header),
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   464
      name -> Document.Node.Edits(text_edits),
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   465
      name -> Document.Node.Perspective(perspective)))
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   466
  }
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   467
}