src/Pure/System/session.ML
changeset 32077 11f8ee55662d
parent 31898 82d5190ff7c8
child 32738 15bb09ca0378
equal deleted inserted replaced
32076:b54cb3acbbe4 32077:11f8ee55662d
     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 use_dir: string -> string -> bool -> string list -> bool -> bool ->
    12   val use_dir: string -> string -> bool -> string list -> bool -> bool ->
    13     string -> bool -> string list -> string -> string -> bool * string ->
    13     string -> bool -> string list -> string -> string -> bool * string ->
    14     string -> int -> bool -> bool -> int -> int -> bool -> unit
    14     string -> int -> bool -> bool -> int -> int -> int -> unit
    15   val finish: unit -> unit
    15   val finish: unit -> unit
    16 end;
    16 end;
    17 
    17 
    18 structure Session: SESSION =
    18 structure Session: SESSION =
    19 struct
    19 struct