discontinued command 'print_drafts';
authorwenzelm
Sun Jul 07 18:34:29 2013 +0200 (2013-07-07 ago)
changeset 52549802576856527
parent 52548 a1a8248a4677
child 52550 09e52d4a850a
discontinued command 'print_drafts';
NEWS
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Doc/IsarRef/Document_Preparation.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/Thy/present.ML
     1.1 --- a/NEWS	Sun Jul 07 18:04:46 2013 +0200
     1.2 +++ b/NEWS	Sun Jul 07 18:34:29 2013 +0200
     1.3 @@ -36,6 +36,10 @@
     1.4  implicit change of some global references) is retained for now as
     1.5  control command, e.g. for ProofGeneral 3.7.x.
     1.6  
     1.7 +* Discontinued 'print_drafts' command with its old-fashioned PS output
     1.8 +and Unix command-line print spooling.  Minor INCOMPATIBILITY: use
     1.9 +'display_drafts' instead and print via the regular document viewer.
    1.10 +
    1.11  
    1.12  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.13  
     2.1 --- a/etc/isar-keywords-ZF.el	Sun Jul 07 18:04:46 2013 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Sun Jul 07 18:34:29 2013 +0200
     2.3 @@ -133,7 +133,6 @@
     2.4      "print_context"
     2.5      "print_defn_rules"
     2.6      "print_dependencies"
     2.7 -    "print_drafts"
     2.8      "print_facts"
     2.9      "print_induct_rules"
    2.10      "print_interps"
    2.11 @@ -302,7 +301,6 @@
    2.12      "print_context"
    2.13      "print_defn_rules"
    2.14      "print_dependencies"
    2.15 -    "print_drafts"
    2.16      "print_facts"
    2.17      "print_induct_rules"
    2.18      "print_interps"
     3.1 --- a/etc/isar-keywords.el	Sun Jul 07 18:04:46 2013 +0200
     3.2 +++ b/etc/isar-keywords.el	Sun Jul 07 18:34:29 2013 +0200
     3.3 @@ -188,7 +188,6 @@
     3.4      "print_context"
     3.5      "print_defn_rules"
     3.6      "print_dependencies"
     3.7 -    "print_drafts"
     3.8      "print_facts"
     3.9      "print_induct_rules"
    3.10      "print_inductives"
    3.11 @@ -417,7 +416,6 @@
    3.12      "print_context"
    3.13      "print_defn_rules"
    3.14      "print_dependencies"
    3.15 -    "print_drafts"
    3.16      "print_facts"
    3.17      "print_induct_rules"
    3.18      "print_inductives"
     4.1 --- a/src/Doc/IsarRef/Document_Preparation.thy	Sun Jul 07 18:04:46 2013 +0200
     4.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy	Sun Jul 07 18:34:29 2013 +0200
     4.3 @@ -554,21 +554,19 @@
     4.4  text {*
     4.5    \begin{matharray}{rcl}
     4.6      @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     4.7 -    @{command_def "print_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     4.8    \end{matharray}
     4.9  
    4.10    @{rail "
    4.11 -    (@@{command display_drafts} | @@{command print_drafts}) (@{syntax name} +)
    4.12 +    @@{command display_drafts} (@{syntax name} +)
    4.13  
    4.14    "}
    4.15  
    4.16    \begin{description}
    4.17  
    4.18 -  \item @{command "display_drafts"}~@{text paths} and @{command
    4.19 -  "print_drafts"}~@{text paths} perform simple output of a given list
    4.20 -  of raw source files.  Only those symbols that do not require
    4.21 -  additional {\LaTeX} packages are displayed properly, everything else
    4.22 -  is left verbatim.
    4.23 +  \item @{command "display_drafts"}~@{text paths} performs simple output of a
    4.24 +  given list of raw source files. Only those symbols that do not require
    4.25 +  additional {\LaTeX} packages are displayed properly, everything else is left
    4.26 +  verbatim.
    4.27  
    4.28    \end{description}
    4.29  *}
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Jul 07 18:04:46 2013 +0200
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Jul 07 18:34:29 2013 +0200
     5.3 @@ -39,8 +39,6 @@
     5.4    val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
     5.5    val diag_state: Proof.context -> Toplevel.state
     5.6    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
     5.7 -  val display_drafts: string list -> Toplevel.transition -> Toplevel.transition
     5.8 -  val print_drafts: string list -> Toplevel.transition -> Toplevel.transition
     5.9    val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
    5.10    val thy_deps: Toplevel.transition -> Toplevel.transition
    5.11    val locale_deps: Toplevel.transition -> Toplevel.transition
    5.12 @@ -275,21 +273,6 @@
    5.13        (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
    5.14  
    5.15  
    5.16 -(* present draft files *)
    5.17 -
    5.18 -fun display_drafts names = Toplevel.imperative (fn () =>
    5.19 -  let
    5.20 -    val paths = map Path.explode names;
    5.21 -    val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") paths);
    5.22 -  in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
    5.23 -
    5.24 -fun print_drafts names = Toplevel.imperative (fn () =>
    5.25 -  let
    5.26 -    val paths = map Path.explode names;
    5.27 -    val outfile = File.shell_path (Present.drafts "ps" paths);
    5.28 -  in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
    5.29 -
    5.30 -
    5.31  (* print theorems *)
    5.32  
    5.33  val print_theorems_proof =
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Jul 07 18:04:46 2013 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Jul 07 18:34:29 2013 +0200
     6.3 @@ -962,12 +962,8 @@
     6.4  val _ =
     6.5    Outer_Syntax.improper_command @{command_spec "display_drafts"}
     6.6      "display raw source files with symbols"
     6.7 -    (Scan.repeat1 Parse.path >> Isar_Cmd.display_drafts);
     6.8 -
     6.9 -val _ =
    6.10 -  Outer_Syntax.improper_command @{command_spec "print_drafts"}
    6.11 -    "print raw source files with symbols"
    6.12 -    (Scan.repeat1 Parse.path >> Isar_Cmd.print_drafts);
    6.13 +    (Scan.repeat1 Parse.path >> (fn names =>
    6.14 +      Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
    6.15  
    6.16  val _ =
    6.17    Outer_Syntax.improper_command @{command_spec "print_state"}
     7.1 --- a/src/Pure/Pure.thy	Sun Jul 07 18:04:46 2013 +0200
     7.2 +++ b/src/Pure/Pure.thy	Sun Jul 07 18:34:29 2013 +0200
     7.3 @@ -88,7 +88,7 @@
     7.4    and "cd" :: control
     7.5    and "pwd" :: diag
     7.6    and "use_thy" "remove_thy" "kill_thy" :: control
     7.7 -  and "display_drafts" "print_drafts" "print_state" "pr" :: diag
     7.8 +  and "display_drafts" "print_state" "pr" :: diag
     7.9    and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
    7.10    and "welcome" :: diag
    7.11    and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
     8.1 --- a/src/Pure/Thy/present.ML	Sun Jul 07 18:04:46 2013 +0200
     8.2 +++ b/src/Pure/Thy/present.ML	Sun Jul 07 18:34:29 2013 +0200
     8.3 @@ -21,7 +21,7 @@
     8.4    val theory_source: string -> (unit -> HTML.text) -> unit
     8.5    val theory_output: string -> string -> unit
     8.6    val begin_theory: int -> Path.T -> theory -> theory
     8.7 -  val drafts: string -> Path.T list -> Path.T
     8.8 +  val display_drafts: Path.T list -> int
     8.9  end;
    8.10  
    8.11  structure Present: PRESENT =
    8.12 @@ -450,8 +450,10 @@
    8.13  
    8.14  (** draft document output **)
    8.15  
    8.16 -fun drafts doc_format src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir =>
    8.17 +fun display_drafts src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir =>
    8.18    let
    8.19 +    val doc_format = getenv "ISABELLE_DOC_FORMAT";
    8.20 +
    8.21      fun prep_draft path i =
    8.22        let
    8.23          val base = Path.base path;
    8.24 @@ -487,9 +489,11 @@
    8.25  
    8.26      val result =
    8.27        isabelle_document {verbose = false, purge = true} doc_format documentN "" doc_path;
    8.28 -    val result' = Isabelle_System.create_tmp_path documentN doc_format;
    8.29 -    val _ = File.copy result result';
    8.30 -  in result' end);
    8.31 +    val detachable_result = Isabelle_System.create_tmp_path documentN doc_format;
    8.32 +    val _ = File.copy result detachable_result;
    8.33 +  in
    8.34 +    Isabelle_System.isabelle_tool "display" ("-c " ^ File.shell_path detachable_result ^ " &")
    8.35 +  end);
    8.36  
    8.37  end;
    8.38