src/Pure/PIDE/command.scala
author wenzelm
Thu, 12 Aug 2010 15:19:11 +0200
changeset 38363 af7f41a8a0a8
parent 38362 754ad6340055
child 38367 f7d2574dc3a6
permissions -rw-r--r--
clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type Document.id (ML) / Document.ID;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     1
/*  Title:      Pure/PIDE/command.scala
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     2
    Author:     Fabian Immler, TU Munich
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     3
    Author:     Makarius
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     4
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     5
Prover commands with semantic state.
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     6
*/
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
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: 34865
diff changeset
     8
package isabelle
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     9
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    10
34699
wenzelm
parents: 34698
diff changeset
    11
import scala.actors.Actor, Actor._
34497
184fda8cce04 more explicit indication of mutable collections;
wenzelm
parents: 34495
diff changeset
    12
import scala.collection.mutable
34486
7985efd78aa1 tuned handling of accumulated results;
wenzelm
parents: 34485
diff changeset
    13
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    14
34637
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    15
object Command
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    16
{
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    17
  object Status extends Enumeration
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    18
  {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    19
    val UNPROCESSED = Value("UNPROCESSED")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    20
    val FINISHED = Value("FINISHED")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    21
    val FAILED = Value("FAILED")
36990
449628c148cf explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
wenzelm
parents: 36676
diff changeset
    22
    val UNDEFINED = Value("UNDEFINED")
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    23
  }
34707
cc5d388fcbf2 eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents: 34705
diff changeset
    24
37197
953fc4983439 more detailed token markup, including command kind as sub_kind;
wenzelm
parents: 37189
diff changeset
    25
  case class HighlightInfo(kind: String, sub_kind: Option[String]) {
953fc4983439 more detailed token markup, including command kind as sub_kind;
wenzelm
parents: 37189
diff changeset
    26
    override def toString = kind
953fc4983439 more detailed token markup, including command kind as sub_kind;
wenzelm
parents: 37189
diff changeset
    27
  }
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34708
diff changeset
    28
  case class TypeInfo(ty: String)
34707
cc5d388fcbf2 eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents: 34705
diff changeset
    29
  case class RefInfo(file: Option[String], line: Option[Int],
38363
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38362
diff changeset
    30
    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    31
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    32
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    33
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    34
  /** accumulated results from prover **/
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    35
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    36
  case class State(
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    37
    val command: Command,
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    38
    val status: Command.Status.Value,
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    39
    val forks: Int,
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    40
    val reverse_results: List[XML.Tree],
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    41
    val markup: Markup_Text)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    42
  {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    43
    def this(command: Command) =
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    44
      this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    45
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    46
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    47
    /* content */
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    48
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    49
    lazy val results = reverse_results.reverse
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    50
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    51
    def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    52
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    53
    def add_markup(node: Markup_Tree): State = copy(markup = markup + node)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    54
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    55
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    56
    /* markup */
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    57
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    58
    lazy val highlight: Markup_Text =
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    59
    {
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    60
      markup.filter(_.info match {
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    61
        case Command.HighlightInfo(_, _) => true
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    62
        case _ => false
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    63
      })
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    64
    }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    65
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    66
    private lazy val types: List[Markup_Node] =
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    67
      markup.filter(_.info match {
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    68
        case Command.TypeInfo(_) => true
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    69
        case _ => false }).flatten
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    70
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    71
    def type_at(pos: Int): Option[String] =
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    72
    {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    73
      types.find(t => t.start <= pos && pos < t.stop) match {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    74
        case Some(t) =>
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    75
          t.info match {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    76
            case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    77
            case _ => None
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    78
          }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    79
        case None => None
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    80
      }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    81
    }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    82
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    83
    private lazy val refs: List[Markup_Node] =
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    84
      markup.filter(_.info match {
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    85
        case Command.RefInfo(_, _, _, _) => true
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    86
        case _ => false }).flatten
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    87
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    88
    def ref_at(pos: Int): Option[Markup_Node] =
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    89
      refs.find(t => t.start <= pos && pos < t.stop)
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    90
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    91
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    92
    /* message dispatch */
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    93
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    94
    def accumulate(message: XML.Tree): Command.State =
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    95
      message match {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    96
        case XML.Elem(Markup(Markup.STATUS, _), elems) =>
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    97
          (this /: elems)((state, elem) =>
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    98
            elem match {
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    99
              case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED)
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   100
              case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED)
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   101
              case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED)
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   102
              case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1)
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   103
              case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   104
              case _ => System.err.println("Ignored status message: " + elem); state
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   105
            })
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   106
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   107
        case XML.Elem(Markup(Markup.REPORT, _), elems) =>
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   108
          (this /: elems)((state, elem) =>
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   109
            elem match {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   110
              case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   111
                atts match {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   112
                  case Position.Range(begin, end) =>
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   113
                    if (kind == Markup.ML_TYPING) {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   114
                      val info = Pretty.string_of(body, margin = 40)
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   115
                      state.add_markup(
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   116
                        command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   117
                    }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   118
                    else if (kind == Markup.ML_REF) {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   119
                      body match {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   120
                        case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   121
                          state.add_markup(
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   122
                            command.markup_node(
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   123
                              begin - 1, end - 1,
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   124
                              Command.RefInfo(
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   125
                                Position.get_file(props),
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   126
                                Position.get_line(props),
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   127
                                Position.get_id(props),
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
   128
                                Position.get_offset(props))))
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   129
                        case _ => state
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   130
                      }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   131
                    }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   132
                    else {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   133
                      state.add_markup(
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   134
                        command.markup_node(begin - 1, end - 1,
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   135
                          Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   136
                    }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   137
                  case _ => state
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   138
                }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   139
              case _ => System.err.println("Ignored report message: " + elem); state
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   140
            })
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   141
        case _ => add_result(message)
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   142
      }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   143
  }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   144
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   145
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   146
34697
3d4874198e62 State: immutable;
wenzelm
parents: 34688
diff changeset
   147
class Command(
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37373
diff changeset
   148
    val id: Document.Command_ID,
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   149
    val span: Thy_Syntax.Span,
38220
b30aa2dbedca avoid null in Scala;
wenzelm
parents: 38150
diff changeset
   150
    val static_parent: Option[Command] = None)  // FIXME !?
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   151
  extends Session.Entity
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   152
{
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   153
  /* classification */
34500
384427c750c8 state_results: separate buffer for messages from running command;
wenzelm
parents: 34497
diff changeset
   154
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 34871
diff changeset
   155
  def is_command: Boolean = !span.isEmpty && span.head.is_command
34865
104298db6abf Outer_Lex.is_ignored;
wenzelm
parents: 34860
diff changeset
   156
  def is_ignored: Boolean = span.forall(_.is_ignored)
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   157
  def is_malformed: Boolean = !is_command && !is_ignored
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   158
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 34871
diff changeset
   159
  def name: String = if (is_command) span.head.content else ""
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   160
  override def toString =
37373
25078ba44436 tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
wenzelm
parents: 37197
diff changeset
   161
    id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
34495
722533c532da Command: added name field and toString;
wenzelm
parents: 34491
diff changeset
   162
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   163
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   164
  /* source text */
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   165
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   166
  val source: String = span.map(_.source).mkString
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   167
  def source(i: Int, j: Int): String = source.substring(i, j)
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   168
  def length: Int = source.length
34855
81d0410dc3ac iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents: 34835
diff changeset
   169
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   170
  lazy val symbol_index = new Symbol.Index(source)
34593
cf37a9f988bf ignore unchanged commands
immler@in.tum.de
parents: 34577
diff changeset
   171
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   172
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   173
  /* accumulated messages */
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   174
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   175
  @volatile protected var state = new Command.State(this)
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   176
  def current_state: Command.State = state
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   177
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   178
  private case class Consume(message: XML.Tree, forward: Command => Unit)
34832
d785f72ef388 more explicit treatment of command/document state;
wenzelm
parents: 34823
diff changeset
   179
  private case object Assign
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   180
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   181
  private val accumulator = actor {
34832
d785f72ef388 more explicit treatment of command/document state;
wenzelm
parents: 34823
diff changeset
   182
    var assigned = false
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   183
    loop {
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   184
      react {
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   185
        case Consume(message, forward) if !assigned =>
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   186
          val old_state = state
37178
d52f934f8ff6 accumulate only local results -- no proper history support yet;
wenzelm
parents: 37129
diff changeset
   187
          state = old_state.accumulate(message)
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   188
          if (!(state eq old_state)) forward(static_parent getOrElse this)
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   189
34832
d785f72ef388 more explicit treatment of command/document state;
wenzelm
parents: 34823
diff changeset
   190
        case Assign =>
34835
67733fd0e3fa back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents: 34832
diff changeset
   191
          assigned = true  // single assignment
34832
d785f72ef388 more explicit treatment of command/document state;
wenzelm
parents: 34823
diff changeset
   192
          reply(())
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   193
37189
2b4e52ecf6fc tuned messages;
wenzelm
parents: 37178
diff changeset
   194
        case bad => System.err.println("Command accumulator: ignoring bad message " + bad)
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   195
      }
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   196
    }
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   197
  }
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   198
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   199
  def consume(message: XML.Tree, forward: Command => Unit)
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   200
  {
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   201
    accumulator ! Consume(message, forward)
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   202
  }
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   203
38363
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38362
diff changeset
   204
  def assign_exec(exec_id: Document.Exec_ID): Command =
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   205
  {
38363
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38362
diff changeset
   206
    val cmd = new Command(exec_id, span, Some(this))
34832
d785f72ef388 more explicit treatment of command/document state;
wenzelm
parents: 34823
diff changeset
   207
    accumulator !? Assign
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   208
    cmd.state = current_state
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   209
    cmd
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
   210
  }
34676
9e725d34df7b Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents: 34675
diff changeset
   211
9e725d34df7b Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents: 34675
diff changeset
   212
9e725d34df7b Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents: 34675
diff changeset
   213
  /* markup */
34508
422a43b76f77 eliminated Command.Status.REMOVE/REMOVED;
wenzelm
parents: 34500
diff changeset
   214
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   215
  lazy val empty_markup = new Markup_Text(Nil, source)
34676
9e725d34df7b Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents: 34675
diff changeset
   216
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34708
diff changeset
   217
  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
34699
wenzelm
parents: 34698
diff changeset
   218
  {
34703
ff037c17332a minor tuning;
wenzelm
parents: 34699
diff changeset
   219
    val start = symbol_index.decode(begin)
ff037c17332a minor tuning;
wenzelm
parents: 34699
diff changeset
   220
    val stop = symbol_index.decode(end)
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34708
diff changeset
   221
    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
34500
384427c750c8 state_results: separate buffer for messages from running command;
wenzelm
parents: 34497
diff changeset
   222
  }
34676
9e725d34df7b Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents: 34675
diff changeset
   223
}