src/Pure/System/isabelle_process.ML
changeset 49647 21ae8500d261
parent 49566 66cbf8bb4693
child 49661 ac48def96b69
equal deleted inserted replaced
49646:77a0a53caa2f 49647:21ae8500d261
    15 
    15 
    16 signature ISABELLE_PROCESS =
    16 signature ISABELLE_PROCESS =
    17 sig
    17 sig
    18   val is_active: unit -> bool
    18   val is_active: unit -> bool
    19   val protocol_command: string -> (string list -> unit) -> unit
    19   val protocol_command: string -> (string list -> unit) -> unit
       
    20   val tracing_limit: int Unsynchronized.ref;
       
    21   val reset_tracing_limits: unit -> unit
    20   val crashes: exn list Synchronized.var
    22   val crashes: exn list Synchronized.var
    21   val init_fifos: string -> string -> unit
    23   val init_fifos: string -> string -> unit
    22   val init_socket: string -> unit
    24   val init_socket: string -> unit
    23 end;
    25 end;
    24 
    26 
    57       (Runtime.debugging cmd args handle exn =>
    59       (Runtime.debugging cmd args handle exn =>
    58         error ("Isabelle process protocol failure: " ^ quote name ^ "\n" ^
    60         error ("Isabelle process protocol failure: " ^ quote name ^ "\n" ^
    59           ML_Compiler.exn_message exn)));
    61           ML_Compiler.exn_message exn)));
    60 
    62 
    61 end;
    63 end;
       
    64 
       
    65 
       
    66 (* tracing limit *)
       
    67 
       
    68 val tracing_limit = Unsynchronized.ref 500000;
       
    69 
       
    70 val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table);
       
    71 
       
    72 fun reset_tracing_limits () = Synchronized.change tracing_limits (K Inttab.empty);
       
    73 
       
    74 fun update_tracing_limits msg =
       
    75   (case Position.get_id (Position.thread_data ()) of
       
    76     NONE => ()
       
    77   | SOME id =>
       
    78       Synchronized.change tracing_limits (fn tab =>
       
    79         let
       
    80           val i = Markup.parse_int id;
       
    81           val n = the_default 0 (Inttab.lookup tab i) + size msg;
       
    82           val _ = if n > ! tracing_limit then raise Output.TRACING_LIMIT n else ();
       
    83         in Inttab.update (i, n) tab end));
    62 
    84 
    63 
    85 
    64 (* message channels *)
    86 (* message channels *)
    65 
    87 
    66 local
    88 local
   103     val _ = Simple_Thread.fork false (message_output mbox channel);
   125     val _ = Simple_Thread.fork false (message_output mbox channel);
   104   in
   126   in
   105     Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
   127     Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
   106     Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
   128     Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
   107     Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
   129     Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
   108     Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
   130     Output.Private_Hooks.tracing_fn :=
       
   131       (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) "E" s));
   109     Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
   132     Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
   110     Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
   133     Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
   111     Output.Private_Hooks.protocol_message_fn := message true mbox "H";
   134     Output.Private_Hooks.protocol_message_fn := message true mbox "H";
   112     Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
   135     Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
   113     Output.Private_Hooks.prompt_fn := ignore;
   136     Output.Private_Hooks.prompt_fn := ignore;