src/Pure/System/isabelle_process.ML
changeset 71878 3cd8449829fa
parent 71675 55cb4271858b
child 72104 d9a42786fbc9
equal deleted inserted replaced
71877:f5dd0abd49d1 71878:3cd8449829fa
     5 *)
     5 *)
     6 
     6 
     7 signature ISABELLE_PROCESS =
     7 signature ISABELLE_PROCESS =
     8 sig
     8 sig
     9   val is_active: unit -> bool
     9   val is_active: unit -> bool
    10   exception STOP
    10   exception STOP of int
    11   exception EXIT of int
       
    12   val protocol_command: string -> (string list -> unit) -> unit
    11   val protocol_command: string -> (string list -> unit) -> unit
    13   val reset_tracing: Document_ID.exec -> unit
    12   val reset_tracing: Document_ID.exec -> unit
    14   val crashes: exn list Synchronized.var
    13   val crashes: exn list Synchronized.var
    15   val init_options: unit -> unit
    14   val init_options: unit -> unit
    16   val init_options_interactive: unit -> unit
    15   val init_options_interactive: unit -> unit
    34 val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
    33 val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
    35 
    34 
    36 
    35 
    37 (* protocol commands *)
    36 (* protocol commands *)
    38 
    37 
    39 exception STOP;
    38 exception STOP of int;
    40 exception EXIT of int;
    39 
    41 
    40 val is_protocol_exn = fn STOP _ => true | _ => false;
    42 val is_protocol_exn = fn STOP => true | EXIT _ => true | _ => false;
       
    43 
    41 
    44 local
    42 local
    45 
    43 
    46 val commands =
    44 val commands =
    47   Synchronized.var "Isabelle_Process.commands"
    45   Synchronized.var "Isabelle_Process.commands"
   189 
   187 
   190     fun protocol_loop () =
   188     fun protocol_loop () =
   191       let
   189       let
   192         val _ =
   190         val _ =
   193           (case Byte_Message.read_message in_stream of
   191           (case Byte_Message.read_message in_stream of
   194             NONE => raise STOP
   192             NONE => raise STOP 0
   195           | SOME [] => Output.system_message "Isabelle process: no input"
   193           | SOME [] => Output.system_message "Isabelle process: no input"
   196           | SOME (name :: args) => run_command name args)
   194           | SOME (name :: args) => run_command name args)
   197           handle exn =>
   195           handle exn =>
   198             if is_protocol_exn exn then Exn.reraise exn
   196             if is_protocol_exn exn then Exn.reraise exn
   199             else (Runtime.exn_system_message exn handle crash => recover crash);
   197             else (Runtime.exn_system_message exn handle crash => recover crash);
   215     val _ = BinIO.closeIn in_stream;
   213     val _ = BinIO.closeIn in_stream;
   216     val _ = BinIO.closeOut out_stream;
   214     val _ = BinIO.closeOut out_stream;
   217 
   215 
   218   in
   216   in
   219     (case result of
   217     (case result of
   220       Exn.Exn STOP => ()
   218       Exn.Exn (STOP rc) => if rc = 0 then () else exit rc
   221     | Exn.Exn (EXIT rc) => exit rc
       
   222     | _ => Exn.release result)
   219     | _ => Exn.release result)
   223   end);
   220   end);
   224 
   221 
   225 end;
   222 end;
   226 
   223