src/Pure/PIDE/command.scala
author wenzelm
Fri, 05 Jul 2013 22:58:24 +0200
changeset 52536 3a35ce87a55c
parent 52535 b7badd371e4d
child 52642 84eb792224a8
permissions -rw-r--r--
tuned signature; tuned comments;
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
52536
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
     5
Prover commands with accumulated results from execution.
36676
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
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    11
import scala.collection.mutable
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    12
import scala.collection.immutable.SortedMap
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    13
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
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
{
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    17
  /** accumulated results from prover **/
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    18
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    19
  /* results */
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    20
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    21
  object Results
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    22
  {
51496
cb677987b7e3 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents: 51494
diff changeset
    23
    type Entry = (Long, XML.Tree)
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    24
    val empty = new Results(SortedMap.empty)
51496
cb677987b7e3 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents: 51494
diff changeset
    25
    def make(es: Iterable[Results.Entry]): Results = (empty /: es.iterator)(_ + _)
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    26
    def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    27
  }
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    28
51494
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    29
  final class Results private(private val rep: SortedMap[Long, XML.Tree])
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    30
  {
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    31
    def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    32
    def get(serial: Long): Option[XML.Tree] = rep.get(serial)
51496
cb677987b7e3 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents: 51494
diff changeset
    33
    def entries: Iterator[Results.Entry] = rep.iterator
50508
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    34
51496
cb677987b7e3 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents: 51494
diff changeset
    35
    def + (entry: Results.Entry): Results =
50508
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    36
      if (defined(entry._1)) this
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    37
      else new Results(rep + entry)
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    38
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    39
    def ++ (other: Results): Results =
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    40
      if (this eq other) this
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    41
      else if (rep.isEmpty) other
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    42
      else (this /: other.entries)(_ + _)
50540
wenzelm
parents: 50508
diff changeset
    43
51494
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    44
    override def hashCode: Int = rep.hashCode
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    45
    override def equals(that: Any): Boolean =
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    46
      that match {
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    47
        case other: Results => rep == other.rep
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    48
        case _ => false
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    49
      }
50540
wenzelm
parents: 50508
diff changeset
    50
    override def toString: String = entries.mkString("Results(", ", ", ")")
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    51
  }
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    52
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    53
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    54
  /* state */
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
    55
43714
3749d1e6dde9 tuned signature;
wenzelm
parents: 43662
diff changeset
    56
  sealed case class State(
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
    57
    command: Command,
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
    58
    status: List[Markup] = Nil,
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    59
    results: Results = Results.empty,
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
    60
    markup: Markup_Tree = Markup_Tree.empty)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    61
  {
49645
5a0817ec0314 tuned signature;
wenzelm
parents: 49614
diff changeset
    62
    def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
5a0817ec0314 tuned signature;
wenzelm
parents: 49614
diff changeset
    63
      markup.to_XML(command.range, command.source, filter)
49614
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49527
diff changeset
    64
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49527
diff changeset
    65
51494
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    66
    /* content */
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    67
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    68
    def eq_content(other: State): Boolean =
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    69
      command.source == other.command.source &&
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    70
      status == other.status &&
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    71
      results == other.results &&
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    72
      markup == other.markup
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    73
46152
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    74
    private def add_status(st: Markup): State = copy(status = st :: status)
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    75
    private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    76
52531
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
    77
    def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    78
      message match {
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50163
diff changeset
    79
        case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
38714
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    80
          (this /: msgs)((state, msg) =>
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    81
            msg match {
46152
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    82
              case elem @ XML.Elem(markup, Nil) =>
50499
f496b2b7bafb rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
wenzelm
parents: 50201
diff changeset
    83
                state.add_status(markup)
f496b2b7bafb rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
wenzelm
parents: 50201
diff changeset
    84
                  .add_markup(Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
46152
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    85
52536
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
    86
              case _ =>
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
    87
                java.lang.System.err.println("Ignored status message: " + msg)
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
    88
                state
38714
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    89
            })
38581
d503a0912e14 simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents: 38579
diff changeset
    90
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50163
diff changeset
    91
        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
38572
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    92
          (this /: msgs)((state, msg) =>
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    93
            msg match {
39173
ed3946086358 Command.State.accumulate: check actual source range;
wenzelm
parents: 39172
diff changeset
    94
              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
49527
b96e4a39cc3e accumulate under exec_id as well;
wenzelm
parents: 49526
diff changeset
    95
              if (id == command.id || id == alt_id) &&
b96e4a39cc3e accumulate under exec_id as well;
wenzelm
parents: 49526
diff changeset
    96
                  command.range.contains(command.decode(raw_range)) =>
39173
ed3946086358 Command.State.accumulate: check actual source range;
wenzelm
parents: 39172
diff changeset
    97
                val range = command.decode(raw_range)
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    98
                val props = Position.purge(atts)
45455
4f974c0c5c2f prefer statically typed Text.Markup;
wenzelm
parents: 44959
diff changeset
    99
                val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
38723
wenzelm
parents: 38722
diff changeset
   100
                state.add_markup(info)
49526
6d1465c00f2e more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
wenzelm
parents: 49493
diff changeset
   101
              case XML.Elem(Markup(name, atts), args)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50163
diff changeset
   102
              if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
49037
d7a1973b063c more markup for failed goal forks, reusing "bad";
wenzelm
parents: 48922
diff changeset
   103
                val range = command.proper_range
d7a1973b063c more markup for failed goal forks, reusing "bad";
wenzelm
parents: 48922
diff changeset
   104
                val props = Position.purge(atts)
d7a1973b063c more markup for failed goal forks, reusing "bad";
wenzelm
parents: 48922
diff changeset
   105
                val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
d7a1973b063c more markup for failed goal forks, reusing "bad";
wenzelm
parents: 48922
diff changeset
   106
                state.add_markup(info)
40572
2315c3daee74 avoid spam;
wenzelm
parents: 40454
diff changeset
   107
              case _ =>
52536
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
   108
                // FIXME java.lang.System.err.println("Ignored report message: " + msg)
40572
2315c3daee74 avoid spam;
wenzelm
parents: 40454
diff changeset
   109
                state
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   110
            })
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
   111
        case XML.Elem(Markup(name, atts), body) =>
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
   112
          atts match {
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50163
diff changeset
   113
            case Markup.Serial(i) =>
50163
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents: 50158
diff changeset
   114
              val props = Position.purge(atts)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50163
diff changeset
   115
              val message1 = XML.Elem(Markup(Markup.message(name), props), body)
50163
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents: 50158
diff changeset
   116
              val message2 = XML.Elem(Markup(name, props), body)
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents: 50158
diff changeset
   117
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents: 50158
diff changeset
   118
              val st0 = copy(results = results + (i -> message1))
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39173
diff changeset
   119
              val st1 =
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   120
                if (Protocol.is_inlined(message))
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   121
                  (st0 /: Protocol.message_positions(command, message))(
50163
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents: 50158
diff changeset
   122
                    (st, range) => st.add_markup(Text.Info(range, message2)))
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   123
                else st0
49445
638cefe3ee99 earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents: 49418
diff changeset
   124
638cefe3ee99 earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents: 49418
diff changeset
   125
              st1
52536
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
   126
            case _ =>
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
   127
              java.lang.System.err.println("Ignored message without serial number: " + message)
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
   128
              this
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
   129
          }
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   130
      }
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52524
diff changeset
   131
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52524
diff changeset
   132
    def ++ (other: State): State =
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52524
diff changeset
   133
      copy(results = results ++ other.results)  // FIXME merge more content!?
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   134
  }
38367
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
   135
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
   136
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   137
  /* make commands */
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   138
48745
184158734fba tuned signature;
wenzelm
parents: 48718
diff changeset
   139
  type Span = List[Token]
184158734fba tuned signature;
wenzelm
parents: 48718
diff changeset
   140
52524
wenzelm
parents: 52509
diff changeset
   141
  def apply(
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   142
    id: Document_ID.Command,
52524
wenzelm
parents: 52509
diff changeset
   143
    node_name: Document.Node.Name,
wenzelm
parents: 52509
diff changeset
   144
    span: Span,
wenzelm
parents: 52509
diff changeset
   145
    results: Results = Results.empty,
wenzelm
parents: 52509
diff changeset
   146
    markup: Markup_Tree = Markup_Tree.empty): Command =
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   147
  {
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   148
    val source: String =
48745
184158734fba tuned signature;
wenzelm
parents: 48718
diff changeset
   149
      span match {
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   150
        case List(tok) => tok.source
48745
184158734fba tuned signature;
wenzelm
parents: 48718
diff changeset
   151
        case _ => span.map(_.source).mkString
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   152
      }
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   153
48745
184158734fba tuned signature;
wenzelm
parents: 48718
diff changeset
   154
    val span1 = new mutable.ListBuffer[Token]
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   155
    var i = 0
48745
184158734fba tuned signature;
wenzelm
parents: 48718
diff changeset
   156
    for (Token(kind, s) <- span) {
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   157
      val n = s.length
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   158
      val s1 = source.substring(i, i + n)
48745
184158734fba tuned signature;
wenzelm
parents: 48718
diff changeset
   159
      span1 += Token(kind, s1)
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   160
      i += n
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   161
    }
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   162
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   163
    new Command(id, node_name, span1.toList, source, results, markup)
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   164
  }
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   165
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   166
  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil)
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49359
diff changeset
   167
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   168
  def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   169
      : Command =
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   170
    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49359
diff changeset
   171
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   172
  def unparsed(source: String): Command =
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   173
    unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   174
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   175
  def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49359
diff changeset
   176
  {
49466
99ed1f422635 tuned signature;
wenzelm
parents: 49445
diff changeset
   177
    val text = XML.content(body)
99ed1f422635 tuned signature;
wenzelm
parents: 49445
diff changeset
   178
    val markup = Markup_Tree.from_XML(body)
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   179
    unparsed(id, text, results, markup)
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49359
diff changeset
   180
  }
49359
c1262d7389fb refined output panel: more value-oriented approach to update and caret focus;
wenzelm
parents: 49037
diff changeset
   181
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   182
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   183
  /* perspective */
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   184
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   185
  object Perspective
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   186
  {
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   187
    val empty: Perspective = Perspective(Nil)
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   188
  }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   189
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   190
  sealed case class Perspective(commands: List[Command])  // visible commands in canonical order
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   191
  {
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   192
    def same(that: Perspective): Boolean =
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   193
    {
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   194
      val cmds1 = this.commands
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   195
      val cmds2 = that.commands
48754
c2c1e5944536 clarified undefined, unparsed, unfinished command spans;
wenzelm
parents: 48745
diff changeset
   196
      require(!cmds1.exists(_.is_undefined))
c2c1e5944536 clarified undefined, unparsed, unfinished command spans;
wenzelm
parents: 48745
diff changeset
   197
      require(!cmds2.exists(_.is_undefined))
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   198
      cmds1.length == cmds2.length &&
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   199
        (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   200
    }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   201
  }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   202
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   203
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   204
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46164
diff changeset
   205
final class Command private(
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   206
    val id: Document_ID.Command,
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44607
diff changeset
   207
    val node_name: Document.Node.Name,
52535
b7badd371e4d tuned signature -- eliminated pointless type synonym;
wenzelm
parents: 52531
diff changeset
   208
    val span: List[Token],
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49359
diff changeset
   209
    val source: String,
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   210
    val init_results: Command.Results,
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49359
diff changeset
   211
    val init_markup: Markup_Tree)
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   212
{
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   213
  /* classification */
34500
384427c750c8 state_results: separate buffer for messages from running command;
wenzelm
parents: 34497
diff changeset
   214
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   215
  def is_undefined: Boolean = id == Document_ID.none
48754
c2c1e5944536 clarified undefined, unparsed, unfinished command spans;
wenzelm
parents: 48745
diff changeset
   216
  val is_unparsed: Boolean = span.exists(_.is_unparsed)
c2c1e5944536 clarified undefined, unparsed, unfinished command spans;
wenzelm
parents: 48745
diff changeset
   217
  val is_unfinished: Boolean = span.exists(_.is_unfinished)
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   218
48599
5e64b7770f35 tuned signature;
wenzelm
parents: 47459
diff changeset
   219
  val is_ignored: Boolean = !span.exists(_.is_proper)
48754
c2c1e5944536 clarified undefined, unparsed, unfinished command spans;
wenzelm
parents: 48745
diff changeset
   220
  val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error))
47012
0e246130486b clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents: 46910
diff changeset
   221
  def is_command: Boolean = !is_ignored && !is_malformed
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   222
47012
0e246130486b clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents: 46910
diff changeset
   223
  def name: String =
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48599
diff changeset
   224
    span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
47012
0e246130486b clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents: 46910
diff changeset
   225
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   226
  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
   227
    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
   228
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   229
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 52507
diff changeset
   230
  /* source */
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   231
46813
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   232
  def length: Int = source.length
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   233
  val range: Text.Range = Text.Range(0, length)
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   234
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   235
  val proper_range: Text.Range =
51048
123be08eed88 clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
wenzelm
parents: 50540
diff changeset
   236
    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
46813
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   237
38426
2858ec7b6dd8 specific types Text.Offset and Text.Range;
wenzelm
parents: 38415
diff changeset
   238
  def source(range: Text.Range): String = source.substring(range.start, range.stop)
38572
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
   239
52507
27925b58d6bd tuned signature;
wenzelm
parents: 51496
diff changeset
   240
  lazy val symbol_index = Symbol.Index(source)
38579
ce46a6f55bce tuned signature;
wenzelm
parents: 38577
diff changeset
   241
  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
ce46a6f55bce tuned signature;
wenzelm
parents: 38577
diff changeset
   242
  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   243
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   244
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   245
  /* accumulated results */
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   246
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   247
  val init_state: Command.State =
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   248
    Command.State(this, results = init_results, markup = init_markup)
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52524
diff changeset
   249
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52524
diff changeset
   250
  val empty_state: Command.State = Command.State(this)
34676
9e725d34df7b Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents: 34675
diff changeset
   251
}