author | wenzelm |
Mon, 29 Dec 2008 21:01:55 +0100 | |
changeset 34458 | e2aa32bb73c0 |
parent 34456 | 14367c0715e8 |
child 34459 | b08299e7bbe6 |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
2 |
* Higher-level prover communication |
|
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 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
12 |
import java.util.Properties |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
13 |
|
34453 | 14 |
import scala.collection.mutable.{HashMap, HashSet} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
15 |
|
34456 | 16 |
import org.gjt.sp.util.Log |
17 |
||
34443
f2e13329cc49
dynamic instances Isabelle.system, Isabelle.symbols;
wenzelm
parents:
34410
diff
changeset
|
18 |
import isabelle.proofdocument.{ProofDocument, Text, Token} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
19 |
|
34453 | 20 |
|
21 |
class Prover(isabelle_system: IsabelleSystem, isabelle_symbols: Symbol.Interpretation) |
|
22 |
{ |
|
23 |
private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC") |
|
24 |
private var process: Isar = null |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
25 |
private var commands = new HashMap[String, Command] |
34453 | 26 |
|
34399
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34397
diff
changeset
|
27 |
val command_decls = new HashSet[String] |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34397
diff
changeset
|
28 |
val keyword_decls = new HashSet[String] |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
29 |
private var initialized = false |
34453 | 30 |
|
34456 | 31 |
val activated = new EventBus[Unit] |
32 |
val command_info = new EventBus[Command] |
|
33 |
val output_info = new EventBus[String] |
|
34453 | 34 |
var document: Document = null |
34399
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34397
diff
changeset
|
35 |
|
34444
a245f6cc3105
replaced inUIThread by scala-style swing/swing_async combinators;
wenzelm
parents:
34443
diff
changeset
|
36 |
|
34456 | 37 |
def command_change(c: Command) = Swing.now { command_info.event(c) } |
34399
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34397
diff
changeset
|
38 |
|
34453 | 39 |
private def handle_result(r: IsabelleProcess.Result) = { |
40 |
val id = if (r.props != null) r.props.getProperty(Markup.ID) else null |
|
41 |
val st = if (id != null) commands.getOrElse(id, null) else null |
|
42 |
||
43 |
if (r.kind == IsabelleProcess.Kind.STDOUT || r.kind == IsabelleProcess.Kind.STDIN) |
|
34456 | 44 |
Swing.now { output_info.event(r.result) } |
34453 | 45 |
else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) { |
46 |
initialized = true |
|
34456 | 47 |
Swing.now { |
34453 | 48 |
if (document != null) { |
49 |
document.activate() |
|
34456 | 50 |
activated.event(()) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
51 |
} |
34453 | 52 |
} |
53 |
} |
|
54 |
else { |
|
55 |
val tree = YXML.parse_failsafe(isabelle_symbols.decode(r.result)) |
|
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34456
diff
changeset
|
56 |
if (st == null || (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)) { |
34453 | 57 |
r.kind match { |
34404
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34401
diff
changeset
|
58 |
|
34453 | 59 |
case IsabelleProcess.Kind.STATUS => |
60 |
//{{{ handle all kinds of status messages here |
|
61 |
tree match { |
|
62 |
case XML.Elem(Markup.MESSAGE, _, elems) => |
|
63 |
for (elem <- elems) { |
|
64 |
elem match { |
|
65 |
//{{{ |
|
66 |
// command status |
|
67 |
case XML.Elem(Markup.FINISHED, _, _) => |
|
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34456
diff
changeset
|
68 |
st.status = Command.Status.FINISHED |
34456 | 69 |
command_change(st) |
34453 | 70 |
case XML.Elem(Markup.UNPROCESSED, _, _) => |
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34456
diff
changeset
|
71 |
st.status = Command.Status.UNPROCESSED |
34456 | 72 |
command_change(st) |
34453 | 73 |
case XML.Elem(Markup.FAILED, _, _) => |
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34456
diff
changeset
|
74 |
st.status = Command.Status.FAILED |
34456 | 75 |
command_change(st) |
34453 | 76 |
case XML.Elem(Markup.DISPOSED, _, _) => |
77 |
document.prover.commands.removeKey(st.id) |
|
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34456
diff
changeset
|
78 |
st.status = Command.Status.REMOVED |
34456 | 79 |
command_change(st) |
34399
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34397
diff
changeset
|
80 |
|
34453 | 81 |
// command and keyword declarations |
34456 | 82 |
case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: _, _) => |
83 |
command_decls += name |
|
84 |
case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => |
|
85 |
keyword_decls += name |
|
34404
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34401
diff
changeset
|
86 |
|
34453 | 87 |
// other markup |
88 |
case XML.Elem(kind, |
|
89 |
(Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) :: |
|
90 |
(Markup.ID, markup_id) :: _, _) => |
|
91 |
val begin = Int.unbox(java.lang.Integer.valueOf(offset)) - 1 |
|
92 |
val end = Int.unbox(java.lang.Integer.valueOf(end_offset)) - 1 |
|
93 |
||
94 |
val command = |
|
95 |
// outer syntax: no id in props |
|
96 |
if (st == null) commands.getOrElse(markup_id, null) |
|
97 |
// inner syntax: id from props |
|
98 |
else st |
|
99 |
command.root_node.insert(command.node_from(kind, begin, end)) |
|
100 |
||
101 |
case _ => |
|
102 |
//}}} |
|
103 |
} |
|
104 |
} |
|
105 |
case _ => |
|
106 |
} |
|
107 |
//}}} |
|
108 |
||
109 |
case IsabelleProcess.Kind.ERROR if st != null => |
|
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34456
diff
changeset
|
110 |
if (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE) |
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34456
diff
changeset
|
111 |
st.status = Command.Status.FAILED |
34453 | 112 |
st.add_result(tree) |
34456 | 113 |
command_change(st) |
34453 | 114 |
|
115 |
case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY |
|
116 |
| IsabelleProcess.Kind.WARNING if st != null => |
|
117 |
st.add_result(tree) |
|
34456 | 118 |
command_change(st) |
34453 | 119 |
|
120 |
case _ => |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
121 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
122 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
123 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
124 |
} |
34453 | 125 |
|
34370 | 126 |
|
34453 | 127 |
def start(logic: String) { |
128 |
if (logic != null) _logic = logic |
|
34456 | 129 |
|
130 |
val results = new EventBus[IsabelleProcess.Result] |
|
131 |
results += handle_result |
|
132 |
results.logger = Log.log(Log.ERROR, null, _) |
|
133 |
||
34453 | 134 |
process = new Isar(isabelle_system, results, "-m", "xsymbols", _logic) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
135 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
136 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
137 |
def stop() { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
138 |
process.kill |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
139 |
} |
34453 | 140 |
|
34456 | 141 |
def set_document(text: Text, path: String) { |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
142 |
this.document = new Document(text, this) |
34453 | 143 |
process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path)) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
144 |
|
34456 | 145 |
document.structural_changes += (changes => { |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
146 |
for (cmd <- changes.removedCommands) remove(cmd) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
147 |
for (cmd <- changes.addedCommands) send(cmd) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
148 |
}) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
149 |
if (initialized) { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
150 |
document.activate() |
34456 | 151 |
activated.event(()) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
152 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
153 |
} |
34453 | 154 |
|
155 |
private def send(cmd: Command) { |
|
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34456
diff
changeset
|
156 |
cmd.status = Command.Status.UNPROCESSED |
34451 | 157 |
commands.put(cmd.id, cmd) |
34453 | 158 |
|
34451 | 159 |
val props = new Properties |
34453 | 160 |
props.setProperty(Markup.ID, cmd.id) |
161 |
props.setProperty(Markup.OFFSET, "1") |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
162 |
|
34443
f2e13329cc49
dynamic instances Isabelle.system, Isabelle.symbols;
wenzelm
parents:
34410
diff
changeset
|
163 |
val content = isabelle_symbols.encode(document.getContent(cmd)) |
34453 | 164 |
process.create_command(props, content) |
165 |
process.insert_command(if (cmd.previous == null) "" else cmd.previous.id, cmd.id) |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
166 |
} |
34453 | 167 |
|
168 |
def remove(cmd: Command) { |
|
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34456
diff
changeset
|
169 |
cmd.status = Command.Status.REMOVE |
34453 | 170 |
process.remove_command(cmd.id) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
171 |
} |
34453 | 172 |
} |