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