author | wenzelm |
Sat, 05 Sep 2009 00:35:37 +0200 | |
changeset 34707 | cc5d388fcbf2 |
parent 34703 | ff037c17332a |
child 34709 | 2f0c18f9b6c7 |
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} |
34703 | 14 |
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
|
15 |
|
34456 | 16 |
import org.gjt.sp.util.Log |
34671 | 17 |
import javax.swing.JTextArea |
34456 | 18 |
|
34501 | 19 |
import isabelle.jedit.Isabelle |
34660 | 20 |
import isabelle.proofdocument.{ProofDocument, Change, Token} |
34690 | 21 |
import isabelle.Isar_Document |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
22 |
|
34703 | 23 |
|
24 |
object ProverEvents |
|
25 |
{ |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
26 |
case class Activate |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
27 |
} |
34453 | 28 |
|
34703 | 29 |
|
34672 | 30 |
class Prover(isabelle_system: Isabelle_System, logic: String, change_receiver: Actor) |
34692
3c0a8bece8b8
Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end;
wenzelm
parents:
34690
diff
changeset
|
31 |
extends Actor |
34453 | 32 |
{ |
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
33 |
/* prover process */ |
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 |
{ |
34692
3c0a8bece8b8
Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end;
wenzelm
parents:
34690
diff
changeset
|
37 |
val receiver = new Actor { |
3c0a8bece8b8
Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end;
wenzelm
parents:
34690
diff
changeset
|
38 |
def act() = { |
3c0a8bece8b8
Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end;
wenzelm
parents:
34690
diff
changeset
|
39 |
loop { react { case res: Isabelle_Process.Result => handle_result(res) } } |
3c0a8bece8b8
Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end;
wenzelm
parents:
34690
diff
changeset
|
40 |
} |
3c0a8bece8b8
Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end;
wenzelm
parents:
34690
diff
changeset
|
41 |
}.start |
3c0a8bece8b8
Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end;
wenzelm
parents:
34690
diff
changeset
|
42 |
new Isabelle_Process(isabelle_system, receiver, "-m", "xsymbols", logic) with Isar_Document |
34504
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 |
|
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
45 |
def stop() { process.kill } |
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
46 |
|
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
47 |
|
34509 | 48 |
/* document state information */ |
49 |
||
34690 | 50 |
private val states = new mutable.HashMap[Isar_Document.State_ID, Command_State] with |
51 |
mutable.SynchronizedMap[Isar_Document.State_ID, Command_State] |
|
52 |
private val commands = new mutable.HashMap[Isar_Document.Command_ID, Command] with |
|
53 |
mutable.SynchronizedMap[Isar_Document.Command_ID, Command] |
|
34654 | 54 |
val document_0 = |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
55 |
ProofDocument.empty. |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
56 |
set_command_keyword(command_decls.contains). |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
57 |
set_change_receiver(change_receiver) |
34650 | 58 |
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
|
59 |
|
34690 | 60 |
def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id) |
61 |
def document(id: Isar_Document.Document_ID) = document_versions.find(_.id == id) |
|
34509 | 62 |
|
63 |
private var initialized = false |
|
64 |
||
65 |
||
34485 | 66 |
/* outer syntax keywords */ |
67 |
||
34465
ccadbf63e320
added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents:
34462
diff
changeset
|
68 |
val decl_info = new EventBus[(String, String)] |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
69 |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
70 |
private val keyword_decls = |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
71 |
new mutable.HashSet[String] with mutable.SynchronizedSet[String] { |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
72 |
override def +=(name: String) = { |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
73 |
decl_info.event(name, OuterKeyword.MINOR) |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
74 |
super.+=(name) |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
75 |
} |
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
76 |
} |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
77 |
private val command_decls = |
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34509
diff
changeset
|
78 |
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
|
79 |
override def +=(entry: (String, String)) = { |
1dac47492863
decl_info: cover both commands and keywords, with kind;
wenzelm
parents:
34466
diff
changeset
|
80 |
decl_info.event(entry) |
1dac47492863
decl_info: cover both commands and keywords, with kind;
wenzelm
parents:
34466
diff
changeset
|
81 |
super.+=(entry) |
34465
ccadbf63e320
added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents:
34462
diff
changeset
|
82 |
} |
ccadbf63e320
added EventBus for new command- or keyword-declarations
immler@in.tum.de
parents:
34462
diff
changeset
|
83 |
} |
34485 | 84 |
|
85 |
||
34611 | 86 |
/* completions */ |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
87 |
|
34612
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
88 |
private var _completion = Isabelle.completion |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
89 |
def completion = _completion |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
90 |
decl_info += (p => _completion += p._1) |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
91 |
|
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 |
/* event handling */ |
34673
1a30c075c202
change_receiver and output_info are used before regular initialisation
immler@in.tum.de
parents:
34672
diff
changeset
|
94 |
lazy val output_info = new EventBus[Isabelle_Process.Result] |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
95 |
|
34671 | 96 |
val output_text_view = new JTextArea |
97 |
output_info += (result => output_text_view.append(result.toString + "\n")) |
|
98 |
||
34615 | 99 |
private def handle_result(result: Isabelle_Process.Result) |
34489
7b7ccf0ff629
replaced java.util.Property by plain association list;
wenzelm
parents:
34485
diff
changeset
|
100 |
{ |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
101 |
val state = |
34509 | 102 |
result.props.find(p => p._1 == Markup.ID) match { |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
103 |
case None => None |
34509 | 104 |
case Some((_, id)) => |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
105 |
if (commands.contains(id)) Some(commands(id)) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
106 |
else if (states.contains(id)) Some(states(id)) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
107 |
else None |
34509 | 108 |
} |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
109 |
output_info.event(result) |
34692
3c0a8bece8b8
Isabelle_Process: receiver as Actor -- requires Scheduler.shutdown in the end;
wenzelm
parents:
34690
diff
changeset
|
110 |
val message = Isabelle_Process.parse_message(isabelle_system, result) |
34677 | 111 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
112 |
if (state.isDefined) state.get ! message |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
113 |
else result.kind match { |
34404
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34401
diff
changeset
|
114 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
115 |
case Isabelle_Process.Kind.STATUS => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
116 |
//{{{ handle all kinds of status messages here |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
117 |
message match { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
118 |
case XML.Elem(Markup.MESSAGE, _, elems) => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
119 |
for (elem <- elems) { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
120 |
elem match { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
121 |
//{{{ |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
122 |
// command and keyword declarations |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
123 |
case XML.Elem(Markup.COMMAND_DECL, |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
124 |
(Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
125 |
command_decls += (name -> kind) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
126 |
case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
127 |
keyword_decls += name |
34404
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34401
diff
changeset
|
128 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
129 |
// process ready (after initialization) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
130 |
case XML.Elem(Markup.READY, _, _) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
131 |
if !initialized => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
132 |
initialized = true |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
133 |
change_receiver ! ProverEvents.Activate |
34453 | 134 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
135 |
// document edits |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
136 |
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
137 |
if document_versions.exists(_.id == doc_id) => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
138 |
val doc = document_versions.find(_.id == doc_id).get |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
139 |
for { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
140 |
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
141 |
<- edits |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
142 |
} { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
143 |
if (commands.contains(cmd_id)) { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
144 |
val cmd = commands(cmd_id) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
145 |
val state = new Command_State(cmd) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
146 |
states(state_id) = state |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
147 |
doc.states += (cmd -> state) |
34685
93f4978fe2a8
global event buses for changes concerning commands and document edits
immler@in.tum.de
parents:
34677
diff
changeset
|
148 |
cmd.changed() |
34509 | 149 |
} |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
150 |
|
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
151 |
} |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
152 |
case XML.Elem(kind, attr, body) => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
153 |
// TODO: This is mostly irrelevant information on removed commands, but it can |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
154 |
// also be outer-syntax-markup since there is no id in props (fix that?) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
155 |
val (begin, end) = Position.offsets_of(attr) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
156 |
val markup_id = Position.id_of(attr) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
157 |
val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
158 |
if (outer && begin.isDefined && end.isDefined && markup_id.isDefined) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
159 |
commands.get(markup_id.get).map (cmd => cmd ! message) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
160 |
case _ => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
161 |
//}}} |
34509 | 162 |
} |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
163 |
} |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
164 |
case _ => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
165 |
} |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
166 |
//}}} |
34453 | 167 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34674
diff
changeset
|
168 |
case _ => |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
169 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
170 |
} |
34453 | 171 |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
172 |
def act() { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
173 |
import ProverEvents._ |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
174 |
loop { |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
175 |
react { |
34660 | 176 |
case change: Change => { |
177 |
val old = document(change.parent.get.id).get |
|
34544
56217d219e27
proofdocument-versions get id from changes
immler@in.tum.de
parents:
34540
diff
changeset
|
178 |
val (doc, structure_change) = old.text_changed(change) |
56217d219e27
proofdocument-versions get id from changes
immler@in.tum.de
parents:
34540
diff
changeset
|
179 |
document_versions ::= doc |
34650 | 180 |
edit_document(old, doc, structure_change) |
34685
93f4978fe2a8
global event buses for changes concerning commands and document edits
immler@in.tum.de
parents:
34677
diff
changeset
|
181 |
change_receiver ! doc |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
182 |
} |
34650 | 183 |
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
|
184 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
185 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
186 |
} |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
187 |
|
34672 | 188 |
def set_document(path: String) { |
34650 | 189 |
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
|
190 |
} |
34453 | 191 |
|
34660 | 192 |
private def edit_document(old: ProofDocument, doc: ProofDocument, |
193 |
changes: ProofDocument.StructureChange) = { |
|
194 |
val id_changes = changes map {case (c1, c2) => |
|
195 |
(c1.map(_.id).getOrElse(document_0.id), |
|
196 |
c2 match { |
|
197 |
case None => None |
|
198 |
case Some(cmd) => |
|
199 |
commands += (cmd.id -> cmd) |
|
200 |
process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content)) |
|
201 |
Some(cmd.id) |
|
202 |
}) |
|
203 |
} |
|
204 |
process.edit_document(old.id, doc.id, id_changes) |
|
34650 | 205 |
} |
34453 | 206 |
} |