author | immler@in.tum.de |
Mon, 13 Jul 2009 14:30:39 +0200 | |
changeset 34654 | 30f588245884 |
parent 34653 | 2e033aaf128e |
child 34660 | e0561943bfc9 |
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 |
} |
34453 | 27 |
|
34615 | 28 |
class Prover(isabelle_system: Isabelle_System, logic: String) extends Actor |
34453 | 29 |
{ |
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
30 |
/* prover process */ |
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
31 |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
32 |
private val process = |
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
33 |
{ |
34615 | 34 |
val results = new EventBus[Isabelle_Process.Result] + handle_result |
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
35 |
results.logger = Log.log(Log.ERROR, null, _) |
34615 | 36 |
new Isabelle_Process(isabelle_system, results, "-m", "xsymbols", logic) with IsarDocument |
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
37 |
} |
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
38 |
|
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
39 |
def stop() { process.kill } |
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 |
|
34509 | 42 |
/* document state information */ |
43 |
||
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
44 |
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
|
45 |
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
|
46 |
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
|
47 |
mutable.SynchronizedMap[IsarDocument.Command_ID, Command] |
34654 | 48 |
val document_0 = |
34650 | 49 |
ProofDocument.empty.set_command_keyword(command_decls.contains) |
50 |
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
|
51 |
|
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
34564
diff
changeset
|
52 |
def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id) |
34654 | 53 |
def document(id: IsarDocument.Document_ID) = document_versions.find(_.id == id) |
34509 | 54 |
|
55 |
private var initialized = false |
|
56 |
||
57 |
||
34485 | 58 |
/* outer syntax keywords */ |
59 |
||
34465
ccadbf63e320
added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents:
34462
diff
changeset
|
60 |
val decl_info = new EventBus[(String, String)] |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
61 |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
62 |
private val keyword_decls = |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
63 |
new mutable.HashSet[String] with mutable.SynchronizedSet[String] { |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
64 |
override def +=(name: String) = { |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
65 |
decl_info.event(name, OuterKeyword.MINOR) |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
66 |
super.+=(name) |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
67 |
} |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
68 |
} |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
69 |
private val command_decls = |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
70 |
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
|
71 |
override def +=(entry: (String, String)) = { |
1dac47492863
decl_info: cover both commands and keywords, with kind;
wenzelm
parents:
34466
diff
changeset
|
72 |
decl_info.event(entry) |
1dac47492863
decl_info: cover both commands and keywords, with kind;
wenzelm
parents:
34466
diff
changeset
|
73 |
super.+=(entry) |
34465
ccadbf63e320
added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents:
34462
diff
changeset
|
74 |
} |
ccadbf63e320
added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents:
34462
diff
changeset
|
75 |
} |
34485 | 76 |
|
77 |
||
34611 | 78 |
/* completions */ |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
79 |
|
34612
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
80 |
private var _completion = Isabelle.completion |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
81 |
def completion = _completion |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
82 |
decl_info += (p => _completion += p._1) |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
83 |
|
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
84 |
|
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
85 |
/* event handling */ |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
86 |
|
34456 | 87 |
val output_info = new EventBus[String] |
34582 | 88 |
var change_receiver: Actor = null |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
89 |
|
34615 | 90 |
private def handle_result(result: Isabelle_Process.Result) |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
91 |
{ |
34650 | 92 |
def command_change(c: Command) = change_receiver ! c |
34653 | 93 |
val (state, command) = |
34509 | 94 |
result.props.find(p => p._1 == Markup.ID) match { |
34653 | 95 |
case None => (null, null) |
34509 | 96 |
case Some((_, id)) => |
34653 | 97 |
if (commands.contains(id)) (null, commands(id)) |
98 |
else if (states.contains(id)) (id, states(id)) |
|
99 |
else (null, null) |
|
34509 | 100 |
} |
34453 | 101 |
|
34615 | 102 |
if (result.kind == Isabelle_Process.Kind.STDOUT || |
103 |
result.kind == Isabelle_Process.Kind.STDIN) |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
104 |
output_info.event(result.toString) |
34453 | 105 |
else { |
34509 | 106 |
result.kind match { |
107 |
||
34615 | 108 |
case Isabelle_Process.Kind.WRITELN |
109 |
| Isabelle_Process.Kind.PRIORITY |
|
110 |
| Isabelle_Process.Kind.WARNING |
|
111 |
| Isabelle_Process.Kind.ERROR => |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
112 |
if (command != null) { |
34615 | 113 |
if (result.kind == Isabelle_Process.Kind.ERROR) |
34653 | 114 |
command.set_status(state, Command.Status.FAILED) |
115 |
command.add_result(state, process.parse_message(result)) |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
116 |
command_change(command) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
117 |
} else { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
118 |
output_info.event(result.toString) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
119 |
} |
34404
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34401
diff
changeset
|
120 |
|
34615 | 121 |
case Isabelle_Process.Kind.STATUS => |
34509 | 122 |
//{{{ handle all kinds of status messages here |
123 |
process.parse_message(result) match { |
|
124 |
case XML.Elem(Markup.MESSAGE, _, elems) => |
|
125 |
for (elem <- elems) { |
|
126 |
elem match { |
|
127 |
//{{{ |
|
128 |
// command and keyword declarations |
|
129 |
case XML.Elem(Markup.COMMAND_DECL, |
|
130 |
(Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => |
|
131 |
command_decls += (name -> kind) |
|
132 |
case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => |
|
133 |
keyword_decls += name |
|
34404
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34401
diff
changeset
|
134 |
|
34589
d461e5506d02
handle_result: activate via explicit status "ready" (cf. http://isabelle.in.tum.de/repos/isabelle/rev/ce169bd37fc0);
wenzelm
parents:
34582
diff
changeset
|
135 |
// process ready (after initialization) |
d461e5506d02
handle_result: activate via explicit status "ready" (cf. http://isabelle.in.tum.de/repos/isabelle/rev/ce169bd37fc0);
wenzelm
parents:
34582
diff
changeset
|
136 |
case XML.Elem(Markup.READY, _, _) |
d461e5506d02
handle_result: activate via explicit status "ready" (cf. http://isabelle.in.tum.de/repos/isabelle/rev/ce169bd37fc0);
wenzelm
parents:
34582
diff
changeset
|
137 |
if !initialized => |
d461e5506d02
handle_result: activate via explicit status "ready" (cf. http://isabelle.in.tum.de/repos/isabelle/rev/ce169bd37fc0);
wenzelm
parents:
34582
diff
changeset
|
138 |
initialized = true |
34649 | 139 |
change_receiver ! ProverEvents.Activate |
34589
d461e5506d02
handle_result: activate via explicit status "ready" (cf. http://isabelle.in.tum.de/repos/isabelle/rev/ce169bd37fc0);
wenzelm
parents:
34582
diff
changeset
|
140 |
|
34509 | 141 |
// document edits |
142 |
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) |
|
34582 | 143 |
if document_versions.exists(_.id == doc_id) => |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
144 |
output_info.event(result.toString) |
34653 | 145 |
val doc = document_versions.find(_.id == doc_id).get |
34509 | 146 |
for { |
147 |
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) |
|
148 |
<- edits |
|
149 |
} { |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
150 |
if (commands.contains(cmd_id)) { |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
151 |
val cmd = commands(cmd_id) |
34540 | 152 |
states(state_id) = cmd |
34653 | 153 |
doc.states += (cmd -> state_id) |
154 |
cmd.states += (state_id -> new Command_State(cmd)) |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
155 |
command_change(cmd) |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
156 |
} |
34453 | 157 |
|
34509 | 158 |
} |
159 |
// command status |
|
160 |
case XML.Elem(Markup.UNPROCESSED, _, _) |
|
161 |
if command != null => |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
162 |
output_info.event(result.toString) |
34653 | 163 |
command.set_status(state, Command.Status.UNPROCESSED) |
34509 | 164 |
command_change(command) |
165 |
case XML.Elem(Markup.FINISHED, _, _) |
|
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) |
34653 | 168 |
command.set_status(state, Command.Status.FINISHED) |
34509 | 169 |
command_change(command) |
170 |
case XML.Elem(Markup.FAILED, _, _) |
|
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) |
34653 | 173 |
command.set_status(state, Command.Status.FAILED) |
34509 | 174 |
command_change(command) |
34570
c3bdaea2dd6a
improved handling of markup-information with command=null
immler@in.tum.de
parents:
34568
diff
changeset
|
175 |
case XML.Elem(kind, attr, body) |
c3bdaea2dd6a
improved handling of markup-information with command=null
immler@in.tum.de
parents:
34568
diff
changeset
|
176 |
if command != null => |
34610 | 177 |
val (begin, end) = Position.offsets_of(attr) |
34576
b86c54be2fe0
check presence of begin, end in attributes
immler@in.tum.de
parents:
34570
diff
changeset
|
178 |
if (begin.isDefined && end.isDefined) { |
b86c54be2fe0
check presence of begin, end in attributes
immler@in.tum.de
parents:
34570
diff
changeset
|
179 |
if (kind == Markup.ML_TYPING) { |
b86c54be2fe0
check presence of begin, end in attributes
immler@in.tum.de
parents:
34570
diff
changeset
|
180 |
val info = body.first.asInstanceOf[XML.Text].content |
34653 | 181 |
command.add_markup(state, |
182 |
command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info))) |
|
34576
b86c54be2fe0
check presence of begin, end in attributes
immler@in.tum.de
parents:
34570
diff
changeset
|
183 |
} else if (kind == Markup.ML_REF) { |
b86c54be2fe0
check presence of begin, end in attributes
immler@in.tum.de
parents:
34570
diff
changeset
|
184 |
body match { |
b86c54be2fe0
check presence of begin, end in attributes
immler@in.tum.de
parents:
34570
diff
changeset
|
185 |
case List(XML.Elem(Markup.ML_DEF, attr, _)) => |
34653 | 186 |
command.add_markup(state, command.markup_node( |
34610 | 187 |
begin.get - 1, end.get - 1, |
188 |
RefInfo( |
|
189 |
Position.file_of(attr), |
|
190 |
Position.line_of(attr), |
|
191 |
Position.id_of(attr), |
|
34653 | 192 |
Position.offset_of(attr)))) |
34576
b86c54be2fe0
check presence of begin, end in attributes
immler@in.tum.de
parents:
34570
diff
changeset
|
193 |
case _ => |
b86c54be2fe0
check presence of begin, end in attributes
immler@in.tum.de
parents:
34570
diff
changeset
|
194 |
} |
b86c54be2fe0
check presence of begin, end in attributes
immler@in.tum.de
parents:
34570
diff
changeset
|
195 |
} else { |
34653 | 196 |
command.add_markup(state, |
197 |
command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind))) |
|
34570
c3bdaea2dd6a
improved handling of markup-information with command=null
immler@in.tum.de
parents:
34568
diff
changeset
|
198 |
} |
34557 | 199 |
} |
34555
7c001369956a
included information on ML status messages in Sidekick's status-window
immler@in.tum.de
parents:
34554
diff
changeset
|
200 |
command_change(command) |
34570
c3bdaea2dd6a
improved handling of markup-information with command=null
immler@in.tum.de
parents:
34568
diff
changeset
|
201 |
case XML.Elem(kind, attr, body) |
c3bdaea2dd6a
improved handling of markup-information with command=null
immler@in.tum.de
parents:
34568
diff
changeset
|
202 |
if command == null => |
c3bdaea2dd6a
improved handling of markup-information with command=null
immler@in.tum.de
parents:
34568
diff
changeset
|
203 |
// TODO: This is mostly irrelevant information on removed commands, but it can |
c3bdaea2dd6a
improved handling of markup-information with command=null
immler@in.tum.de
parents:
34568
diff
changeset
|
204 |
// also be outer-syntax-markup since there is no id in props (fix that?) |
34610 | 205 |
val (begin, end) = Position.offsets_of(attr) |
206 |
val markup_id = Position.id_of(attr) |
|
34579
f5c3ad245539
outer syntax could clash with status on removed commands
immler@in.tum.de
parents:
34578
diff
changeset
|
207 |
val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind) |
34653 | 208 |
if (outer && state == null && begin.isDefined && end.isDefined && markup_id.isDefined) |
34570
c3bdaea2dd6a
improved handling of markup-information with command=null
immler@in.tum.de
parents:
34568
diff
changeset
|
209 |
commands.get(markup_id.get).map (cmd => { |
34653 | 210 |
cmd.add_markup(state, |
211 |
cmd.markup_node(begin.get - 1, end.get - 1, OuterInfo(kind))) |
|
34570
c3bdaea2dd6a
improved handling of markup-information with command=null
immler@in.tum.de
parents:
34568
diff
changeset
|
212 |
command_change(cmd) |
c3bdaea2dd6a
improved handling of markup-information with command=null
immler@in.tum.de
parents:
34568
diff
changeset
|
213 |
}) |
34509 | 214 |
case _ => |
215 |
//}}} |
|
34453 | 216 |
} |
34509 | 217 |
} |
218 |
case _ => |
|
219 |
} |
|
220 |
//}}} |
|
34453 | 221 |
|
34509 | 222 |
case _ => |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
223 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
224 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
225 |
} |
34453 | 226 |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
227 |
def act() { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
228 |
import ProverEvents._ |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
229 |
loop { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
230 |
react { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
231 |
case change: Text.Change => { |
34654 | 232 |
val old = document(change.base.get.id).get |
34544
56217d219e27
proofdocument-versions get id from changes
immler@in.tum.de
parents:
34540
diff
changeset
|
233 |
val (doc, structure_change) = old.text_changed(change) |
56217d219e27
proofdocument-versions get id from changes
immler@in.tum.de
parents:
34540
diff
changeset
|
234 |
document_versions ::= doc |
34650 | 235 |
edit_document(old, doc, structure_change) |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
236 |
} |
34650 | 237 |
case x => System.err.println("warning: ignored " + x) |
34538
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 |
34650 | 244 |
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
|
245 |
} |
34453 | 246 |
|
34650 | 247 |
private def edit_document(old: ProofDocument, doc: ProofDocument, changes: StructureChange) = { |
248 |
val removes = |
|
249 |
for (cmd <- changes.removed_commands) yield { |
|
250 |
commands -= cmd.id |
|
251 |
changes.before_change.map(_.id).getOrElse(document_0.id) -> None |
|
252 |
} |
|
253 |
val inserts = |
|
254 |
for (cmd <- changes.added_commands) yield { |
|
255 |
commands += (cmd.id -> cmd) |
|
256 |
process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content)) |
|
257 |
(doc.commands.prev(cmd).map(_.id).getOrElse(document_0.id)) -> Some(cmd.id) |
|
258 |
} |
|
259 |
process.edit_document(old.id, doc.id, removes.reverse ++ inserts) |
|
260 |
} |
|
34453 | 261 |
} |