src/Pure/System/session.scala
author wenzelm
Wed, 11 Aug 2010 22:41:26 +0200
changeset 38355 8cb265fb12fe
parent 38260 d4a1c7a19be3
child 38359 96b22dfeb56a
permissions -rw-r--r--
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
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
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 35013
diff changeset
     5
Isabelle session, potentially with running prover.
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
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    10
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
    11
import scala.actors.TIMEOUT
38226
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
    12
import scala.actors.Actor
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    13
import scala.actors.Actor._
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    14
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
    15
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    16
object Session
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    17
{
34813
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    18
  /* events */
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    19
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    20
  case object Global_Settings
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    21
  case object Perspective
34813
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    22
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    23
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    24
  /* managed entities */
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    25
38355
8cb265fb12fe represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents: 38260
diff changeset
    26
  type Entity_ID = Long
34813
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    27
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    28
  trait Entity
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    29
  {
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    30
    val id: Entity_ID
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
    31
    def consume(message: XML.Tree, forward: Command => Unit): Unit
34813
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    32
  }
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    33
}
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    34
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    35
34851
304a86164dd2 provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
wenzelm
parents: 34848
diff changeset
    36
class Session(system: Isabelle_System)
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    37
{
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    38
  /* real time parameters */  // FIXME properties or settings (!?)
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    39
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    40
  // user input (e.g. text edits, cursor movement)
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    41
  val input_delay = 300
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    42
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    43
  // prover output (markup, common messages)
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    44
  val output_delay = 100
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    45
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    46
  // GUI layout updates
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    47
  val update_delay = 500
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    48
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    49
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    50
  /* pervasive event buses */
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    51
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    52
  val global_settings = new Event_Bus[Session.Global_Settings.type]
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    53
  val raw_results = new Event_Bus[Isabelle_Process.Result]
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents: 37063
diff changeset
    54
  val raw_output = new Event_Bus[Isabelle_Process.Result]
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
    55
  val commands_changed = new Event_Bus[Command_Set]
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    56
  val perspective = new Event_Bus[Session.Perspective.type]
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    57
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    58
34778
8eccd35e975e removed unused Session.prover_logic;
wenzelm
parents: 34777
diff changeset
    59
  /* unique ids */
8eccd35e975e removed unused Session.prover_logic;
wenzelm
parents: 34777
diff changeset
    60
38355
8cb265fb12fe represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents: 38260
diff changeset
    61
  private var id_count: Long = 0
8cb265fb12fe represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents: 38260
diff changeset
    62
  def create_id(): Session.Entity_ID = synchronized {
8cb265fb12fe represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents: 38260
diff changeset
    63
    require(id_count > java.lang.Long.MIN_VALUE)
8cb265fb12fe represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents: 38260
diff changeset
    64
    id_count -= 1
8cb265fb12fe represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents: 38260
diff changeset
    65
    id_count
8cb265fb12fe represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents: 38260
diff changeset
    66
  }
34778
8eccd35e975e removed unused Session.prover_logic;
wenzelm
parents: 34777
diff changeset
    67
8eccd35e975e removed unused Session.prover_logic;
wenzelm
parents: 34777
diff changeset
    68
34826
6b38fc0b3406 eliminated redundant session documents database;
wenzelm
parents: 34825
diff changeset
    69
6b38fc0b3406 eliminated redundant session documents database;
wenzelm
parents: 34825
diff changeset
    70
  /** main actor **/
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    71
34851
304a86164dd2 provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
wenzelm
parents: 34848
diff changeset
    72
  @volatile private var syntax = new Outer_Syntax(system.symbols)
34819
86cb7f8e5a0d tuned signature;
wenzelm
parents: 34818
diff changeset
    73
  def current_syntax: Outer_Syntax = syntax
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    74
34816
d33312514220 maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents: 34815
diff changeset
    75
  @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
d33312514220 maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents: 34815
diff changeset
    76
  def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
34835
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
    77
  def lookup_command(id: Session.Entity_ID): Option[Command] =
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
    78
    lookup_entity(id) match {
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
    79
      case Some(cmd: Command) => Some(cmd)
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
    80
      case _ => None
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
    81
    }
34816
d33312514220 maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents: 34815
diff changeset
    82
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
    83
  private case class Started(timeout: Int, args: List[String])
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    84
  private case object Stop
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    85
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
    86
  private lazy val session_actor = actor {
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    87
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    88
    var prover: Isabelle_Process with Isar_Document = null
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    89
34816
d33312514220 maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents: 34815
diff changeset
    90
    def register(entity: Session.Entity) { entities += (entity.id -> entity) }
d33312514220 maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents: 34815
diff changeset
    91
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
    92
    var documents = Map[Document.Version_ID, Document]()
34835
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
    93
    def register_document(doc: Document) { documents += (doc.id -> doc) }
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
    94
    register_document(Document.init)
34835
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
    95
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    96
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    97
    /* document changes */
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    98
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38226
diff changeset
    99
    def handle_change(change: Document.Change)
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   100
    //{{{
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   101
    {
34824
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
   102
      require(change.parent.isDefined)
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   103
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   104
      val (node_edits, doc) = change.result.join
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   105
      val id_edits =
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   106
        node_edits map {
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   107
          case (name, None) => (name, None)
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   108
          case (name, Some(cmd_edits)) =>
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   109
            val chs =
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   110
              cmd_edits map {
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   111
                case (c1, c2) =>
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   112
                  val id1 = c1.map(_.id)
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   113
                  val id2 =
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   114
                    c2 match {
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   115
                      case None => None
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   116
                      case Some(command) =>
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   117
                        if (!lookup_command(command.id).isDefined) {
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   118
                          register(command)
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   119
                          prover.define_command(command.id, system.symbols.encode(command.source))
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   120
                        }
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   121
                        Some(command.id)
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   122
                    }
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   123
                  (id1, id2)
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   124
              }
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   125
            (name -> Some(chs))
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   126
        }
34835
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
   127
      register_document(doc)
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   128
      prover.edit_document(change.parent.get.id, doc.id, id_edits)
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   129
    }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   130
    //}}}
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   131
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   132
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   133
    /* prover results */
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   134
34836
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   135
    def bad_result(result: Isabelle_Process.Result)
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   136
    {
37041
dae419819a80 bad_result: report fully explicit message;
wenzelm
parents: 36947
diff changeset
   137
      System.err.println("Ignoring prover result: " + result.message.toString)
34836
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   138
    }
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   139
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   140
    def handle_result(result: Isabelle_Process.Result)
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   141
    //{{{
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   142
    {
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   143
      raw_results.event(result)
34799
0330a4284a9b just one variable for outer syntax keywords and completion;
wenzelm
parents: 34795
diff changeset
   144
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 38227
diff changeset
   145
      val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties)
34813
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
   146
      val target: Option[Session.Entity] =
34835
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
   147
        target_id match {
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   148
          case None => None
34835
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
   149
          case Some(id) => lookup_entity(id)
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   150
        }
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   151
      if (target.isDefined) target.get.consume(result.message, indicate_command_change)
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
   152
      else if (result.is_status) {
34818
7df68a8f0e3e register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents: 34817
diff changeset
   153
        // global status message
34836
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   154
        result.body match {
34835
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34833
diff changeset
   155
35013
f3d491658893 fixed spelling;
wenzelm
parents: 34871
diff changeset
   156
          // document state assignment
36682
3f989067f87d extractors for document updates;
wenzelm
parents: 36676
diff changeset
   157
          case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
34836
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   158
            documents.get(target_id.get) match {
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   159
              case Some(doc) =>
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   160
                val states =
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   161
                  for {
36682
3f989067f87d extractors for document updates;
wenzelm
parents: 36676
diff changeset
   162
                    Isar_Document.Edit(cmd_id, state_id) <- edits
34836
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   163
                    cmd <- lookup_command(cmd_id)
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   164
                  } yield {
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   165
                    val st = cmd.assign_state(state_id)
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   166
                    register(st)
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   167
                    (cmd, st)
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   168
                  }
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   169
                doc.assign_states(states)
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   170
              case None => bad_result(result)
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   171
            }
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   172
36682
3f989067f87d extractors for document updates;
wenzelm
parents: 36676
diff changeset
   173
          // keyword declarations
36947
285b39022372 renamed Outer_Keyword to Keyword (in Scala);
wenzelm
parents: 36782
diff changeset
   174
          case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
285b39022372 renamed Outer_Keyword to Keyword (in Scala);
wenzelm
parents: 36782
diff changeset
   175
          case List(Keyword.Keyword_Decl(name)) => syntax += name
34836
b83c7a738eb8 singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents: 34835
diff changeset
   176
34839
3457436a1110 more precise notion of bad messages;
wenzelm
parents: 34837
diff changeset
   177
          case _ => if (!result.is_ready) bad_result(result)
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   178
        }
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   179
      }
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
   180
      else if (result.kind == Markup.EXIT)
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   181
        prover = null
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents: 37063
diff changeset
   182
      else if (result.is_raw)
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents: 37063
diff changeset
   183
        raw_output.event(result)
37063
492bc98a8809 ignore system messages;
wenzelm
parents: 37041
diff changeset
   184
      else if (!result.is_system)   // FIXME syslog (!?)
34837
aa73039d5d14 result.is_ready is not bad;
wenzelm
parents: 34836
diff changeset
   185
        bad_result(result)
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   186
    }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   187
    //}}}
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   188
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   189
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   190
    /* prover startup */
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   191
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   192
    def startup_error(): String =
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   193
    {
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   194
      val buf = new StringBuilder
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   195
      while (
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   196
        receiveWithin(0) {
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   197
          case result: Isabelle_Process.Result =>
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   198
            if (result.is_raw) {
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   199
              for (text <- XML.content(result.message))
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   200
                buf.append(text)
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   201
            }
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   202
            true
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   203
          case TIMEOUT => false
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   204
        }) {}
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   205
      buf.toString
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   206
    }
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   207
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   208
    def prover_startup(timeout: Int): Option[String] =
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   209
    {
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   210
      receiveWithin(timeout) {
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   211
        case result: Isabelle_Process.Result
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
   212
          if result.kind == Markup.INIT =>
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   213
          while (receive {
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   214
            case result: Isabelle_Process.Result =>
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   215
              handle_result(result); !result.is_ready
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   216
            }) {}
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   217
          None
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   218
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   219
        case result: Isabelle_Process.Result
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
   220
          if result.kind == Markup.EXIT =>
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   221
          Some(startup_error())
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   222
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   223
        case TIMEOUT =>  // FIXME clarify
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   224
          prover.kill; Some(startup_error())
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   225
      }
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   226
    }
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   227
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   228
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   229
    /* main loop */
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   230
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   231
    val xml_cache = new XML.Cache(131071)
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   232
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   233
    loop {
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   234
      react {
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   235
        case Started(timeout, args) =>
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   236
          if (prover == null) {
34851
304a86164dd2 provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
wenzelm
parents: 34848
diff changeset
   237
            prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   238
            val origin = sender
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   239
            val opt_err = prover_startup(timeout)
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   240
            if (opt_err.isDefined) prover = null
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   241
            origin ! opt_err
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   242
          }
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   243
          else reply(None)
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   244
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   245
        case Stop =>  // FIXME clarify; synchronous
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   246
          if (prover != null) {
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   247
            prover.kill
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   248
            prover = null
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   249
          }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   250
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38226
diff changeset
   251
        case change: Document.Change if prover != null =>
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   252
          handle_change(change)
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   253
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   254
        case result: Isabelle_Process.Result =>
34795
c97335b7e8c3 cache results;
wenzelm
parents: 34792
diff changeset
   255
          handle_result(result.cache(xml_cache))
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   256
36782
0499d05663dd ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;
wenzelm
parents: 36682
diff changeset
   257
        case TIMEOUT =>  // FIXME clarify!
0499d05663dd ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;
wenzelm
parents: 36682
diff changeset
   258
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   259
        case bad if prover != null =>
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   260
          System.err.println("session_actor: ignoring bad message " + bad)
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   261
      }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   262
    }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   263
  }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   264
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   265
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   266
38226
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   267
  /** buffered command changes (delay_first discipline) **/
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   268
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   269
  private lazy val command_change_buffer = actor
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   270
  //{{{
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   271
  {
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   272
    import scala.compat.Platform.currentTime
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   273
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   274
    var changed: Set[Command] = Set()
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   275
    var flush_time: Option[Long] = None
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   276
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   277
    def flush_timeout: Long =
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   278
      flush_time match {
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   279
        case None => 5000L
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   280
        case Some(time) => (time - currentTime) max 0
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   281
      }
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   282
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   283
    def flush()
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   284
    {
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   285
      if (!changed.isEmpty) commands_changed.event(Command_Set(changed))
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   286
      changed = Set()
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   287
      flush_time = None
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   288
    }
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   289
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   290
    def invoke()
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   291
    {
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   292
      val now = currentTime
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   293
      flush_time match {
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
   294
        case None => flush_time = Some(now + output_delay)
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   295
        case Some(time) => if (now >= time) flush()
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   296
      }
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   297
    }
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   298
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   299
    loop {
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   300
      reactWithin(flush_timeout) {
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   301
        case command: Command => changed += command; invoke()
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   302
        case TIMEOUT => flush()
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   303
        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   304
      }
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   305
    }
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   306
  }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   307
  //}}}
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   308
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   309
  def indicate_command_change(command: Command)
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   310
  {
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   311
    command_change_buffer ! command
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   312
  }
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   313
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37065
diff changeset
   314
