src/Pure/System/isabelle_process.ML
author wenzelm
Tue Jul 30 19:53:06 2013 +0200 (2013-07-30 ago)
changeset 52799 6a4498b048b7
parent 52787 c143ad7811fc
child 52800 1baa5d19ac44
permissions -rw-r--r--
tuned -- more uniform ML vs. Scala;
wenzelm@30173
     1
(*  Title:      Pure/System/isabelle_process.ML
wenzelm@25528
     2
    Author:     Makarius
wenzelm@25528
     3
wenzelm@38445
     4
Isabelle process wrapper, based on private fifos for maximum
wenzelm@48712
     5
robustness and performance, or local socket for maximum portability.
wenzelm@25528
     6
*)
wenzelm@25528
     7
wenzelm@25528
     8
signature ISABELLE_PROCESS =
wenzelm@25528
     9
sig
wenzelm@42897
    10
  val is_active: unit -> bool
wenzelm@46119
    11
  val protocol_command: string -> (string list -> unit) -> unit
wenzelm@52655
    12
  val reset_tracing: Document_ID.exec -> unit
wenzelm@43684
    13
  val crashes: exn list Synchronized.var
wenzelm@45029
    14
  val init_fifos: string -> string -> unit
wenzelm@45028
    15
  val init_socket: string -> unit
wenzelm@25528
    16
end;
wenzelm@25528
    17
wenzelm@31797
    18
structure Isabelle_Process: ISABELLE_PROCESS =
wenzelm@25528
    19
struct
wenzelm@25528
    20
wenzelm@42897
    21
(* print mode *)
wenzelm@25554
    22
wenzelm@25748
    23
val isabelle_processN = "isabelle_process";
wenzelm@25748
    24
wenzelm@42897
    25
fun is_active () = Print_Mode.print_mode_active isabelle_processN;
wenzelm@42897
    26
wenzelm@26550
    27
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
wenzelm@28036
    28
val _ = Markup.add_mode isabelle_processN YXML.output_markup;
wenzelm@25841
    29
wenzelm@25841
    30
wenzelm@46119
    31
(* protocol commands *)
wenzelm@38270
    32
wenzelm@38270
    33
local
wenzelm@38270
    34
wenzelm@43684
    35
val commands =
wenzelm@43684
    36
  Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table);
wenzelm@38270
    37
wenzelm@38270
    38
in
wenzelm@38270
    39
wenzelm@46119
    40
fun protocol_command name cmd =
wenzelm@43684
    41
  Synchronized.change commands (fn cmds =>
wenzelm@38270
    42
   (if not (Symtab.defined cmds name) then ()
wenzelm@52582
    43
    else warning ("Redefining Isabelle protocol command " ^ quote name);
wenzelm@43684
    44
    Symtab.update (name, cmd) cmds));
wenzelm@38270
    45
wenzelm@46119
    46
fun run_command name args =
wenzelm@43684
    47
  (case Symtab.lookup (Synchronized.value commands) name of
wenzelm@52582
    48
    NONE => error ("Undefined Isabelle protocol command " ^ quote name)
wenzelm@46119
    49
  | SOME cmd =>
wenzelm@46119
    50
      (Runtime.debugging cmd args handle exn =>
wenzelm@52582
    51
        error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
wenzelm@48056
    52
          ML_Compiler.exn_message exn)));
wenzelm@38270
    53
wenzelm@38270
    54
end;
wenzelm@38270
    55
wenzelm@38270
    56
wenzelm@50505
    57
(* restricted tracing messages *)
wenzelm@49647
    58
wenzelm@52105
    59
val tracing_messages =
wenzelm@52105
    60
  Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
wenzelm@49647
    61
wenzelm@52655
    62
fun reset_tracing exec_id =
wenzelm@52655
    63
  Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
wenzelm@49647
    64
wenzelm@50505
    65
