wenzelm@34410
|
1 |
/*
|
wenzelm@34410
|
2 |
* Prover commands with semantic state
|
wenzelm@34410
|
3 |
*
|
wenzelm@34410
|
4 |
* @author Johannes Hölzl, TU Munich
|
wenzelm@34410
|
5 |
* @author Fabian Immler, TU Munich
|
wenzelm@34410
|
6 |
*/
|
wenzelm@34410
|
7 |
|
wenzelm@34763
|
8 |
package isabelle.proofdocument
|
wenzelm@34321
|
9 |
|
wenzelm@34454
|
10 |
|
wenzelm@34702
|
11 |
import scala.actors.Actor, Actor._
|
wenzelm@34500
|
12 |
import scala.collection.mutable
|
wenzelm@34489
|
13 |
|
wenzelm@34780
|
14 |
import isabelle.jedit.Isabelle
|
immler@34678
|
15 |
|
wenzelm@34454
|
16 |
|
wenzelm@34640
|
17 |
object Command
|
wenzelm@34640
|
18 |
{
|
wenzelm@34640
|
19 |
object Status extends Enumeration
|
wenzelm@34640
|
20 |
{
|
wenzelm@34321
|
21 |
val UNPROCESSED = Value("UNPROCESSED")
|
wenzelm@34321
|
22 |
val FINISHED = Value("FINISHED")
|
wenzelm@34321
|
23 |
val FAILED = Value("FAILED")
|
wenzelm@34321
|
24 |
}
|
wenzelm@34710
|
25 |
|
wenzelm@34710
|
26 |
case class HighlightInfo(highlight: String) { override def toString = highlight }
|
wenzelm@34720
|
27 |
case class TypeInfo(ty: String)
|
wenzelm@34710
|
28 |
case class RefInfo(file: Option[String], line: Option[Int],
|
wenzelm@34720
|
29 |
command_id: Option[String], offset: Option[Int])
|
wenzelm@34321
|
30 |
}
|
wenzelm@34321
|
31 |
|
wenzelm@34454
|
32 |
|
wenzelm@34700
|
33 |
class Command(
|
wenzelm@34816
|
34 |
val id: Isar_Document.Command_ID,
|
wenzelm@34862
|
35 |
val span: Thy_Syntax.Span)
|
wenzelm@34818
|
36 |
extends Session.Entity
|
wenzelm@34454
|
37 |
{
|
wenzelm@34862
|
38 |
/* classification */
|
wenzelm@34503
|
39 |
|
wenzelm@34862
|
40 |
def is_command: Boolean = !span.isEmpty && span.first.is_command
|
wenzelm@34862
|
41 |
def is_ignored: Boolean = span.forall(tok => tok.is_space || tok.is_comment)
|
wenzelm@34862
|
42 |
def is_malformed: Boolean = !is_command && !is_ignored
|
wenzelm@34498
|
43 |
|
wenzelm@34862
|
44 |
def name: String = if (is_command) span.first.content else ""
|
wenzelm@34862
|
45 |
override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
|
immler@34399
|
46 |
|
wenzelm@34858
|
47 |
|
wenzelm@34862
|
48 |
/* source text */
|
wenzelm@34862
|
49 |
|
wenzelm@34862
|
50 |
val source: String = span.map(_.source).mkString
|
wenzelm@34862
|
51 |
def source(i: Int, j: Int): String = source.substring(i, j)
|
wenzelm@34862
|
52 |
def length: Int = source.length
|
wenzelm@34862
|
53 |
|
wenzelm@34862
|
54 |
lazy val symbol_index = new Symbol.Index(source)
|
immler@34596
|
55 |
|
wenzelm@34818
|
56 |
|
wenzelm@34818
|
57 |
/* accumulated messages */
|
wenzelm@34818
|
58 |
|
wenzelm@34818
|
59 |
@volatile protected var state = new State(this)
|
wenzelm@34818
|
60 |
def current_state: State = state
|
wenzelm@34818
|
61 |
|
wenzelm@34818
|
62 |
private case class Consume(session: Session, message: XML.Tree)
|
wenzelm@34835
|
63 |
private case object Assign
|
wenzelm@34818
|
64 |
|
wenzelm@34818
|
65 |
private val accumulator = actor {
|
wenzelm@34835
|
66 |
var assigned = false
|
wenzelm@34818
|
67 |
loop {
|
wenzelm@34818
|
68 |
react {
|
wenzelm@34835
|
69 |
case Consume(session: Session, message: XML.Tree) if !assigned =>
|
wenzelm@34818
|
70 |
state = state.+(session, message)
|
wenzelm@34818
|
71 |
|
wenzelm@34835
|
72 |
case Assign =>
|
wenzelm@34838
|
73 |
assigned = true // single assignment
|
wenzelm@34835
|
74 |
reply(())
|
wenzelm@34818
|
75 |
|
wenzelm@34818
|
76 |
case bad => System.err.println("command accumulator: ignoring bad message " + bad)
|
wenzelm@34818
|
77 |
}
|
wenzelm@34818
|
78 |
}
|
wenzelm@34818
|
79 |
}
|
wenzelm@34818
|
80 |
|
wenzelm@34818
|
81 |
def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
|
wenzelm@34818
|
82 |
|
wenzelm@34835
|
83 |
def assign_state(state_id: Isar_Document.State_ID): Command =
|
wenzelm@34818
|
84 |
{
|
wenzelm@34862
|
85 |
val cmd = new Command(state_id, span)
|
wenzelm@34835
|
86 |
accumulator !? Assign
|
wenzelm@34818
|
87 |
cmd.state = current_state
|
wenzelm@34818
|
88 |
cmd
|
wenzelm@34818
|
89 |
}
|
wenzelm@34640
|
90 |
|
immler@34679
|
91 |
|
immler@34679
|
92 |
/* markup */
|
immler@34679
|
93 |
|
wenzelm@34862
|
94 |
lazy val empty_markup = new Markup_Text(Nil, source)
|
immler@34679
|
95 |
|
wenzelm@34720
|
96 |
def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
|
wenzelm@34702
|
97 |
{
|
wenzelm@34706
|
98 |
val start = symbol_index.decode(begin)
|
wenzelm@34706
|
99 |
val stop = symbol_index.decode(end)
|
wenzelm@34720
|
100 |
new Markup_Tree(new Markup_Node(start, stop, info), Nil)
|
wenzelm@34503
|
101 |
}
|
immler@34679
|
102 |
}
|