src/Pure/System/session.ML
changeset 49433 1a634f9614fb
parent 47841 9667e0dcb5e2
child 49460 cb4136e4cabf
equal deleted inserted replaced
49432:bb1d4ec90f30 49433:1a634f9614fb
     7 signature SESSION =
     7 signature SESSION =
     8 sig
     8 sig
     9   val id: unit -> string list
     9   val id: unit -> string list
    10   val name: unit -> string
    10   val name: unit -> string
    11   val welcome: unit -> string
    11   val welcome: unit -> string
       
    12   val init: bool -> string -> string -> unit
    12   val use_dir: string -> string -> bool -> string list -> bool -> bool ->
    13   val use_dir: string -> string -> bool -> string list -> bool -> bool ->
    13     string -> bool -> string list -> string -> string -> bool * string ->
    14     string -> bool -> string list -> string -> string -> bool * string ->
    14     string -> int -> bool -> bool -> int -> int -> int -> int -> unit
    15     string -> int -> bool -> bool -> int -> int -> int -> int -> unit
    15   val finish: unit -> unit
    16   val finish: unit -> unit
    16 end;
    17 end;