# HG changeset patch
# User berghofe
# Date 1105449390 -3600
# Node ID a2cbdf16832ea44ae306a2170973811a6936d19e
# Parent  f04179b1454beede6e6e615765dcb50351408a26
Added flag for hiding proofs in documents to use_dir.

diff -r f04179b1454b -r a2cbdf16832e src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Tue Jan 11 14:15:14 2005 +0100
+++ b/src/Pure/Isar/session.ML	Tue Jan 11 14:16:30 2005 +0100
@@ -10,7 +10,7 @@
   val name: unit -> string
   val welcome: unit -> string
   val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string
-    -> string -> string -> string -> int -> bool -> unit
+    -> string -> string -> string -> int -> bool -> bool -> unit
   val finish: unit -> unit
 end;
 
@@ -79,14 +79,14 @@
        rpath := Some (Url.unpack rpath_str);
    (!rpath, rpath_str <> ""));
 
-fun use_dir root_file build modes reset info doc doc_graph parent name dump rpath_str level verbose =
+fun use_dir root_file build modes reset info doc doc_graph parent name dump rpath_str level verbose hide =
   Library.setmp print_mode (modes @ ! print_mode)
-    (Library.setmp Proofterm.proofs level (fn () =>
+    (Library.setmp Proofterm.proofs level (Library.setmp IsarOutput.hide_commands hide (fn () =>
       (init reset parent name;
        Present.init build info doc doc_graph (path ()) name
          (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose;
        File.use (Path.basic root_file);
-       finish ()))) ()
+       finish ())))) ()
   handle exn => (writeln (Toplevel.exn_message exn); exit 1);