# HG changeset patch # User wenzelm # Date 1003602100 -7200 # Node ID 56bc01962cf266155fa2a19491bc3c89e9ddc2ec # Parent 651650b717e10e05e42fadcafa071365e8c4ed65 document graph option; diff -r 651650b717e1 -r 56bc01962cf2 src/Pure/Isar/session.ML --- a/src/Pure/Isar/session.ML Sat Oct 20 20:21:14 2001 +0200 +++ b/src/Pure/Isar/session.ML Sat Oct 20 20:21:40 2001 +0200 @@ -10,7 +10,7 @@ sig val name: unit -> string val welcome: unit -> string - val use_dir: string list -> bool -> bool -> string -> string + val use_dir: string list -> bool -> bool -> string -> bool -> string -> string -> string -> string -> int -> bool -> unit val finish: unit -> unit end; @@ -78,11 +78,11 @@ rpath := Some (Url.unpack rpath_str); (!rpath, rpath_str <> "")); -fun use_dir modes reset info doc parent name dump rpath_str level verbose = +fun use_dir modes reset info doc doc_graph parent name dump rpath_str level verbose = Library.setmp print_mode (modes @ ! print_mode) (Library.setmp Proofterm.proofs level (fn () => (init reset parent name; - Present.init info doc (path ()) name + Present.init info doc doc_graph (path ()) name (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose; File.symbol_use root_file; finish ()))) ()