more abstract message channel;
authorwenzelm
Wed Jul 10 23:25:28 2013 +0200 (2013-07-10)
changeset 525845cad4a5f5615
parent 52583 0a7240d88e09
child 52585 ff525a38dba9
more abstract message channel;
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/message_channel.ML
     1.1 --- a/src/Pure/ROOT	Wed Jul 10 22:56:48 2013 +0200
     1.2 +++ b/src/Pure/ROOT	Wed Jul 10 23:25:28 2013 +0200
     1.3 @@ -181,6 +181,7 @@
     1.4      "System/isabelle_process.ML"
     1.5      "System/isabelle_system.ML"
     1.6      "System/isar.ML"
     1.7 +    "System/message_channel.ML"
     1.8      "System/options.ML"
     1.9      "System/session.ML"
    1.10      "System/system_channel.ML"
     2.1 --- a/src/Pure/ROOT.ML	Wed Jul 10 22:56:48 2013 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Wed Jul 10 23:25:28 2013 +0200
     2.3 @@ -288,6 +288,7 @@
     2.4  use "System/session.ML";
     2.5  use "System/command_line.ML";
     2.6  use "System/system_channel.ML";
     2.7 +use "System/message_channel.ML";
     2.8  use "System/isabelle_process.ML";
     2.9  use "System/invoke_scala.ML";
    2.10  use "PIDE/protocol.ML";
     3.1 --- a/src/Pure/System/isabelle_process.ML	Wed Jul 10 22:56:48 2013 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Jul 10 23:25:28 2013 +0200
     3.3 @@ -103,45 +103,13 @@
     3.4  local
     3.5  
     3.6  fun chunk s = [string_of_int (size s), "\n", s];
     3.7 -fun flush channel = ignore (try System_Channel.flush channel);
     3.8  
     3.9 -datatype target =
    3.10 -  Sync of {send: string list -> unit} |
    3.11 -  Async of {send: string list -> bool -> unit, shutdown: unit -> unit};
    3.12 -
    3.13 -fun message do_flush target name raw_props body =
    3.14 +fun message do_flush msg_channel name raw_props body =
    3.15    let
    3.16      val robust_props = map (pairself YXML.embed_controls) raw_props;
    3.17      val header = YXML.string_of (XML.Elem ((name, robust_props), []));
    3.18      val msg = chunk header @ chunk body;
    3.19 -  in (case target of Sync {send} => send msg | Async {send, ...} => send msg do_flush) end;
    3.20 -
    3.21 -fun message_output mbox channel =
    3.22 -  let
    3.23 -    fun loop receive =
    3.24 -      (case receive mbox of
    3.25 -        SOME NONE => flush channel
    3.26 -      | SOME (SOME (msg, do_flush)) =>
    3.27 -         (List.app (fn s => System_Channel.output channel s) msg;
    3.28 -          if do_flush then flush channel else ();
    3.29 -          loop (Mailbox.receive_timeout (seconds 0.02)))
    3.30 -      | NONE => (flush channel; loop (SOME o Mailbox.receive)));
    3.31 -  in fn () => loop (SOME o Mailbox.receive) end;
    3.32 -
    3.33 -fun make_target channel =
    3.34 -  if Multithreading.available then
    3.35 -    let
    3.36 -      val mbox = Mailbox.create ();
    3.37 -      val thread = Simple_Thread.fork false (message_output mbox channel);
    3.38 -    in
    3.39 -      Async {
    3.40 -        send = fn msg => fn do_flush => Mailbox.send mbox (SOME (msg, do_flush)),
    3.41 -        shutdown = fn () =>
    3.42 -          (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread)
    3.43 -      }
    3.44 -    end
    3.45 -  else
    3.46 -    Sync {send = fn msg => (List.app (fn s => System_Channel.output channel s) msg; flush channel)};
    3.47 +  in Message_Channel.send msg_channel msg do_flush end;
    3.48  
    3.49  in
    3.50  
    3.51 @@ -150,12 +118,12 @@
    3.52      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    3.53      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    3.54  
    3.55 -    val target = make_target channel;
    3.56 +    val msg_channel = Message_Channel.make channel;
    3.57  
    3.58      fun standard_message opt_serial name body =
    3.59        if body = "" then ()
    3.60        else
    3.61 -        message false target name
    3.62 +        message false msg_channel name
    3.63            ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
    3.64              (Position.properties_of (Position.thread_data ()))) body;
    3.65    in
    3.66 @@ -170,11 +138,11 @@
    3.67        (fn s => standard_message (SOME (serial ())) Markup.warningN s);
    3.68      Output.Private_Hooks.error_fn :=
    3.69        (fn (i, s) => standard_message (SOME i) Markup.errorN s);
    3.70 -    Output.Private_Hooks.protocol_message_fn := message true target Markup.protocolN;
    3.71 +    Output.Private_Hooks.protocol_message_fn := message true msg_channel Markup.protocolN;
    3.72      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    3.73      Output.Private_Hooks.prompt_fn := ignore;
    3.74 -    message true target Markup.initN [] (Session.welcome ());
    3.75 -    (case target of Async {shutdown, ...} => shutdown | _ => fn () => ())
    3.76 +    message true msg_channel Markup.initN [] (Session.welcome ());
    3.77 +    msg_channel
    3.78    end;
    3.79  
    3.80  end;
    3.81 @@ -242,10 +210,10 @@
    3.82          (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
    3.83  
    3.84      val channel = rendezvous ();
    3.85 -    val shutdown_channels = init_channels channel;
    3.86 +    val msg_channel = init_channels channel;
    3.87      val _ = Session.init_protocol_handlers ();
    3.88      val _ = loop channel;
    3.89 -  in shutdown_channels () end);
    3.90 +  in Message_Channel.shutdown msg_channel end);
    3.91  
    3.92  fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
    3.93  fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/System/message_channel.ML	Wed Jul 10 23:25:28 2013 +0200
     4.3 @@ -0,0 +1,54 @@
     4.4 +(*  Title:      Pure/System/message_channel.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Preferably asynchronous channel for Isabelle messages.
     4.8 +*)
     4.9 +
    4.10 +signature MESSAGE_CHANNEL =
    4.11 +sig
    4.12 +  type T
    4.13 +  val send: T -> string list -> bool -> unit
    4.14 +  val shutdown: T -> unit
    4.15 +  val make: System_Channel.T -> T
    4.16 +end;
    4.17 +
    4.18 +structure Message_Channel: MESSAGE_CHANNEL =
    4.19 +struct
    4.20 +
    4.21 +datatype T = Message_Channel of
    4.22 + {send: string list -> bool -> unit,
    4.23 +  shutdown: unit -> unit};
    4.24 +
    4.25 +fun send (Message_Channel {send, ...}) = send;
    4.26 +fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
    4.27 +
    4.28 +fun flush channel = ignore (try System_Channel.flush channel);
    4.29 +
    4.30 +fun message_output mbox channel =
    4.31 +  let
    4.32 +    fun loop receive =
    4.33 +      (case receive mbox of
    4.34 +        SOME NONE => flush channel
    4.35 +      | SOME (SOME (msg, do_flush)) =>
    4.36 +         (List.app (fn s => System_Channel.output channel s) msg;
    4.37 +          if do_flush then flush channel else ();
    4.38 +          loop (Mailbox.receive_timeout (seconds 0.02)))
    4.39 +      | NONE => (flush channel; loop (SOME o Mailbox.receive)));
    4.40 +  in fn () => loop (SOME o Mailbox.receive) end;
    4.41 +
    4.42 +fun make channel =
    4.43 +  if Multithreading.available then
    4.44 +    let
    4.45 +      val mbox = Mailbox.create ();
    4.46 +      val thread = Simple_Thread.fork false (message_output mbox channel);
    4.47 +      fun send msg do_flush = Mailbox.send mbox (SOME (msg, do_flush));
    4.48 +      fun shutdown () =
    4.49 +        (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);
    4.50 +    in Message_Channel {send = send, shutdown = shutdown} end
    4.51 +  else
    4.52 +    let
    4.53 +      fun send msg = (List.app (fn s => System_Channel.output channel s) msg; flush channel);
    4.54 +    in Message_Channel {send = fn msg => fn _ => send msg, shutdown = fn () => ()} end;
    4.55 +
    4.56 +end;
    4.57 +