# HG changeset patch
# User wenzelm
# Date 1373214869 -7200
# Node ID 80257685652722a490f2e52cb8f961f6c942e916
# Parent  a1a8248a4677f076fe74a5ed147bcc9548d7dc9b
discontinued command 'print_drafts';

diff -r a1a8248a4677 -r 802576856527 NEWS
--- a/NEWS	Sun Jul 07 18:04:46 2013 +0200
+++ b/NEWS	Sun Jul 07 18:34:29 2013 +0200
@@ -36,6 +36,10 @@
 implicit change of some global references) is retained for now as
 control command, e.g. for ProofGeneral 3.7.x.
 
+* Discontinued 'print_drafts' command with its old-fashioned PS output
+and Unix command-line print spooling.  Minor INCOMPATIBILITY: use
+'display_drafts' instead and print via the regular document viewer.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r a1a8248a4677 -r 802576856527 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sun Jul 07 18:04:46 2013 +0200
+++ b/etc/isar-keywords-ZF.el	Sun Jul 07 18:34:29 2013 +0200
@@ -133,7 +133,6 @@
     "print_context"
     "print_defn_rules"
     "print_dependencies"
-    "print_drafts"
     "print_facts"
     "print_induct_rules"
     "print_interps"
@@ -302,7 +301,6 @@
     "print_context"
     "print_defn_rules"
     "print_dependencies"
-    "print_drafts"
     "print_facts"
     "print_induct_rules"
     "print_interps"
diff -r a1a8248a4677 -r 802576856527 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sun Jul 07 18:04:46 2013 +0200
+++ b/etc/isar-keywords.el	Sun Jul 07 18:34:29 2013 +0200
@@ -188,7 +188,6 @@
     "print_context"
     "print_defn_rules"
     "print_dependencies"
-    "print_drafts"
     "print_facts"
     "print_induct_rules"
     "print_inductives"
@@ -417,7 +416,6 @@
     "print_context"
     "print_defn_rules"
     "print_dependencies"
-    "print_drafts"
     "print_facts"
     "print_induct_rules"
     "print_inductives"
diff -r a1a8248a4677 -r 802576856527 src/Doc/IsarRef/Document_Preparation.thy
--- a/src/Doc/IsarRef/Document_Preparation.thy	Sun Jul 07 18:04:46 2013 +0200
+++ b/src/Doc/IsarRef/Document_Preparation.thy	Sun Jul 07 18:34:29 2013 +0200
@@ -554,21 +554,19 @@
 text {*
   \begin{matharray}{rcl}
     @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
-    @{command_def "print_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
   \end{matharray}
 
   @{rail "
-    (@@{command display_drafts} | @@{command print_drafts}) (@{syntax name} +)
+    @@{command display_drafts} (@{syntax name} +)
 
   "}
 
   \begin{description}
 
-  \item @{command "display_drafts"}~@{text paths} and @{command
-  "print_drafts"}~@{text paths} perform simple output of a given list
-  of raw source files.  Only those symbols that do not require
-  additional {\LaTeX} packages are displayed properly, everything else
-  is left verbatim.
+  \item @{command "display_drafts"}~@{text paths} performs simple output of a
+  given list of raw source files. Only those symbols that do not require
+  additional {\LaTeX} packages are displayed properly, everything else is left
+  verbatim.
 
   \end{description}
 *}
diff -r a1a8248a4677 -r 802576856527 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Jul 07 18:04:46 2013 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Jul 07 18:34:29 2013 +0200
@@ -39,8 +39,6 @@
   val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
   val diag_state: Proof.context -> Toplevel.state
   val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
-  val display_drafts: string list -> Toplevel.transition -> Toplevel.transition
-  val print_drafts: string list -> Toplevel.transition -> Toplevel.transition
   val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
   val thy_deps: Toplevel.transition -> Toplevel.transition
   val locale_deps: Toplevel.transition -> Toplevel.transition
@@ -275,21 +273,6 @@
       (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
 
 
-(* present draft files *)
-
-fun display_drafts names = Toplevel.imperative (fn () =>
-  let
-    val paths = map Path.explode names;
-    val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") paths);
-  in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
-
-fun print_drafts names = Toplevel.imperative (fn () =>
-  let
-    val paths = map Path.explode names;
-    val outfile = File.shell_path (Present.drafts "ps" paths);
-  in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
-
-
 (* print theorems *)
 
 val print_theorems_proof =
diff -r a1a8248a4677 -r 802576856527 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Jul 07 18:04:46 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Jul 07 18:34:29 2013 +0200
@@ -962,12 +962,8 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "display_drafts"}
     "display raw source files with symbols"
-    (Scan.repeat1 Parse.path >> Isar_Cmd.display_drafts);
-
-val _ =
-  Outer_Syntax.improper_command @{command_spec "print_drafts"}
-    "print raw source files with symbols"
-    (Scan.repeat1 Parse.path >> Isar_Cmd.print_drafts);
+    (Scan.repeat1 Parse.path >> (fn names =>
+      Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_state"}
diff -r a1a8248a4677 -r 802576856527 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Jul 07 18:04:46 2013 +0200
+++ b/src/Pure/Pure.thy	Sun Jul 07 18:34:29 2013 +0200
@@ -88,7 +88,7 @@
   and "cd" :: control
   and "pwd" :: diag
   and "use_thy" "remove_thy" "kill_thy" :: control
-  and "display_drafts" "print_drafts" "print_state" "pr" :: diag
+  and "display_drafts" "print_state" "pr" :: diag
   and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
   and "welcome" :: diag
   and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
diff -r a1a8248a4677 -r 802576856527 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Jul 07 18:04:46 2013 +0200
+++ b/src/Pure/Thy/present.ML	Sun Jul 07 18:34:29 2013 +0200
@@ -21,7 +21,7 @@
   val theory_source: string -> (unit -> HTML.text) -> unit
   val theory_output: string -> string -> unit
   val begin_theory: int -> Path.T -> theory -> theory
-  val drafts: string -> Path.T list -> Path.T
+  val display_drafts: Path.T list -> int
 end;
 
 structure Present: PRESENT =
@@ -450,8 +450,10 @@
 
 (** draft document output **)
 
-fun drafts doc_format src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir =>
+fun display_drafts src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir =>
   let
+    val doc_format = getenv "ISABELLE_DOC_FORMAT";
+
     fun prep_draft path i =
       let
         val base = Path.base path;
@@ -487,9 +489,11 @@
 
     val result =
       isabelle_document {verbose = false, purge = true} doc_format documentN "" doc_path;
-    val result' = Isabelle_System.create_tmp_path documentN doc_format;
-    val _ = File.copy result result';
-  in result' end);
+    val detachable_result = Isabelle_System.create_tmp_path documentN doc_format;
+    val _ = File.copy result detachable_result;
+  in
+    Isabelle_System.isabelle_tool "display" ("-c " ^ File.shell_path detachable_result ^ " &")
+  end);
 
 end;