fun update_tracing () =
wenzelm@50911
    66
  (case Position.parse_id (Position.thread_data ()) of
wenzelm@49647
    67
    NONE => ()
wenzelm@52655
    68
  | SOME exec_id =>
wenzelm@50505
    69
      let
wenzelm@52560
    70
        val ok =
wenzelm@52105
    71
          Synchronized.change_result tracing_messages (fn tab =>
wenzelm@50505
    72
            let
wenzelm@52655
    73
              val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
wenzelm@52105
    74
              val ok = n <= Options.default_int "editor_tracing_messages";
wenzelm@52655
    75
            in (ok, Inttab.update (exec_id, n) tab) end);
wenzelm@50505
    76
      in
wenzelm@50505
    77
        if ok then ()
wenzelm@50505
    78
        else
wenzelm@50505
    79
          let
wenzelm@50505
    80
            val (text, promise) = Active.dialog_text ();
wenzelm@50505
    81
            val _ =
wenzelm@50505
    82
              writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
wenzelm@51044
    83
                text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
wenzelm@50505
    84
            val m = Markup.parse_int (Future.join promise)
wenzelm@50505
    85
              handle Fail _ => error "Stopped";
wenzelm@50505
    86
          in
wenzelm@52105
    87
            Synchronized.change tracing_messages
wenzelm@52655
    88
              (Inttab.map_default (exec_id, 0) (fn k => k - m))
wenzelm@50505
    89
          end
wenzelm@50505
    90
      end);
wenzelm@49647
    91
wenzelm@49647
    92
wenzelm@40134
    93
(* message channels *)
wenzelm@25841
    94
wenzelm@25841
    95
local
wenzelm@25810
    96
wenzelm@40134
    97
fun chunk s = [string_of_int (size s), "\n", s];
wenzelm@26574
    98
wenzelm@52584
    99
fun message do_flush msg_channel name raw_props body =
wenzelm@43771
   100
  let
wenzelm@43772
   101
    val robust_props = map (pairself YXML.embed_controls) raw_props;
wenzelm@49677
   102
    val header = YXML.string_of (XML.Elem ((name, robust_props), []));
wenzelm@52580
   103
    val msg = chunk header @ chunk body;
wenzelm@52584
   104
  in Message_Channel.send msg_channel msg do_flush end;
wenzelm@52583
   105
wenzelm@28188
   106
in
wenzelm@28188
   107
wenzelm@48712
   108
fun init_channels channel =
wenzelm@28189
   109
  let
wenzelm@40134
   110
    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
wenzelm@40134
   111
    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
wenzelm@40134
   112
wenzelm@52584
   113
    val msg_channel = Message_Channel.make channel;
wenzelm@52580
   114
wenzelm@52580
   115
    fun standard_message opt_serial name body =
wenzelm@52580
   116
      if body = "" then ()
wenzelm@52580
   117
      else
wenzelm@52584
   118
        message false msg_channel name
wenzelm@52580
   119
          ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
wenzelm@52580
   120
            (Position.properties_of (Position.thread_data ()))) body;
wenzelm@28044
   121
  in
wenzelm@52580
   122
    Output.Private_Hooks.status_fn := standard_message NONE Markup.statusN;
wenzelm@52580
   123
    Output.Private_Hooks.report_fn := standard_message NONE Markup.reportN;
wenzelm@52580
   124
    Output.Private_Hooks.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
wenzelm@49677
   125
    Output.Private_Hooks.writeln_fn :=
wenzelm@52580
   126
      (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
wenzelm@49647
   127
    Output.Private_Hooks.tracing_fn :=
wenzelm@52580
   128
      (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s));
wenzelm@49677
   129
    Output.Private_Hooks.warning_fn :=
wenzelm@52580
   130
      (fn s => standard_message (SOME (serial ())) Markup.warningN s);
wenzelm@49677
   131
    Output.Private_Hooks.error_fn :=
wenzelm@52580
   132
      (fn (i, s) => standard_message (SOME i) Markup.errorN s);
wenzelm@52584
   133
    Output.Private_Hooks.protocol_message_fn := message true msg_channel Markup.protocolN;
wenzelm@40133
   134
    Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
wenzelm@40133
   135
    Output.Private_Hooks.prompt_fn := ignore;
wenzelm@52584
   136
    message true msg_channel Markup.initN [] (Session.welcome ());
wenzelm@52584
   137
    msg_channel
wenzelm@28044
   138
  end;
wenzelm@25841
   139
wenzelm@28188
   140
end;
wenzelm@28188
   141
