author | wenzelm |
Tue, 08 Dec 2009 16:30:20 +0100 | |
changeset 34760 | dc7f5e0d9d27 |
parent 34759 | bfea7839d9e1 |
child 34769 | 826525fc5285 |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
34501 | 2 |
* Higher-level prover communication: interactive document model |
34407 | 3 |
* |
4 |
* @author Johannes Hölzl, TU Munich |
|
5 |
* @author Fabian Immler, TU Munich |
|
34453 | 6 |
* @author Makarius |
34407 | 7 |
*/ |
8 |
||
34760 | 9 |
package isabelle.proofdocument |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
10 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
11 |
|
34703 | 12 |
import scala.actors.Actor, Actor._ |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
13 |
|
34671 | 14 |
import javax.swing.JTextArea |
34456 | 15 |
|
34501 | 16 |
import isabelle.jedit.Isabelle |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
|
34703 | 18 |
|
34742 | 19 |
class Prover(system: Isabelle_System, logic: String) |
34453 | 20 |
{ |
34724
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34723
diff
changeset
|
21 |
/* incoming messages */ |
34730 | 22 |
|
34721
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
23 |
private var prover_ready = false |
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
24 |
|
34742 | 25 |
private val receiver = new Actor { |
26 |
def act() { |
|
27 |
loop { |
|
28 |
react { |
|
29 |
case result: Isabelle_Process.Result => handle_result(result) |
|
30 |
case change: Change if prover_ready => handle_change(change) |
|
31 |
case bad if prover_ready => System.err.println("prover: ignoring bad message " + bad) |
|
32 |
} |
|
34721
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
33 |
} |
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
34 |
} |
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
35 |
} |
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
36 |
|
34742 | 37 |
def input(change: Change) { receiver ! change } |
38 |
||
34721
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
39 |
|
34724
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34723
diff
changeset
|
40 |
/* outgoing messages */ |
34730 | 41 |
|
34724
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34723
diff
changeset
|
42 |
val command_change = new Event_Bus[Command] |
34760 | 43 |
val document_change = new Event_Bus[Proof_Document] |
34724
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34723
diff
changeset
|
44 |
|
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34723
diff
changeset
|
45 |
|
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
46 |
/* prover process */ |
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
47 |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
48 |
private val process = |
34742 | 49 |
new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document |
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
50 |
|
34730 | 51 |
|
34720 | 52 |
/* outer syntax keywords and completion */ |
53 |
||
34723 | 54 |
@volatile private var _command_decls = Map[String, String]() |
55 |
def command_decls() = _command_decls |
|
56 |
||
34720 | 57 |
@volatile private var _keyword_decls = Set[String]() |
58 |
def keyword_decls() = _keyword_decls |
|
59 |
||
60 |
@volatile private var _completion = Isabelle.completion |
|
61 |
def completion() = _completion |
|
62 |
||
63 |
||
34509 | 64 |
/* document state information */ |
65 |
||
34721
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
66 |
@volatile private var states = Map[Isar_Document.State_ID, Command_State]() |
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
67 |
@volatile private var commands = Map[Isar_Document.Command_ID, Command]() |
34654 | 68 |
val document_0 = |
34760 | 69 |
Proof_Document.empty. |
34740 | 70 |
set_command_keyword((s: String) => command_decls().contains(s)) |
34721
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
71 |
@volatile private var document_versions = List(document_0) |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
72 |
|
34690 | 73 |
def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id) |
34760 | 74 |
def document(id: Isar_Document.Document_ID): Option[Proof_Document] = |
34740 | 75 |
document_versions.find(_.id == id) |
34730 | 76 |
|
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
77 |
|
34721
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
78 |
/* prover results */ |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
79 |
|
34728
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
80 |
val output_text_view = new JTextArea // FIXME separate jEdit component |
34671 | 81 |
|
34615 | 82 |
private def handle_result(result: Isabelle_Process.Result) |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
83 |
{ |
34728
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
84 |
// FIXME separate jEdit component |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
85 |
Swing_Thread.later { output_text_view.append(result.toString + "\n") } |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
86 |
|
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
87 |
val message = Isabelle_Process.parse_message(system, result) |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
88 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
89 |
val state = |
34740 | 90 |
Position.id_of(result.props) match { |
91 |
case None => None |
|
92 |
case Some(id) => commands.get(id) orElse states.get(id) orElse None |
|
93 |
} |
|
34724
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34723
diff
changeset
|
94 |
if (state.isDefined) state.get ! (this, message) |
34728
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
95 |
else if (result.kind == Isabelle_Process.Kind.STATUS) { |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
96 |
//{{{ global status message |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
97 |
message match { |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
98 |
case XML.Elem(Markup.MESSAGE, _, elems) => |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
99 |
for (elem <- elems) { |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
100 |
elem match { |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
101 |
// document edits |
34740 | 102 |
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) => |
103 |
document_versions.find(_.id == doc_id) match { |
|
104 |
case Some(doc) => |
|
105 |
for { |
|
106 |
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) |
|
34741 | 107 |
<- edits } |
108 |
{ |
|
109 |
commands.get(cmd_id) match { |
|
110 |
case Some(cmd) => |
|
111 |
val state = new Command_State(cmd) |
|
112 |
states += (state_id -> state) |
|
113 |
doc.states += (cmd -> state) |
|
34742 | 114 |
command_change.event(cmd) // FIXME really!? |
34741 | 115 |
case None => |
116 |
} |
|
34740 | 117 |
} |
118 |
case None => |
|
34728
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
119 |
} |
34730 | 120 |
|
34741 | 121 |
// command and keyword declarations |
34740 | 122 |
case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => |
34728
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
123 |
_command_decls += (name -> kind) |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
124 |
_completion += name |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
125 |
case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
126 |
_keyword_decls += name |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
127 |
_completion += name |
34453 | 128 |
|
34741 | 129 |
// process ready (after initialization) |
34728
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
130 |
case XML.Elem(Markup.READY, _, _) => prover_ready = true |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
131 |
|
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
132 |
case _ => |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
133 |
} |
34728
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
134 |
} |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
135 |
case _ => |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
136 |
} |
e3df9c8699ea
handle_result: no special treatment of outer markup (it is now properly identified by the prover);
wenzelm
parents:
34724
diff
changeset
|
137 |
//}}} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
138 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
139 |
} |
34453 | 140 |
|
34721
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
141 |
|
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
142 |
/* document changes */ |
4f3e352dde8b
Prover: just one actor -- single message dispatch;
wenzelm
parents:
34720
diff
changeset
|
143 |
|
34729 | 144 |
def begin_document(path: String) { |
34650 | 145 |
process.begin_document(document_0.id, path) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
146 |
} |
34453 | 147 |
|
34729 | 148 |
def handle_change(change: Change) { |
149 |
val old = document(change.parent.get.id).get |
|
150 |
val (doc, changes) = old.text_changed(change) |
|
151 |
document_versions ::= doc |
|
152 |
||
34709 | 153 |
val id_changes = changes map { case (c1, c2) => |
34730 | 154 |
(c1.map(_.id).getOrElse(document_0.id), |
155 |
c2 match { |
|
156 |
case None => None |
|
157 |
case Some(command) => |
|
158 |
commands += (command.id -> command) |
|
159 |
process.define_command(command.id, system.symbols.encode(command.content)) |
|
160 |
Some(command.id) |
|
161 |
}) |
|
34660 | 162 |
} |
163 |
process.edit_document(old.id, doc.id, id_changes) |
|
34729 | 164 |
|
165 |
document_change.event(doc) |
|
34650 | 166 |
} |
34742 | 167 |
|
168 |
||
169 |
/* main controls */ |
|
170 |
||
171 |
def start() { receiver.start() } |
|
172 |
||
173 |
def stop() { process.kill() } |
|
34453 | 174 |
} |