src/Pure/Isar/session.ML
changeset 10571 fdde440a9033
parent 9414 1463576f3968
child 10937 5651e0636e38
equal deleted inserted replaced
10570:fc7afc98a329 10571:fdde440a9033
     7 *)
     7 *)
     8 
     8 
     9 signature SESSION =
     9 signature SESSION =
    10 sig
    10 sig
    11   val welcome: unit -> string
    11   val welcome: unit -> string
    12   val use_dir: bool -> bool -> string -> string -> string -> string -> string -> unit
    12   val use_dir:
       
    13     string list -> bool -> bool -> string -> string -> string -> string -> string -> unit
    13   val finish: unit -> unit
    14   val finish: unit -> unit
    14 end;
    15 end;
    15 
    16 
    16 structure Session: SESSION =
    17 structure Session: SESSION =
    17 struct
    18 struct
    73        error "Path for remote theory browsing information may only be set once"
    74        error "Path for remote theory browsing information may only be set once"
    74      else
    75      else
    75        rpath := Some (Url.unpack rpath_str);
    76        rpath := Some (Url.unpack rpath_str);
    76    (!rpath, rpath_str <> ""));
    77    (!rpath, rpath_str <> ""));
    77 
    78 
    78 fun use_dir reset info doc parent name dump rpath_str =
    79 fun use_dir modes reset info doc parent name dump rpath_str =
    79   (init reset parent name;
    80   Library.setmp print_mode (modes @ ! print_mode) (fn () =>
    80    Present.init info doc (path ()) name
    81     (init reset parent name;
    81      (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str);
    82      Present.init info doc (path ()) name
    82    File.symbol_use root_file;
    83        (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str);
    83    finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    84      File.symbol_use root_file;
       
    85      finish ())) ()
       
    86   handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    84 
    87 
    85 
    88 
    86 end;
    89 end;