--- 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 ***
--- 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"
--- 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"
--- 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}
*}
--- 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 =
--- 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"}
--- 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
--- 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;