38226
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   315
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   316
  /** editor history **/
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   317
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   318
  private case class Edit_Document(edits: List[Document.Node_Text_Edit])
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   319
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   320
  private val editor_history = new Actor
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   321
  {
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38226
diff changeset
   322
    @volatile private var history = Document.Change.init
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38226
diff changeset
   323
    def current_change(): Document.Change = history
38226
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   324
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   325
    def act
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   326
    {
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   327
      loop {
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   328
        react {
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   329
          case Edit_Document(edits) =>
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   330
            val old_change = history
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   331
            val new_id = create_id()
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   332
            val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   333
              isabelle.Future.fork {
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   334
                val old_doc = old_change.join_document
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   335
                old_doc.await_assignment
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   336
                Document.text_edits(Session.this, old_doc, new_id, edits)
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   337
              }
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38226
diff changeset
   338
            val new_change = new Document.Change(new_id, Some(old_change), edits, result)
38226
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   339
            history = new_change
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   340
            new_change.result.map(_ => session_actor ! new_change)
38260
d4a1c7a19be3 edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
wenzelm
parents: 38230
diff changeset
   341
            reply(())
38226
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   342
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   343
          case bad => System.err.println("editor_model: ignoring bad message " + bad)
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   344
        }
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   345
      }
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   346
    }
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   347
  }
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   348
  editor_history.start
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   349
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   350
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   351
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
   352
  /** main methods **/
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   353
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   354
  def started(timeout: Int, args: List[String]): Option[String] =
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   355
    (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   356
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   357
  def stop() { session_actor ! Stop }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   358
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38226
diff changeset
   359
  def current_change(): Document.Change = editor_history.current_change()
38260
d4a1c7a19be3 edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
wenzelm
parents: 38230
diff changeset
   360
d4a1c7a19be3 edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
wenzelm
parents: 38230
diff changeset
   361
  def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   362
}