1.1 --- a/src/Pure/General/markup.ML	Fri Jan 16 22:54:11 2009 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Fri Jan 16 22:56:12 2009 +0100
     1.3 @@ -95,17 +95,7 @@
     1.4    val editN: string val edit: string -> string -> T
     1.5    val pidN: string
     1.6    val sessionN: string
     1.7 -  val classN: string
     1.8 -  val messageN: string val message: string -> T
     1.9    val promptN: string val prompt: T
    1.10 -  val writelnN: string
    1.11 -  val priorityN: string
    1.12 -  val tracingN: string
    1.13 -  val warningN: string
    1.14 -  val errorN: string
    1.15 -  val debugN: string
    1.16 -  val initN: string
    1.17 -  val statusN: string
    1.18    val no_output: output * output
    1.19    val default_output: T -> output * output
    1.20    val add_mode: string -> (T -> output * output) -> unit
    1.21 @@ -284,19 +274,8 @@
    1.22  val pidN = "pid";
    1.23  val sessionN = "session";
    1.24  
    1.25 -val classN = "class";
    1.26 -val (messageN, message) = markup_string "message" classN;
    1.27 -
    1.28  val (promptN, prompt) = markup_elem "prompt";
    1.29  
    1.30 -val writelnN = "writeln";
    1.31 -val priorityN = "priority";
    1.32 -val tracingN = "tracing";
    1.33 -val warningN = "warning";
    1.34 -val errorN = "error";
    1.35 -val debugN = "debug";
    1.36 -val initN = "init";
    1.37 -val statusN = "status";
    1.38  
    1.39  
    1.40  (* print mode operations *)

     2.1 --- a/src/Pure/General/markup.scala	Fri Jan 16 22:54:11 2009 +0100
     2.2 +++ b/src/Pure/General/markup.scala	Fri Jan 16 22:56:12 2009 +0100
     2.3 @@ -131,6 +131,21 @@
     2.4    val SESSION = "session"
     2.5  
     2.6    val MESSAGE = "message"
     2.7 +  val CLASS = "class"
     2.8 +
     2.9 +  val INIT = "init"
    2.10 +  val STATUS = "status"
    2.11 +  val WRITELN = "writeln"
    2.12 +  val PRIORITY = "priority"
    2.13 +  val TRACING = "tracing"
    2.14 +  val WARNING = "warning"
    2.15 +  val ERROR = "error"
    2.16 +  val DEBUG = "debug"
    2.17 +  val SYSTEM = "system"
    2.18 +  val STDIN = "stdin"
    2.19 +  val STDOUT = "stdout"
    2.20 +  val SIGNAL = "signal"
    2.21 +  val EXIT = "exit"
    2.22  
    2.23  
    2.24    /* content */

     3.1 --- a/src/Pure/Tools/isabelle_process.ML	Fri Jan 16 22:54:11 2009 +0100
     3.2 +++ b/src/Pure/Tools/isabelle_process.ML	Fri Jan 16 22:56:12 2009 +0100
     3.3 @@ -55,9 +55,6 @@
     3.4    let val clean = clean_string [Symbol.STX, "\n", "\r"]
     3.5    in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
     3.6  
     3.7 -fun message_text class body =
     3.8 -  YXML.element Markup.messageN [(Markup.classN, class)] [clean_string [Symbol.STX] body];
     3.9 -
    3.10  fun message_pos trees = trees |> get_first
    3.11    (fn XML.Elem (name, atts, ts) =>
    3.12          if name = Markup.positionN then SOME (Position.of_properties atts)
    3.13 @@ -69,21 +66,21 @@
    3.14  
    3.15  in
    3.16  
    3.17 -fun message _ _ _ "" = ()
    3.18 -  | message out_stream ch class body =
    3.19 +fun message _ _ "" = ()
    3.20 +  | message out_stream ch body =
    3.21        let
    3.22          val pos = the_default Position.none (message_pos (YXML.parse_body body));
    3.23          val props =
    3.24            Position.properties_of (Position.thread_data ())
    3.25            |> Position.default_properties pos;
    3.26 -        val txt = message_text class body;
    3.27 +        val txt = clean_string [Symbol.STX] body;
    3.28        in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
    3.29  
    3.30  fun init_message out_stream =
    3.31    let
    3.32      val pid = (Markup.pidN, process_id ());
    3.33      val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
    3.34 -    val text = message_text Markup.initN (Session.welcome ());
    3.35 +    val text = Session.welcome ();
    3.36    in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
    3.37  
    3.38  end;
    3.39 @@ -116,13 +113,13 @@
    3.40      val _ = SimpleThread.fork false (auto_flush out_stream);
    3.41      val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
    3.42    in
    3.43 -    Output.status_fn   := message out_stream "B" Markup.statusN;
    3.44 -    Output.writeln_fn  := message out_stream "C" Markup.writelnN;
    3.45 -    Output.priority_fn := message out_stream "D" Markup.priorityN;
    3.46 -    Output.tracing_fn  := message out_stream "E" Markup.tracingN;
    3.47 -    Output.warning_fn  := message out_stream "F" Markup.warningN;
    3.48 -    Output.error_fn    := message out_stream "G" Markup.errorN;
    3.49 -    Output.debug_fn    := message out_stream "H" Markup.debugN;
    3.50 +    Output.status_fn   := message out_stream "B";
    3.51 +    Output.writeln_fn  := message out_stream "C";
    3.52 +    Output.priority_fn := message out_stream "D";
    3.53 +    Output.tracing_fn  := message out_stream "E";
    3.54 +    Output.warning_fn  := message out_stream "F";
    3.55 +    Output.error_fn    := message out_stream "G";
    3.56 +    Output.debug_fn    := message out_stream "H";
    3.57      Output.prompt_fn   := ignore;
    3.58      out_stream
    3.59    end;

     4.1 --- a/src/Pure/Tools/isabelle_process.scala	Fri Jan 16 22:54:11 2009 +0100
     4.2 +++ b/src/Pure/Tools/isabelle_process.scala	Fri Jan 16 22:56:12 2009 +0100
     4.3 @@ -50,6 +50,21 @@
     4.4        ('2' : Int) -> Kind.STDOUT,
     4.5        ('3' : Int) -> Kind.SIGNAL,
     4.6        ('4' : Int) -> Kind.EXIT)
     4.7 +    // message markup
     4.8 +    val markup = Map(
     4.9 +      Kind.INIT -> Markup.INIT,
    4.10 +      Kind.STATUS -> Markup.STATUS,
    4.11 +      Kind.WRITELN -> Markup.WRITELN,
    4.12 +      Kind.PRIORITY -> Markup.PRIORITY,
    4.13 +      Kind.TRACING -> Markup.TRACING,
    4.14 +      Kind.WARNING -> Markup.WARNING,
    4.15 +      Kind.ERROR -> Markup.ERROR,
    4.16 +      Kind.DEBUG -> Markup.DEBUG,
    4.17 +      Kind.SYSTEM -> Markup.SYSTEM,
    4.18 +      Kind.STDIN -> Markup.STDIN,
    4.19 +      Kind.STDOUT -> Markup.STDOUT,
    4.20 +      Kind.SIGNAL -> Markup.SIGNAL,
    4.21 +      Kind.EXIT -> Markup.EXIT)
    4.22      //}}}
    4.23      def is_raw(kind: Value) =
    4.24        kind == STDOUT
    4.25 @@ -67,8 +82,10 @@
    4.26  
    4.27    class Result(val kind: Kind.Value, val props: Properties, val result: String) {
    4.28      override def toString = {
    4.29 -      val tree = YXML.parse_failsafe(result)
    4.30 -      val res = if (kind == Kind.STATUS) tree.toString else XML.content(tree).mkString
    4.31 +      val trees = YXML.parse_body_failsafe(result)
    4.32 +      val res =
    4.33 +        if (kind == Kind.STATUS) trees.map(_.toString).mkString
    4.34 +        else trees.flatMap(XML.content(_).mkString).mkString
    4.35        if (props == null) kind.toString + " [[" + res + "]]"
    4.36        else kind.toString + " " + props.toString + " [[" + res + "]]"
    4.37      }
    4.38 @@ -77,6 +94,10 @@
    4.39      def is_system = Kind.is_system(kind)
    4.40    }
    4.41  
    4.42 +  def parse_message(kind: Kind.Value, result: String) = {
    4.43 +    XML.Elem(Markup.MESSAGE, List((Markup.CLASS, Kind.markup(kind))),
    4.44 +      YXML.parse_body_failsafe(result))
    4.45 +  }
    4.46  }
    4.47  
    4.48