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