# HG changeset patch # User wenzelm # Date 1222277594 -7200 # Node ID f4a17868bde576a025623e8fcfbac4d0059433f9 # Parent 7b605b8b719675085f2f3d6062b03ef3e581475c protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy); added Kind.code map; diff -r 7b605b8b7196 -r f4a17868bde5 src/Pure/Tools/isabelle_process.scala --- a/src/Pure/Tools/isabelle_process.scala Wed Sep 24 19:33:13 2008 +0200 +++ b/src/Pure/Tools/isabelle_process.scala Wed Sep 24 19:33:14 2008 +0200 @@ -21,13 +21,17 @@ /* results */ object Kind extends Enumeration { - //{{{ values + //{{{ values and codes + // internal system notification + val SYSTEM = Value("SYSTEM") // Posix channels/events val STDIN = Value("STDIN") val STDOUT = Value("STDOUT") val SIGNAL = Value("SIGNAL") val EXIT = Value("EXIT") // Isabelle messages + val INIT = Value("INIT") + val STATUS = Value("STATUS") val WRITELN = Value("WRITELN") val PRIORITY = Value("PRIORITY") val TRACING = Value("TRACING") @@ -35,24 +39,36 @@ val ERROR = Value("ERROR") val DEBUG = Value("DEBUG") val PROMPT = Value("PROMPT") - val INIT = Value("INIT") - val STATUS = Value("STATUS") - // internal system notification - val SYSTEM = Value("SYSTEM") + // messages codes + val code = Map( + ('A' : Int) -> Kind.INIT, + ('B' : Int) -> Kind.STATUS, + ('C' : Int) -> Kind.WRITELN, + ('D' : Int) -> Kind.PRIORITY, + ('E' : Int) -> Kind.TRACING, + ('F' : Int) -> Kind.WARNING, + ('G' : Int) -> Kind.ERROR, + ('H' : Int) -> Kind.DEBUG, + ('I' : Int) -> Kind.PROMPT, + ('0' : Int) -> Kind.SYSTEM, + ('1' : Int) -> Kind.STDIN, + ('2' : Int) -> Kind.STDOUT, + ('3' : Int) -> Kind.SIGNAL, + ('4' : Int) -> Kind.EXIT) //}}} def is_raw(kind: Value) = kind == STDOUT def is_control(kind: Value) = + kind == SYSTEM || kind == SIGNAL || - kind == EXIT || - kind == SYSTEM + kind == EXIT def is_system(kind: Value) = + kind == SYSTEM || kind == STDIN || kind == SIGNAL || kind == EXIT || - kind == PROMPT || kind == STATUS || - kind == SYSTEM + kind == PROMPT } class Result(val kind: Kind.Value, val props: Properties, val result: String) { @@ -267,18 +283,9 @@ try_close() } else { - reader.read match { - case 'A' => kind = Kind.WRITELN - case 'B' => kind = Kind.PRIORITY - case 'C' => kind = Kind.TRACING - case 'D' => kind = Kind.WARNING - case 'E' => kind = Kind.ERROR - case 'F' => kind = Kind.DEBUG - case 'G' => kind = Kind.PROMPT - case 'H' => kind = Kind.INIT - case 'I' => kind = Kind.STATUS - case _ => kind = null - } + c = reader.read + if (Kind.code.isDefinedAt(c)) kind = Kind.code(c) + else kind = null props = null } //}}}