lib/classes/isabelle/IsabelleDemo.java
author wenzelm
Sat, 15 Dec 2007 23:54:10 +0100
changeset 25657 9f7796a02b28
parent 25656 7f4cf5b20d38
child 25660 097f1384e371
permissions -rw-r--r--
tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25648
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
     1
/*
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
     2
 * $Id$
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
     3
 *
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
     4
 * Simple demo for IsabelleProcess wrapper.
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
     5
 *
25655
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
     6
 * Example session with Beanshell:
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
     7
 *
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
     8
 *    $ cd [ISABELLE_HOME]/lib/classes
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
     9
 *    $ javac isabelle/*.java
25657
9f7796a02b28 tuned comments;
wenzelm
parents: 25656
diff changeset
    10
 *
25655
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
    11
 *    $ bsh
25657
9f7796a02b28 tuned comments;
wenzelm
parents: 25656
diff changeset
    12
 * or
9f7796a02b28 tuned comments;
wenzelm
parents: 25656
diff changeset
    13
 *    $ java -Disabelle.home=[ISABELLE_HOME] -jar bsh.jar
25656
7f4cf5b20d38 addClassPath;
wenzelm
parents: 25655
diff changeset
    14
 *    % addClassPath(".");
25657
9f7796a02b28 tuned comments;
wenzelm
parents: 25656
diff changeset
    15
 *
25655
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
    16
 *    % import isabelle.*;
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
    17
 *    % isabelle = new IsabelleDemo("HOL");
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
    18
 *    % isabelle.command("theory Test imports Main begin");
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
    19
 *    % isabelle.command("lemma \"A --> A\"");
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
    20
 *    % isabelle.command("..");
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
    21
 *    % isabelle.command("end");
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
    22
 *    % isabelle.close();
e55626a33a8e added example session with Beanshell;
wenzelm
parents: 25653
diff changeset
    23
 *
25648
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
    24
 */
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
    25
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
    26
package isabelle;
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
    27
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
    28
public class IsabelleDemo extends IsabelleProcess {
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
    29
    public IsabelleDemo(String logic) throws IsabelleProcessException
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
    30
    {
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
    31
        super(logic);
25653
wenzelm
parents: 25648
diff changeset
    32
        new Thread (new Runnable () {
wenzelm
parents: 25648
diff changeset
    33
            public void run()
wenzelm
parents: 25648
diff changeset
    34
            {
wenzelm
parents: 25648
diff changeset
    35
                IsabelleProcess.Result result = null;
wenzelm
parents: 25648
diff changeset
    36
                while (result == null || result.kind != IsabelleProcess.Result.Kind.EXIT) {
wenzelm
parents: 25648
diff changeset
    37
                    try {
wenzelm
parents: 25648
diff changeset
    38
                        result = results.take();
wenzelm
parents: 25648
diff changeset
    39
                        System.err.println(result.toString());
wenzelm
parents: 25648
diff changeset
    40
                    } catch (InterruptedException ex) { }
wenzelm
parents: 25648
diff changeset
    41
                }
wenzelm
parents: 25648
diff changeset
    42
                System.err.println("Console thread terminated");
wenzelm
parents: 25648
diff changeset
    43
            }
wenzelm
parents: 25648
diff changeset
    44
        }).start();
25648
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
    45
    }
d2730020af90 reorganized demo;
wenzelm
parents:
diff changeset
    46
}