more direct message header: eliminated historic encoding via single letter;
authorwenzelm
Mon Oct 01 20:17:30 2012 +0200 (2012-10-01 ago)
changeset 49677c4e2762a265c
parent 49676 882aa078eeae
child 49678 954d1c94f55f
more direct message header: eliminated historic encoding via single letter;
src/Pure/PIDE/isabelle_markup.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Mon Oct 01 20:16:37 2012 +0200
     1.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Mon Oct 01 20:17:30 2012 +0200
     1.3 @@ -96,6 +96,13 @@
     1.4    val finishedN: string val finished: Markup.T
     1.5    val failedN: string val failed: Markup.T
     1.6    val serialN: string
     1.7 +  val initN: string
     1.8 +  val statusN: string
     1.9 +  val writelnN: string
    1.10 +  val tracingN: string
    1.11 +  val warningN: string
    1.12 +  val errorN: string
    1.13 +  val protocolN: string
    1.14    val legacyN: string val legacy: Markup.T
    1.15    val promptN: string val prompt: Markup.T
    1.16    val reportN: string val report: Markup.T
    1.17 @@ -291,6 +298,14 @@
    1.18  
    1.19  val serialN = "serial";
    1.20  
    1.21 +val initN = "init";
    1.22 +val statusN = "status";
    1.23 +val writelnN = "writeln";
    1.24 +val tracingN = "tracing";
    1.25 +val warningN = "warning";
    1.26 +val errorN = "error";
    1.27 +val protocolN = "protocol";
    1.28 +
    1.29  val (legacyN, legacy) = markup_elem "legacy";
    1.30  val (promptN, prompt) = markup_elem "prompt";
    1.31  
     2.1 --- a/src/Pure/System/isabelle_process.ML	Mon Oct 01 20:16:37 2012 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Oct 01 20:17:30 2012 +0200
     2.3 @@ -89,16 +89,16 @@
     2.4  
     2.5  fun chunk s = [string_of_int (size s), "\n", s];
     2.6  
     2.7 -fun message do_flush mbox ch raw_props body =
     2.8 +fun message do_flush mbox name raw_props body =
     2.9    let
    2.10      val robust_props = map (pairself YXML.embed_controls) raw_props;
    2.11 -    val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
    2.12 +    val header = YXML.string_of (XML.Elem ((name, robust_props), []));
    2.13    in Mailbox.send mbox (chunk header @ chunk body, do_flush) end;
    2.14  
    2.15 -fun standard_message mbox opt_serial ch body =
    2.16 +fun standard_message mbox opt_serial name body =
    2.17    if body = "" then ()
    2.18    else
    2.19 -    message false mbox ch
    2.20 +    message false mbox name
    2.21        ((case opt_serial of SOME i => cons (Isabelle_Markup.serialN, string_of_int i) | _ => I)
    2.22          (Position.properties_of (Position.thread_data ()))) body;
    2.23  
    2.24 @@ -124,17 +124,22 @@
    2.25      val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
    2.26      val _ = Simple_Thread.fork false (message_output mbox channel);
    2.27    in
    2.28 -    Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
    2.29 -    Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
    2.30 -    Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
    2.31 +    Output.Private_Hooks.status_fn := standard_message mbox NONE Isabelle_Markup.statusN;
    2.32 +    Output.Private_Hooks.report_fn := standard_message mbox NONE Isabelle_Markup.reportN;
    2.33 +    Output.Private_Hooks.writeln_fn :=
    2.34 +      (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.writelnN s);
    2.35      Output.Private_Hooks.tracing_fn :=
    2.36 -      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) "E" s));
    2.37 -    Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
    2.38 -    Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
    2.39 -    Output.Private_Hooks.protocol_message_fn := message true mbox "H";
    2.40 +      (fn s =>
    2.41 +        (update_tracing_limits s;
    2.42 +          standard_message mbox (SOME (serial ())) Isabelle_Markup.tracingN s));
    2.43 +    Output.Private_Hooks.warning_fn :=
    2.44 +      (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.warningN s);
    2.45 +    Output.Private_Hooks.error_fn :=
    2.46 +      (fn (i, s) => standard_message mbox (SOME i) Isabelle_Markup.errorN s);
    2.47 +    Output.Private_Hooks.protocol_message_fn := message true mbox Isabelle_Markup.protocolN;
    2.48      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    2.49      Output.Private_Hooks.prompt_fn := ignore;
    2.50 -    message true mbox "A" [] (Session.welcome ())
    2.51 +    message true mbox Isabelle_Markup.initN [] (Session.welcome ())
    2.52    end;
    2.53  
    2.54  end;
     3.1 --- a/src/Pure/System/isabelle_process.scala	Mon Oct 01 20:16:37 2012 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Oct 01 20:17:30 2012 +0200
     3.3 @@ -20,19 +20,6 @@
     3.4  {
     3.5    /* messages */
     3.6  
     3.7 -  object Kind
     3.8 -  {
     3.9 -    val message_markup = Map(
    3.10 -      ('A' : Int) -> Isabelle_Markup.INIT,
    3.11 -      ('B' : Int) -> Isabelle_Markup.STATUS,
    3.12 -      ('C' : Int) -> Isabelle_Markup.REPORT,
    3.13 -      ('D' : Int) -> Isabelle_Markup.WRITELN,
    3.14 -      ('E' : Int) -> Isabelle_Markup.TRACING,
    3.15 -      ('F' : Int) -> Isabelle_Markup.WARNING,
    3.16 -      ('G' : Int) -> Isabelle_Markup.ERROR,
    3.17 -      ('H' : Int) -> Isabelle_Markup.PROTOCOL)
    3.18 -  }
    3.19 -
    3.20    sealed abstract class Message
    3.21  
    3.22    class Input(name: String, args: List[String]) extends Message
    3.23 @@ -375,9 +362,8 @@
    3.24              //{{{
    3.25              val header = read_chunk(true)
    3.26              header match {
    3.27 -              case List(XML.Elem(Markup(name, props), Nil))
    3.28 -                  if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
    3.29 -                val kind = Kind.message_markup(name(0))
    3.30 +              case List(XML.Elem(Markup(name, props), Nil)) =>
    3.31 +                val kind = name.intern
    3.32                  val body = read_chunk(kind != Isabelle_Markup.PROTOCOL)
    3.33                  output_message(kind, props, body)
    3.34                case _ =>