eliminated prompt messages;
authorwenzelm
Sat Oct 04 14:43:40 2008 +0200 (2008-10-04 ago)
changeset 28498cb1b43edb5ed
parent 28497 40e1cc165b05
child 28499 eff93bc3c14f
eliminated prompt messages;
src/Pure/Tools/isabelle_process.ML
src/Pure/Tools/isabelle_process.scala
     1.1 --- a/src/Pure/Tools/isabelle_process.ML	Sat Oct 04 14:29:45 2008 +0200
     1.2 +++ b/src/Pure/Tools/isabelle_process.ML	Sat Oct 04 14:43:40 2008 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4      Output.warning_fn  := message out_stream "F" Markup.warningN;
     1.5      Output.error_fn    := message out_stream "G" Markup.errorN;
     1.6      Output.debug_fn    := message out_stream "H" Markup.debugN;
     1.7 -    Output.prompt_fn   := message out_stream "I" Markup.promptN;
     1.8 +    Output.prompt_fn   := ignore;
     1.9      out_stream
    1.10    end;
    1.11  
     2.1 --- a/src/Pure/Tools/isabelle_process.scala	Sat Oct 04 14:29:45 2008 +0200
     2.2 +++ b/src/Pure/Tools/isabelle_process.scala	Sat Oct 04 14:43:40 2008 +0200
     2.3 @@ -38,7 +38,6 @@
     2.4      val WARNING = Value("WARNING")
     2.5      val ERROR = Value("ERROR")
     2.6      val DEBUG = Value("DEBUG")
     2.7 -    val PROMPT = Value("PROMPT")
     2.8      // messages codes
     2.9      val code = Map(
    2.10        ('A' : Int) -> Kind.INIT,
    2.11 @@ -49,7 +48,6 @@
    2.12        ('F' : Int) -> Kind.WARNING,
    2.13        ('G' : Int) -> Kind.ERROR,
    2.14        ('H' : Int) -> Kind.DEBUG,
    2.15 -      ('I' : Int) -> Kind.PROMPT,
    2.16        ('0' : Int) -> Kind.SYSTEM,
    2.17        ('1' : Int) -> Kind.STDIN,
    2.18        ('2' : Int) -> Kind.STDOUT,
    2.19 @@ -67,8 +65,7 @@
    2.20        kind == STDIN ||
    2.21        kind == SIGNAL ||
    2.22        kind == EXIT ||
    2.23 -      kind == STATUS ||
    2.24 -      kind == PROMPT
    2.25 +      kind == STATUS
    2.26    }
    2.27  
    2.28    class Result(val kind: Kind.Value, val props: Properties, val result: String) {