author | immler@in.tum.de |
Thu, 19 Mar 2009 16:48:29 +0100 | |
changeset 34539 | 5d88e0681d44 |
parent 34538 | 20bfcca24658 |
parent 34533 | 35308320713a |
child 34540 | 50ae42f01d45 |
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 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
package isabelle.prover |
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 |
|
34497 | 12 |
import scala.collection.mutable |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34471
diff
changeset
|
13 |
import scala.collection.immutable.{TreeSet} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
14 |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
15 |
import scala.actors.Actor |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
16 |
import scala.actors.Actor._ |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
17 |
|
34456 | 18 |
import org.gjt.sp.util.Log |
19 |
||
34501 | 20 |
import isabelle.jedit.Isabelle |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
21 |
import isabelle.proofdocument.{StructureChange, ProofDocument, Text, Token} |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
22 |
import isabelle.IsarDocument |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
23 |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
24 |
object ProverEvents { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
25 |
case class Activate |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
26 |
case class SetEventBus(bus: EventBus[StructureChange]) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
27 |
case class SetIsCommandKeyword(is_command_keyword: String => Boolean) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
28 |
} |
34453 | 29 |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
30 |
class Prover(isabelle_system: IsabelleSystem, logic: String) extends Actor |
34453 | 31 |
{ |
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
32 |
/* prover process */ |
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
33 |
|
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
34 |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
35 |
private val process = |
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
36 |
{ |
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
37 |
val results = new EventBus[IsabelleProcess.Result] + handle_result |
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
38 |
results.logger = Log.log(Log.ERROR, null, _) |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
39 |
new IsabelleProcess(isabelle_system, results, "-m", "xsymbols", logic) with IsarDocument |
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
40 |
} |
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
41 |
|
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
42 |
def stop() { process.kill } |
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
43 |
|
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
44 |
|
34509 | 45 |
/* document state information */ |
46 |
||
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
47 |
private val states = new mutable.HashMap[IsarDocument.State_ID, Command] with |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
48 |
mutable.SynchronizedMap[IsarDocument.State_ID, Command] |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
49 |
private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
50 |
mutable.SynchronizedMap[IsarDocument.Command_ID, Command] |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
51 |
private val document_id0 = Isabelle.plugin.id() |
34539 | 52 |
private var document_versions = List((document_id0, ProofDocument.empty)) |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
53 |
|
34539 | 54 |
def document_id = document_versions.head._1 |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
55 |
def document = document_versions.head._2 |
34509 | 56 |
|
57 |
private var initialized = false |
|
58 |
||
59 |
||
34485 | 60 |
/* outer syntax keywords */ |
61 |
||
34465
ccadbf63e320
added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents:
34462
diff
changeset
|
62 |
val decl_info = new EventBus[(String, String)] |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
63 |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
64 |
private val keyword_decls = |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
65 |
new mutable.HashSet[String] with mutable.SynchronizedSet[String] { |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
66 |
override def +=(name: String) = { |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
67 |
decl_info.event(name, OuterKeyword.MINOR) |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
68 |
super.+=(name) |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
69 |
} |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
70 |
} |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
71 |
private val command_decls = |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
72 |
new mutable.HashMap[String, String] with mutable.SynchronizedMap[String, String] { |
34471
1dac47492863
decl_info: cover both commands and keywords, with kind;
wenzelm
parents:
34466
diff
changeset
|
73 |
override def +=(entry: (String, String)) = { |
1dac47492863
decl_info: cover both commands and keywords, with kind;
wenzelm
parents:
34466
diff
changeset
|
74 |
decl_info.event(entry) |
1dac47492863
decl_info: cover both commands and keywords, with kind;
wenzelm
parents:
34466
diff
changeset
|
75 |
super.+=(entry) |
34465
ccadbf63e320
added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents:
34462
diff
changeset
|
76 |
} |
ccadbf63e320
added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents:
34462
diff
changeset
|
77 |
} |
34485 | 78 |
|
79 |
||
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
80 |
/* completions */ |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
81 |
|
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34471
diff
changeset
|
82 |
var _completions = new TreeSet[String] |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34471
diff
changeset
|
83 |
def completions = _completions |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34471
diff
changeset
|
84 |
/* // TODO: ask Makarius to make Interpretation.symbols public (here: read-only as 'symbol_map') |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34471
diff
changeset
|
85 |
val map = isabelle.jedit.Isabelle.symbols.symbol_map |
34503 | 86 |
for (xsymb <- map.keys) { |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34471
diff
changeset
|
87 |
_completions += xsymb |
34503 | 88 |
if (map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev") |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34471
diff
changeset
|
89 |
} |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34471
diff
changeset
|
90 |
*/ |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34471
diff
changeset
|
91 |
decl_info += (k_v => _completions += k_v._1) |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
92 |
|
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
93 |
|
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
94 |
/* event handling */ |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
95 |
|
34456 | 96 |
val activated = new EventBus[Unit] |
97 |
val output_info = new EventBus[String] |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
98 |
var change_receiver = null: Actor |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
99 |
|
34509 | 100 |
private def handle_result(result: IsabelleProcess.Result) |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
101 |
{ |
34539 | 102 |
def command_change(c: Command) = this ! c |
34509 | 103 |
val (running, command) = |
104 |
result.props.find(p => p._1 == Markup.ID) match { |
|
105 |
case None => (false, null) |
|
106 |
case Some((_, id)) => |
|
107 |
if (commands.contains(id)) (false, commands(id)) |
|
108 |
else if (states.contains(id)) (true, states(id)) |
|
109 |
else (false, null) |
|
110 |
} |
|
34453 | 111 |
|
34509 | 112 |
if (result.kind == IsabelleProcess.Kind.STDOUT || result.kind == IsabelleProcess.Kind.STDIN) |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
113 |
output_info.event(result.toString) |
34509 | 114 |
else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) { // FIXME !? |
34453 | 115 |
initialized = true |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
116 |
Swing.now { this ! ProverEvents.Activate } |
34453 | 117 |
} |
118 |
else { |
|
34509 | 119 |
result.kind match { |
120 |
||
121 |
case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
122 |
| IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR => |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
123 |
if (command != null) { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
124 |
if (result.kind == IsabelleProcess.Kind.ERROR) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
125 |
command.status = Command.Status.FAILED |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
126 |
command.add_result(running, process.parse_message(result)) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
127 |
command_change(command) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
128 |
} else { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
129 |
output_info.event(result.toString) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
130 |
} |
34404
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34401
diff
changeset
|
131 |
|
34509 | 132 |
case IsabelleProcess.Kind.STATUS => |
133 |
//{{{ handle all kinds of status messages here |
|
134 |
process.parse_message(result) match { |
|
135 |
case XML.Elem(Markup.MESSAGE, _, elems) => |
|
136 |
for (elem <- elems) { |
|
137 |
elem match { |
|
138 |
//{{{ |
|
139 |
// command and keyword declarations |
|
140 |
case XML.Elem(Markup.COMMAND_DECL, |
|
141 |
(Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => |
|
142 |
command_decls += (name -> kind) |
|
143 |
case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => |
|
144 |
keyword_decls += name |
|
34404
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34401
diff
changeset
|
145 |
|
34509 | 146 |
// document edits |
147 |
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) |
|
148 |
if document_versions.contains(doc_id) => |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
149 |
output_info.event(result.toString) |
34509 | 150 |
for { |
151 |
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) |
|
152 |
<- edits |
|
153 |
} { |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
154 |
if (commands.contains(cmd_id)) { |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
155 |
val cmd = commands(cmd_id) |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
156 |
if (cmd.state_id != null) states -= cmd.state_id |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
157 |
states(cmd_id) = cmd |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
158 |
cmd.state_id = state_id |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
159 |
cmd.status = Command.Status.UNPROCESSED |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
160 |
command_change(cmd) |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
161 |
} |
34453 | 162 |
|
34509 | 163 |
} |
164 |
// command status |
|
165 |
case XML.Elem(Markup.UNPROCESSED, _, _) |
|
166 |
if command != null => |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
167 |
output_info.event(result.toString) |
34509 | 168 |
command.status = Command.Status.UNPROCESSED |
169 |
command_change(command) |
|
170 |
case XML.Elem(Markup.FINISHED, _, _) |
|
171 |
if command != null => |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
172 |
output_info.event(result.toString) |
34509 | 173 |
command.status = Command.Status.FINISHED |
174 |
command_change(command) |
|
175 |
case XML.Elem(Markup.FAILED, _, _) |
|
176 |
if command != null => |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
177 |
output_info.event(result.toString) |
34509 | 178 |
command.status = Command.Status.FAILED |
179 |
command_change(command) |
|
34453 | 180 |
|
34509 | 181 |
// other markup |
182 |
case XML.Elem(kind, |
|
183 |
(Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) :: |
|
184 |
(Markup.ID, markup_id) :: _, _) => |
|
185 |
val begin = offset.toInt - 1 |
|
186 |
val end = end_offset.toInt - 1 |
|
187 |
||
188 |
val cmd = // FIXME proper command version!? running!? |
|
189 |
// outer syntax: no id in props |
|
190 |
if (command == null) commands.getOrElse(markup_id, null) |
|
191 |
// inner syntax: id from props |
|
192 |
else command |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
193 |
if (cmd != null) { |
34509 | 194 |
cmd.root_node.insert(cmd.node_from(kind, begin, end)) |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
195 |
command_change(cmd) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
196 |
} |
34509 | 197 |
case _ => |
198 |
//}}} |
|
34453 | 199 |
} |
34509 | 200 |
} |
201 |
case _ => |
|
202 |
} |
|
203 |
//}}} |
|
34453 | 204 |
|
34509 | 205 |
case _ => |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
206 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
207 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
208 |
} |
34453 | 209 |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
210 |
def act() { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
211 |
import ProverEvents._ |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
212 |
loop { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
213 |
react { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
214 |
case Activate => { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
215 |
val (doc, structure_change) = document.activate |
34539 | 216 |
val old_id = document_id |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
217 |
val doc_id = Isabelle.plugin.id() |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
218 |
document_versions ::= (doc_id, doc) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
219 |
edit_document(old_id, doc_id, structure_change) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
220 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
221 |
case SetIsCommandKeyword(f) => { |
34539 | 222 |
val old_id = document_id |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
223 |
val doc_id = Isabelle.plugin.id() |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
224 |
document_versions ::= (doc_id, document.set_command_keyword(f)) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
225 |
edit_document(old_id, doc_id, StructureChange(None, Nil, Nil)) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
226 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
227 |
case change: Text.Change => { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
228 |
val (doc, structure_change) = document.text_changed(change) |
34539 | 229 |
val old_id = document_id |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
230 |
val doc_id = Isabelle.plugin.id() |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
231 |
document_versions ::= (doc_id, doc) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
232 |
edit_document(old_id, doc_id, structure_change) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
233 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
234 |
case command: Command => { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
235 |
//state of command has changed |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
236 |
change_receiver ! command |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
237 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
238 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
239 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
240 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
241 |
|
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
242 |
def set_document(change_receiver: Actor, path: String) { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
243 |
this.change_receiver = change_receiver |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
244 |
this ! ProverEvents.SetIsCommandKeyword(command_decls.contains) |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
245 |
process.ML("()") // FIXME force initial writeln |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
246 |
process.begin_document(document_id0, path) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
247 |
} |
34453 | 248 |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
249 |
private def edit_document(old_id: String, document_id: String, changes: StructureChange) = Swing.now |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
250 |
{ |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
251 |
val removes = |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
252 |
for (cmd <- changes.removed_commands) yield { |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
253 |
commands -= cmd.id |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
254 |
if (cmd.state_id != null) states -= cmd.state_id |
34539 | 255 |
(document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> None |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
256 |
} |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
257 |
val inserts = |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
258 |
for (cmd <- changes.added_commands) yield { |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
259 |
commands += (cmd.id -> cmd) |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
260 |
process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content)) |
34539 | 261 |
(document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> Some(cmd.id) |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
262 |
} |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
263 |
process.edit_document(old_id, document_id, removes.reverse ++ inserts) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
264 |
} |
34453 | 265 |
} |