19 object IsabelleProcess { |
19 object IsabelleProcess { |
20 |
20 |
21 /* results */ |
21 /* results */ |
22 |
22 |
23 object Kind extends Enumeration { |
23 object Kind extends Enumeration { |
24 //{{{ values |
24 //{{{ values and codes |
|
25 // internal system notification |
|
26 val SYSTEM = Value("SYSTEM") |
25 // Posix channels/events |
27 // Posix channels/events |
26 val STDIN = Value("STDIN") |
28 val STDIN = Value("STDIN") |
27 val STDOUT = Value("STDOUT") |
29 val STDOUT = Value("STDOUT") |
28 val SIGNAL = Value("SIGNAL") |
30 val SIGNAL = Value("SIGNAL") |
29 val EXIT = Value("EXIT") |
31 val EXIT = Value("EXIT") |
30 // Isabelle messages |
32 // Isabelle messages |
|
33 val INIT = Value("INIT") |
|
34 val STATUS = Value("STATUS") |
31 val WRITELN = Value("WRITELN") |
35 val WRITELN = Value("WRITELN") |
32 val PRIORITY = Value("PRIORITY") |
36 val PRIORITY = Value("PRIORITY") |
33 val TRACING = Value("TRACING") |
37 val TRACING = Value("TRACING") |
34 val WARNING = Value("WARNING") |
38 val WARNING = Value("WARNING") |
35 val ERROR = Value("ERROR") |
39 val ERROR = Value("ERROR") |
36 val DEBUG = Value("DEBUG") |
40 val DEBUG = Value("DEBUG") |
37 val PROMPT = Value("PROMPT") |
41 val PROMPT = Value("PROMPT") |
38 val INIT = Value("INIT") |
42 // messages codes |
39 val STATUS = Value("STATUS") |
43 val code = Map( |
40 // internal system notification |
44 ('A' : Int) -> Kind.INIT, |
41 val SYSTEM = Value("SYSTEM") |
45 ('B' : Int) -> Kind.STATUS, |
|
46 ('C' : Int) -> Kind.WRITELN, |
|
47 ('D' : Int) -> Kind.PRIORITY, |
|
48 ('E' : Int) -> Kind.TRACING, |
|
49 ('F' : Int) -> Kind.WARNING, |
|
50 ('G' : Int) -> Kind.ERROR, |
|
51 ('H' : Int) -> Kind.DEBUG, |
|
52 ('I' : Int) -> Kind.PROMPT, |
|
53 ('0' : Int) -> Kind.SYSTEM, |
|
54 ('1' : Int) -> Kind.STDIN, |
|
55 ('2' : Int) -> Kind.STDOUT, |
|
56 ('3' : Int) -> Kind.SIGNAL, |
|
57 ('4' : Int) -> Kind.EXIT) |
42 //}}} |
58 //}}} |
43 def is_raw(kind: Value) = |
59 def is_raw(kind: Value) = |
44 kind == STDOUT |
60 kind == STDOUT |
45 def is_control(kind: Value) = |
61 def is_control(kind: Value) = |
|
62 kind == SYSTEM || |
46 kind == SIGNAL || |
63 kind == SIGNAL || |
47 kind == EXIT || |
64 kind == EXIT |
48 kind == SYSTEM |
|
49 def is_system(kind: Value) = |
65 def is_system(kind: Value) = |
|
66 kind == SYSTEM || |
50 kind == STDIN || |
67 kind == STDIN || |
51 kind == SIGNAL || |
68 kind == SIGNAL || |
52 kind == EXIT || |
69 kind == EXIT || |
53 kind == PROMPT || |
|
54 kind == STATUS || |
70 kind == STATUS || |
55 kind == SYSTEM |
71 kind == PROMPT |
56 } |
72 } |
57 |
73 |
58 class Result(val kind: Kind.Value, val props: Properties, val result: String) { |
74 class Result(val kind: Kind.Value, val props: Properties, val result: String) { |
59 override def toString = { |
75 override def toString = { |
60 val res = XML.content(YXML.parse_failsafe(result)).mkString("") |
76 val res = XML.content(YXML.parse_failsafe(result)).mkString("") |