25648
|
1 |
/*
|
|
2 |
* $Id$
|
|
3 |
*
|
|
4 |
* Simple demo for IsabelleProcess wrapper.
|
|
5 |
*
|
25655
|
6 |
* Example session with Beanshell:
|
|
7 |
*
|
|
8 |
* $ cd [ISABELLE_HOME]/lib/classes
|
|
9 |
* $ javac isabelle/*.java
|
25657
|
10 |
*
|
25655
|
11 |
* $ bsh
|
25657
|
12 |
* or
|
|
13 |
* $ java -Disabelle.home=[ISABELLE_HOME] -jar bsh.jar
|
25656
|
14 |
* % addClassPath(".");
|
25657
|
15 |
*
|
25655
|
16 |
* % import isabelle.*;
|
|
17 |
* % isabelle = new IsabelleDemo("HOL");
|
|
18 |
* % isabelle.command("theory Test imports Main begin");
|
|
19 |
* % isabelle.command("lemma \"A --> A\"");
|
|
20 |
* % isabelle.command("..");
|
|
21 |
* % isabelle.command("end");
|
|
22 |
* % isabelle.close();
|
|
23 |
*
|
25648
|
24 |
*/
|
|
25 |
|
|
26 |
package isabelle;
|
|
27 |
|
|
28 |
public class IsabelleDemo extends IsabelleProcess {
|
|
29 |
public IsabelleDemo(String logic) throws IsabelleProcessException
|
|
30 |
{
|
|
31 |
super(logic);
|
25653
|
32 |
new Thread (new Runnable () {
|
|
33 |
public void run()
|
|
34 |
{
|
|
35 |
IsabelleProcess.Result result = null;
|
|
36 |
while (result == null || result.kind != IsabelleProcess.Result.Kind.EXIT) {
|
|
37 |
try {
|
|
38 |
result = results.take();
|
|
39 |
System.err.println(result.toString());
|
|
40 |
} catch (InterruptedException ex) { }
|
|
41 |
}
|
|
42 |
System.err.println("Console thread terminated");
|
|
43 |
}
|
|
44 |
}).start();
|
25648
|
45 |
}
|
|
46 |
}
|