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