src/Pure/PIDE/command.scala
author wenzelm
Sun, 22 Aug 2010 16:37:15 +0200
changeset 38575 80d962964216
parent 38574 79cb7b4c908a
child 38577 4e4d3ea3725a
permissions -rw-r--r--
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     1
/*  Title:      Pure/PIDE/command.scala
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     2
    Author:     Fabian Immler, TU Munich
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     3
    Author:     Makarius
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     4
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     5
Prover commands with semantic state.
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     6
*/
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
diff changeset
     7
34871
e596a0b71f3c incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents: 34865
diff changeset
     8
package isabelle
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     9
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    10
34699
wenzelm
parents: 34698
diff changeset
    11
import scala.actors.Actor, Actor._
34497
184fda8cce04 more explicit indication of mutable collections;
wenzelm
parents: 34495
diff changeset
    12
import scala.collection.mutable
34486
7985efd78aa1 tuned handling of accumulated results;
wenzelm
parents: 34485
diff changeset
    13
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    14
34637
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    15
object Command
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    16
{
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
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    19
  case class State(
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    20
    val command: Command,
38480
e5eed57913d0 Command.status: full XML.Tree, i.e. Markup with potential "arguments";
wenzelm
parents: 38479
diff changeset
    21
    val status: List[XML.Tree],
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    22
    val reverse_results: List[XML.Tree],
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38476
diff changeset
    23
    val markup: Markup_Tree)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    24
  {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    25
    /* content */
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    26
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    27
    lazy val results = reverse_results.reverse
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    28
38362
754ad6340055 misc tuning and simplification;
wenzelm
parents: 38361
diff changeset
    29
    def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    30
38564
a6e2715fac5f parameterized type Markup_Tree.Node;
wenzelm
parents: 38480
diff changeset
    31
    def add_markup(node: Markup_Tree.Node[Any]): State = copy(markup = markup + node)
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38476
diff changeset
    32
38564
a6e2715fac5f parameterized type Markup_Tree.Node;
wenzelm
parents: 38480
diff changeset
    33
    def markup_root_node: Markup_Tree.Node[Any] =
38480
e5eed57913d0 Command.status: full XML.Tree, i.e. Markup with potential "arguments";
wenzelm
parents: 38479
diff changeset
    34
      new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38476
diff changeset
    35
    def markup_root: Markup_Tree = markup + markup_root_node
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    36
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    37
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    38
    /* message dispatch */
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    39
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    40
    def accumulate(message: XML.Tree): Command.State =
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    41
      message match {
38480
e5eed57913d0 Command.status: full XML.Tree, i.e. Markup with potential "arguments";
wenzelm
parents: 38479
diff changeset
    42
        case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
38572
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    43
        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    44
          (this /: msgs)((state, msg) =>
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    45
            msg match {
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    46
              case XML.Elem(Markup(name, atts), args)
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    47
              if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    48
                val range = command.decode_range(Position.get_range(atts).get)
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    49
                val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    50
                val node = Markup_Tree.Node[Any](range, XML.Elem(Markup(name, props), args))
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    51
                add_markup(node)
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    52
              case _ => System.err.println("Ignored report message: " + msg); state
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    53
            })
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    54
        case _ => add_result(message)
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    55
      }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    56
  }
38367
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    57
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    58
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    59
  /* unparsed dummy commands */
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    60
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    61
  def unparsed(source: String) =
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    62
    new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    63
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    64
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    65
34697
3d4874198e62 State: immutable;
wenzelm
parents: 34688
diff changeset
    66
class Command(
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37373
diff changeset
    67
    val id: Document.Command_ID,
38373
wenzelm
parents: 38370
diff changeset
    68
    val span: List[Token])
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    69
{
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
    70
  /* classification */
34500
384427c750c8 state_results: separate buffer for messages from running command;
wenzelm
parents: 34497
diff changeset
    71
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 34871
diff changeset
    72
  def is_command: Boolean = !span.isEmpty && span.head.is_command
34865
104298db6abf Outer_Lex.is_ignored;
wenzelm
parents: 34860
diff changeset
    73
  def is_ignored: Boolean = span.forall(_.is_ignored)
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
    74
  def is_malformed: Boolean = !is_command && !is_ignored
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
    75
38367
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    76
  def is_unparsed = id == Document.NO_ID
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    77
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 34871
diff changeset
    78
  def name: String = if (is_command) span.head.content else ""
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
    79
  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
    80
    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
    81
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
    82
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
    83
  /* source text */
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    84
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
    85
  val source: String = span.map(_.source).mkString
38426
2858ec7b6dd8 specific types Text.Offset and Text.Range;
wenzelm
parents: 38415
diff changeset
    86
  def source(range: Text.Range): String = source.substring(range.start, range.stop)
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
    87
  def length: Int = source.length
38572
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    88
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38476
diff changeset
    89
  val range: Text.Range = Text.Range(0, length)
34855
81d0410dc3ac iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents: 34835
diff changeset
    90
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
    91
  lazy val symbol_index = new Symbol.Index(source)
38572
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    92
  def decode_range(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
    93
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
    94
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
    95
  /* accumulated results */
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
    96
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38476
diff changeset
    97
  val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
34676
9e725d34df7b Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents: 34675
diff changeset
    98
}