src/Pure/System/isabelle_process.ML
author wenzelm
Wed Nov 26 14:35:55 2014 +0100 (2014-11-26 ago)
changeset 59055 5a7157b8e870
parent 58850 1bb0ad7827b4
child 59056 cbe9563c03d1
permissions -rw-r--r--
more informative failure of protocol commands, with exception trace;
eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);
     1 (*  Title:      Pure/System/isabelle_process.ML
     2     Author:     Makarius
     3 
     4 Isabelle process wrapper.
     5 *)
     6 
     7 signature ISABELLE_PROCESS =
     8 sig
     9   val is_active: unit -> bool
    10   val protocol_command: string -> (string list -> unit) -> unit
    11   val reset_tracing: Document_ID.exec -> unit
    12   val crashes: exn list Synchronized.var
    13   val init_fifos: string -> string -> unit
    14   val init_socket: string -> unit
    15 end;
    16 
    17 structure Isabelle_Process: ISABELLE_PROCESS =
    18 struct
    19 
    20 (* print mode *)
    21 
    22 val isabelle_processN = "isabelle_process";
    23 
    24 fun is_active () = Print_Mode.print_mode_active isabelle_processN;
    25 
    26 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
    27 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
    28 
    29 
    30 (* protocol commands *)
    31 
    32 local
    33 
    34 val commands =
    35   Synchronized.var "Isabelle_Process.commands"
    36     (Symtab.empty: (string list -> unit) Symtab.table);
    37 
    38 in
    39 
    40 fun protocol_command name cmd =
    41   Synchronized.change commands (fn cmds =>
    42    (if not (Symtab.defined cmds name) then ()
    43     else warning ("Redefining Isabelle protocol command " ^ quote name);
    44     Symtab.update (name, cmd) cmds));
    45 
    46 fun run_command name args =
    47   (case Symtab.lookup (Synchronized.value commands) name of
    48     NONE => error ("Undefined Isabelle protocol command " ^ quote name)
    49   | SOME cmd =>
    50       (print_exception_trace Runtime.exn_message Output.system_message (fn () => cmd args)
    51         handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name)));
    52 
    53 end;
    54 
    55 
    56 (* restricted tracing messages *)
    57 
    58 val tracing_messages =
    59   Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
    60 
    61 fun reset_tracing exec_id =
    62   Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
    63 
    64 fun update_tracing () =
    65   (case Position.parse_id (Position.thread_data ()) of
    66     NONE => ()
    67   | SOME exec_id =>
    68       let
    69         val ok =
    70           Synchronized.change_result tracing_messages (fn tab =>
    71             let
    72               val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
    73               val ok = n <= Options.default_int "editor_tracing_messages";
    74             in (ok, Inttab.update (exec_id, n) tab) end);
    75       in
    76         if ok then ()
    77         else
    78           let
    79             val (text, promise) = Active.dialog_text ();
    80             val _ =
    81               writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
    82                 text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
    83             val m = Markup.parse_int (Future.join promise)
    84               handle Fail _ => error "Stopped";
    85           in
    86             Synchronized.change tracing_messages
    87               (Inttab.map_default (exec_id, 0) (fn k => k - m))
    88           end
    89       end);
    90 
    91 
    92 (* output channels *)
    93 
    94 val serial_props = Markup.serial_properties o serial;
    95 
    96 fun init_channels channel =
    97   let
    98     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    99     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
   100 
   101     val msg_channel = Message_Channel.make channel;
   102 
   103     fun message name props body =
   104       Message_Channel.send msg_channel (Message_Channel.message name props body);
   105 
   106     fun standard_message props name body =
   107       if forall (fn s => s = "") body then ()
   108       else
   109         let
   110           val props' =
   111             (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
   112               (false, SOME id') => props @ [(Markup.idN, id')]
   113             | _ => props);
   114         in message name props' body end;
   115   in
   116     Output.status_fn := standard_message [] Markup.statusN;
   117     Output.report_fn := standard_message [] Markup.reportN;
   118     Output.result_fn :=
   119       (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
   120     Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
   121     Output.tracing_fn :=
   122       (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
   123     Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
   124     Output.error_message_fn :=
   125       (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
   126     Output.system_message_fn := message Markup.systemN [];
   127     Output.protocol_message_fn := message Markup.protocolN;
   128     message Markup.initN [] [Session.welcome ()];
   129     msg_channel
   130   end;
   131 
   132 
   133 (* protocol loop -- uninterruptible *)
   134 
   135 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
   136 
   137 local
   138 
   139 fun recover crash =
   140   (Synchronized.change crashes (cons crash);
   141     Output.physical_stderr
   142       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
   143 
   144 fun read_chunk channel len =
   145   let
   146     val n =
   147       (case Int.fromString len of
   148         SOME n => n
   149       | NONE => error ("Isabelle process: malformed header " ^ quote len));
   150     val chunk = System_Channel.inputN channel n;
   151     val i = size chunk;
   152   in
   153     if i <> n then
   154       error ("Isabelle process: bad chunk (unexpected EOF after " ^
   155         string_of_int i ^ " of " ^ string_of_int n ^ " bytes)")
   156     else chunk
   157   end;
   158 
   159 fun read_command channel =
   160   System_Channel.input_line channel
   161   |> Option.map (fn line => map (read_chunk channel) (space_explode "," line));
   162 
   163 fun task_context e =
   164   Future.task_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
   165 
   166 in
   167 
   168 fun loop channel =
   169   let
   170     val continue =
   171       (case read_command channel of
   172         NONE => false
   173       | SOME [] => (Output.system_message "Isabelle process: no input"; true)
   174       | SOME (name :: args) => (task_context (fn () => run_command name args); true))
   175       handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
   176   in
   177     if continue then loop channel
   178     else (Future.shutdown (); Execution.reset (); ())
   179   end;
   180 
   181 end;
   182 
   183 
   184 (* init *)
   185 
   186 val default_modes1 =
   187   [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN];
   188 val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
   189 
   190 val init = uninterruptible (fn _ => fn rendezvous =>
   191   let
   192     val _ = SHA1_Samples.test ()
   193       handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn);
   194     val _ = Output.physical_stderr Symbol.STX;
   195 
   196     val _ = Printer.show_markup_default := true;
   197     val _ = Context.set_thread_data NONE;
   198     val _ =
   199       Unsynchronized.change print_mode
   200         (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
   201 
   202     val channel = rendezvous ();
   203     val msg_channel = init_channels channel;
   204     val _ = Session.init_protocol_handlers ();
   205     val _ = loop channel;
   206   in Message_Channel.shutdown msg_channel end);
   207 
   208 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
   209 fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);
   210 
   211 end;
   212