src/Pure/PIDE/command.scala
author wenzelm
Wed, 04 Apr 2012 14:19:47 +0200
changeset 47336 bed4b2738d8a
parent 47012 0e246130486b
child 47459 373e456149cc
permissions -rw-r--r--
separate module for prover command execution;
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
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 40572
diff changeset
    10
import java.lang.System
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    11
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    12
import scala.collection.mutable
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    13
import scala.collection.immutable.SortedMap
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    14
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    15
34637
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    16
object Command
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    17
{
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    18
  /** accumulated results from prover **/
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    19
43714
3749d1e6dde9 tuned signature;
wenzelm
parents: 43662
diff changeset
    20
  sealed case class State(
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    21
    val command: Command,
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    22
    val status: List[Markup] = Nil,
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    23
    val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    24
    val markup: Markup_Tree = Markup_Tree.empty)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    25
  {
46152
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    26
    /* accumulate content */
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    27
46152
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    28
    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
    29
    private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    30
46152
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    31
    def + (message: XML.Elem): Command.State =
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    32
      message match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45644
diff changeset
    33
        case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
38714
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    34
          (this /: msgs)((state, msg) =>
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    35
            msg match {
46152
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    36
              case elem @ XML.Elem(markup, Nil) =>
46910
3e068ef04b42 clarified command state -- markup within proper_range, excluding trailing whitespace;
wenzelm
parents: 46813
diff changeset
    37
                state.add_status(markup).add_markup(Text.Info(command.proper_range, elem))
46152
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    38
38714
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    39
              case _ => System.err.println("Ignored status message: " + msg); state
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    40
            })
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
    41
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45644
diff changeset
    42
        case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) =>
38572
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    43
          (this /: msgs)((state, msg) =>
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    44
            msg match {
39173
ed3946086358 Command.State.accumulate: check actual source range;
wenzelm
parents: 39172
diff changeset
    45
              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
ed3946086358 Command.State.accumulate: check actual source range;
wenzelm
parents: 39172
diff changeset
    46
              if id == command.id && command.range.contains(command.decode(raw_range)) =>
ed3946086358 Command.State.accumulate: check actual source range;
wenzelm
parents: 39172
diff changeset
    47
                val range = command.decode(raw_range)
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    48
                val props = Position.purge(atts)
45455
4f974c0c5c2f prefer statically typed Text.Markup;
wenzelm
parents: 44959
diff changeset
    49
                val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
38723
wenzelm
parents: 38722
diff changeset
    50
                state.add_markup(info)
40572
2315c3daee74 avoid spam;
wenzelm
parents: 40454
diff changeset
    51
              case _ =>
2315c3daee74 avoid spam;
wenzelm
parents: 40454
diff changeset
    52
                // FIXME System.err.println("Ignored report message: " + msg)
2315c3daee74 avoid spam;
wenzelm
parents: 40454
diff changeset
    53
                state
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    54
            })
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    55
        case XML.Elem(Markup(name, atts), body) =>
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    56
          atts match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45644
diff changeset
    57
            case Isabelle_Markup.Serial(i) =>
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38877
diff changeset
    58
              val result = XML.Elem(Markup(name, Position.purge(atts)), body)
46152
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    59
              val st0 = copy(results = results + (i -> result))
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39173
diff changeset
    60
              val st1 =
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
    61
                if (Protocol.is_tracing(message)) st0
39622
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39441
diff changeset
    62
                else
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
    63
                  (st0 /: Protocol.message_positions(command, message))(
39622
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39441
diff changeset
    64
                    (st, range) => st.add_markup(Text.Info(range, result)))
46152
793cecd4ffc0 accumulate status as regular markup for command range;
wenzelm
parents: 45709
diff changeset
    65
              val st2 = (st1 /: Protocol.message_reports(message))(_ + _)
39622
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39441
diff changeset
    66
              st2
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    67
            case _ => System.err.println("Ignored message without serial number: " + message); this
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    68
          }
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    69
      }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    70
  }