wenzelm@25841
   142
wenzelm@39234
   143
(* protocol loop -- uninterruptible *)
wenzelm@38270
   144
wenzelm@43684
   145
val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
wenzelm@38270
   146
wenzelm@38270
   147
local
wenzelm@38270
   148
wenzelm@38270
   149
fun recover crash =
wenzelm@43684
   150
  (Synchronized.change crashes (cons crash);
wenzelm@38270
   151
    warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
wenzelm@38270
   152
wenzelm@45029
   153
fun read_chunk channel len =
wenzelm@38270
   154
  let
wenzelm@38270
   155
    val n =
wenzelm@38270
   156
      (case Int.fromString len of
wenzelm@38270
   157
        SOME n => n
wenzelm@52799
   158
      | NONE => error ("Isabelle process: malformed header " ^ quote len));
wenzelm@45029
   159
    val chunk = System_Channel.inputN channel n;
wenzelm@52799
   160
    val i = size chunk;
wenzelm@38270
   161
  in
wenzelm@52799
   162
    if i <> n then
wenzelm@52799
   163
      error ("Isabelle process: bad chunk (unexpected EOF after " ^
wenzelm@52799
   164
        string_of_int i ^ " of " ^ string_of_int n ^ " bytes)")
wenzelm@52799
   165
    else chunk
wenzelm@38270
   166
  end;
wenzelm@38270
   167
wenzelm@45029
   168
fun read_command channel =
wenzelm@45029
   169
  (case System_Channel.input_line channel of
wenzelm@38270
   170
    NONE => raise Runtime.TERMINATE
wenzelm@45029
   171
  | SOME line => map (read_chunk channel) (space_explode "," line));
wenzelm@38270
   172
wenzelm@52559
   173
fun worker_guest e =
wenzelm@52559
   174
  Future.worker_guest "Isabelle_Process.loop" (Future.new_group NONE) e ();
wenzelm@52559
   175
wenzelm@38270
   176
in
wenzelm@38270
   177
wenzelm@45029
   178
fun loop channel =
wenzelm@38270
   179
  let val continue =
wenzelm@45029
   180
    (case read_command channel of
wenzelm@38270
   181
      [] => (Output.error_msg "Isabelle process: no input"; true)
wenzelm@52559
   182
    | name :: args => (worker_guest (fn () => run_command name args); true))
wenzelm@38270
   183
    handle Runtime.TERMINATE => false
wenzelm@38270
   184
      | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
wenzelm@52770
   185
  in
wenzelm@52770
   186
    if continue then loop channel
wenzelm@52787
   187
    else (Future.shutdown (); Goal.reset_futures (); Execution.reset ())
wenzelm@52770
   188
  end;
wenzelm@38270
   189
wenzelm@38270
   190
end;
wenzelm@38270
   191
wenzelm@38270
   192
wenzelm@25554
   193
(* init *)
wenzelm@25554
   194
wenzelm@50715
   195
val default_modes1 =
wenzelm@50715
   196
  [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN];
wenzelm@50715
   197
val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
wenzelm@49566
   198
wenzelm@52578
   199
val init = uninterruptible (fn _ => fn rendezvous =>
wenzelm@38253
   200
  let
wenzelm@46548
   201
    val _ = Output.physical_stderr Symbol.STX;
wenzelm@39528
   202
wenzelm@49661
   203
    val _ = Printer.show_markup_default := true;
wenzelm@39528
   204
    val _ = Context.set_thread_data NONE;
wenzelm@43671
   205
    val _ =
wenzelm@43671
   206
      Unsynchronized.change print_mode
wenzelm@49566
   207
        (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
wenzelm@39528
   208
wenzelm@45029
   209
    val channel = rendezvous ();
wenzelm@52584
   210
    val msg_channel = init_channels channel;
wenzelm@52111
   211
    val _ = Session.init_protocol_handlers ();
wenzelm@52583
   212
    val _ = loop channel;
wenzelm@52584
   213
  in Message_Channel.shutdown msg_channel end);
wenzelm@25528
   214
wenzelm@45029
   215
fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
wenzelm@45029
   216
fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);
wenzelm@45028
   217
wenzelm@25528
   218
end;
wenzelm@39528
   219