# HG changeset patch
# User wenzelm
# Date 1087133408 -7200
# Node ID bf9f525d4821a25b9ce86058caa3007aef98b7d1
# Parent  3fd8c03e3ee66cf81c9110ff8f2bebd2fe6b8dce
added display_drafts and print_drafts commands;

diff -r 3fd8c03e3ee6 -r bf9f525d4821 NEWS
--- a/NEWS	Sun Jun 13 15:28:46 2004 +0200
+++ b/NEWS	Sun Jun 13 15:30:08 2004 +0200
@@ -54,6 +54,14 @@
   and printing the subsequent argument, as in @{thm [locale=LC]
   fold_commute}, for example.
 
+* Document preparation: commands 'display_drafts' and 'print_drafts'
+  perform simple output of raw sources.  Only those symbols that do
+  not require additional LaTeX packages (depending on comments in
+  isabellesym.sty) are displayed properly, everything else is left
+  verbatim.  We use isatool display and isatool print as front ends;
+  these are subject to the DVI_VIEWER and PRINT_COMMAND settings,
+  respectively.
+
 * ML: output via the Isabelle channels of writeln/warning/error
   etc. is now passed through Output.output, with a hook for arbitrary
   transformations depending on the print_mode (cf. Output.add_mode --
diff -r 3fd8c03e3ee6 -r bf9f525d4821 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sun Jun 13 15:28:46 2004 +0200
+++ b/doc-src/IsarRef/pure.tex	Sun Jun 13 15:30:08 2004 +0200
@@ -1507,7 +1507,8 @@
 \subsection{System operations}
 
 \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
-\indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
+\indexisarcmd{update-thy}\indexisarcmd{update-thy-only}\indexisarcmd{display-drafts}
+\indexisarcmd{print-drafts}
 \begin{matharray}{rcl}
   \isarcmd{cd}^* & : & \isarkeep{\cdot} \\
   \isarcmd{pwd}^* & : & \isarkeep{\cdot} \\
@@ -1515,6 +1516,8 @@
   \isarcmd{use_thy_only}^* & : & \isarkeep{\cdot} \\
   \isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\
   \isarcmd{update_thy_only}^* & : & \isarkeep{\cdot} \\
+  \isarcmd{display_drafts}^* & : & \isarkeep{\cdot} \\
+  \isarcmd{print_drafts}^* & : & \isarkeep{\cdot} \\
 \end{matharray}
 
 \begin{descr}
@@ -1528,6 +1531,10 @@
     implicit theory context to that of the theory loaded.}  (see also
   \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar versions may
   load new- and old-style theories alike.
+\item [$\isarkeyword{display_drafts} and \isarkeyword{print_drafts}$] perform
+  simple output of a given list of raw source files (specified as repeated
+  $name$ arguments).  Only those symbols that do not require additional LaTeX
+  packages are displayed properly, everything else is left verbatim.
 \end{descr}
 
 These system commands are scarcely used when working with the Proof~General
diff -r 3fd8c03e3ee6 -r bf9f525d4821 src/Pure/Isar/isar_cmd.ML
--- 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);
diff -r 3fd8c03e3ee6 -r bf9f525d4821 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Jun 13 15:28:46 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Jun 13 15:30:08 2004 +0200
@@ -703,6 +703,14 @@
   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
 
+val display_draftsP =
+  OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
+    K.diag (Scan.repeat1 P.name >> (Toplevel.no_timing oo IsarCmd.display_drafts));
+
+val print_draftsP =
+  OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
+    K.diag (Scan.repeat1 P.name >> (Toplevel.no_timing oo IsarCmd.print_drafts));
+
 val opt_limits =
   Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
 
@@ -787,8 +795,8 @@
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
-  kill_thyP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
-  init_toplevelP, welcomeP];
+  kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
+  enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
 
 end;