src/Pure/Isar/isar_cmd.ML
changeset 52549 802576856527
parent 52143 36ffe23b25f8
child 53171 a5e54d4d9081
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Jul 07 18:04:46 2013 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Jul 07 18:34:29 2013 +0200
     1.3 @@ -39,8 +39,6 @@
     1.4    val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
     1.5    val diag_state: Proof.context -> Toplevel.state
     1.6    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
     1.7 -  val display_drafts: string list -> Toplevel.transition -> Toplevel.transition
     1.8 -  val print_drafts: string list -> Toplevel.transition -> Toplevel.transition
     1.9    val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
    1.10    val thy_deps: Toplevel.transition -> Toplevel.transition
    1.11    val locale_deps: Toplevel.transition -> Toplevel.transition
    1.12 @@ -275,21 +273,6 @@
    1.13        (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
    1.14  
    1.15  
    1.16 -(* present draft files *)
    1.17 -
    1.18 -fun display_drafts names = Toplevel.imperative (fn () =>
    1.19 -  let
    1.20 -    val paths = map Path.explode names;
    1.21 -    val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") paths);
    1.22 -  in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
    1.23 -
    1.24 -fun print_drafts names = Toplevel.imperative (fn () =>
    1.25 -  let
    1.26 -    val paths = map Path.explode names;
    1.27 -    val outfile = File.shell_path (Present.drafts "ps" paths);
    1.28 -  in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
    1.29 -
    1.30 -
    1.31  (* print theorems *)
    1.32  
    1.33  val print_theorems_proof =