38367
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    71
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    72
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    73
  /* make commands */
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    74
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    75
  def apply(id: Document.Command_ID, node_name: Document.Node.Name, toks: List[Token]): Command =
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    76
  {
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    77
    val source: String =
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    78
      toks match {
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    79
        case List(tok) => tok.source
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    80
        case _ => toks.map(_.source).mkString
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    81
      }
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    82
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    83
    val span = new mutable.ListBuffer[Token]
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    84
    var i = 0
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    85
    for (Token(kind, s) <- toks) {
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    86
      val n = s.length
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    87
      val s1 = source.substring(i, i + n)
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    88
      span += Token(kind, s1)
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    89
      i += n
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    90
    }
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    91
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    92
    new Command(id, node_name, span.toList, source)
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    93
  }
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    94
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 39622
diff changeset
    95
  def unparsed(source: String): Command =
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    96
    Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
    97
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
    98
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
    99
  /* perspective */
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   100
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   101
  object Perspective
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   102
  {
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   103
    val empty: Perspective = Perspective(Nil)
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   104
  }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   105
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   106
  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
   107
  {
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   108
    def same(that: Perspective): Boolean =
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   109
    {
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   110
      val cmds1 = this.commands
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   111
      val cmds2 = that.commands
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   112
      require(cmds1.forall(_.is_defined))
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   113
      require(cmds2.forall(_.is_defined))
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   114
      cmds1.length == cmds2.length &&
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   115
        (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   116
    }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   117
  }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   118
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   119
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   120
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46164
diff changeset
   121
final class Command private(
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37373
diff changeset
   122
    val id: Document.Command_ID,
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44607
diff changeset
   123
    val node_name: Document.Node.Name,
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   124
    val span: List[Token],
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   125
    val source: String)
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   126
{
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   127
  /* classification */
34500
384427c750c8 state_results: separate buffer for messages from running command;
wenzelm
parents: 34497
diff changeset
   128
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   129
  def is_defined: Boolean = id != Document.no_id
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   130
47012
0e246130486b clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents: 46910
diff changeset
   131
  val is_ignored: Boolean = span.forall(_.is_ignored)
0e246130486b clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents: 46910
diff changeset
   132
  val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_unparsed))
0e246130486b clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents: 46910
diff changeset
   133
  def is_command: Boolean = !is_ignored && !is_malformed
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   134
47012
0e246130486b clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents: 46910
diff changeset
   135
  def name: String =
0e246130486b clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents: 46910
diff changeset
   136
    span.find(_.is_command) match { case Some(tok) => tok.content case _ => "" }
0e246130486b clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents: 46910
diff changeset
   137
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   138
  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
   139
    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
   140
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   141
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   142
  /* source text */
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   143
46813
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   144
  def length: Int = source.length
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   145
  val range: Text.Range = Text.Range(0, length)
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   146
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   147
  val proper_range: Text.Range =
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   148
    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   149
38426
2858ec7b6dd8 specific types Text.Offset and Text.Range;
wenzelm
parents: 38415
diff changeset
   150
  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
   151
38877
682c4932b3cc Command.newlines: account for physical newlines;
wenzelm
parents: 38872
diff changeset
   152
  val newlines =
682c4932b3cc Command.newlines: account for physical newlines;
wenzelm
parents: 38872
diff changeset
   153
    (0 /: Symbol.iterator(source)) {
682c4932b3cc Command.newlines: account for physical newlines;
wenzelm
parents: 38872
diff changeset
   154
      case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
682c4932b3cc Command.newlines: account for physical newlines;
wenzelm
parents: 38872
diff changeset
   155
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   156
  lazy val symbol_index = new Symbol.Index(source)
38579
ce46a6f55bce tuned signature;
wenzelm
parents: 38577
diff changeset
   157
  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
ce46a6f55bce tuned signature;
wenzelm
parents: 38577
diff changeset
   158
  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
   159
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   160
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   161
  /* accumulated results */
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   162
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
   163
  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
   164
}