--- a/src/Pure/Isar/isar_cmd.ML Sun Jun 13 15:28:46 2004 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Jun 13 15:30:08 2004 +0200
@@ -40,6 +40,8 @@
val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
val update_thy: string -> Toplevel.transition -> Toplevel.transition
val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
+ val display_drafts: string list -> Toplevel.transition -> Toplevel.transition
+ val print_drafts: string list -> Toplevel.transition -> Toplevel.transition
val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
val print_context: Toplevel.transition -> Toplevel.transition
val print_theory: Toplevel.transition -> Toplevel.transition
@@ -179,6 +181,17 @@
Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
+(* present draft files *)
+
+fun display_drafts files = Toplevel.imperative (fn () =>
+ let val outfile = File.quote_sysify_path (Present.drafts "dvi" (map Path.unpack files))
+ in system ("\"$ISATOOL\" display -c " ^ outfile ^ " &"); () end);
+
+fun print_drafts files = Toplevel.imperative (fn () =>
+ let val outfile = File.quote_sysify_path (Present.drafts "ps" (map Path.unpack files))
+ in system ("\"$ISATOOL\" print -c " ^ outfile); () end);
+
+
(* pretty_setmargin *)
fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);