src/Pure/PIDE/command.scala
changeset 52536 3a35ce87a55c
parent 52535 b7badd371e4d
child 52642 84eb792224a8
     1.1 --- a/src/Pure/PIDE/command.scala	Fri Jul 05 22:09:16 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Fri Jul 05 22:58:24 2013 +0200
     1.3 @@ -2,12 +2,11 @@
     1.4      Author:     Fabian Immler, TU Munich
     1.5      Author:     Makarius
     1.6  
     1.7 -Prover commands with semantic state.
     1.8 +Prover commands with accumulated results from execution.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12  
    1.13 -import java.lang.System
    1.14  
    1.15  import scala.collection.mutable
    1.16  import scala.collection.immutable.SortedMap
    1.17 @@ -84,7 +83,9 @@
    1.18                  state.add_status(markup)
    1.19                    .add_markup(Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
    1.20  
    1.21 -              case _ => System.err.println("Ignored status message: " + msg); state
    1.22 +              case _ =>
    1.23 +                java.lang.System.err.println("Ignored status message: " + msg)
    1.24 +                state
    1.25              })
    1.26  
    1.27          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
    1.28 @@ -104,7 +105,7 @@
    1.29                  val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.30                  state.add_markup(info)
    1.31                case _ =>
    1.32 -                // FIXME System.err.println("Ignored report message: " + msg)
    1.33 +                // FIXME java.lang.System.err.println("Ignored report message: " + msg)
    1.34                  state
    1.35              })
    1.36          case XML.Elem(Markup(name, atts), body) =>
    1.37 @@ -122,7 +123,9 @@
    1.38                  else st0
    1.39  
    1.40                st1
    1.41 -            case _ => System.err.println("Ignored message without serial number: " + message); this
    1.42 +            case _ =>
    1.43 +              java.lang.System.err.println("Ignored message without serial number: " + message)
    1.44 +              this
    1.45            }
    1.46        }
    1.47