# HG changeset patch
# User wenzelm
# Date 1414764531 -3600
# Node ID d659a12f9b7f1ea8b39fe6fd67158f741fca4822
# Parent  521cea5fa777c3a70b0faa2193ea33a08ecddeac
obsolete;

diff -r 521cea5fa777 -r d659a12f9b7f src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Fri Oct 31 11:36:41 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,227 +0,0 @@
-(*  Title:      Pure/Tools/proof_general_pure.ML
-    Author:     David Aspinall
-    Author:     Makarius
-
-Proof General setup within theory Pure.
-*)
-
-(*Proof General legacy*)
-
-structure ProofGeneral_Pure: sig end =
-struct
-
-(** preferences **)
-
-(* display *)
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_display
-    NONE
-    @{system_option show_types}
-    "show-types"
-    "Include types in display of Isabelle terms";
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_display
-    NONE
-    @{system_option show_sorts}
-    "show-sorts"
-    "Include sorts in display of Isabelle types";
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_display
-    NONE
-    @{system_option show_consts}
-    "show-consts"
-    "Show types of consts in Isabelle goal display";
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_display
-    NONE
-    @{system_option names_long}
-    "long-names"
-    "Show fully qualified names in Isabelle terms";
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_display
-    NONE
-    @{system_option show_brackets}
-    "show-brackets"
-    "Show full bracketing in Isabelle terms";
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_display
-    NONE
-    @{system_option show_main_goal}
-    "show-main-goal"
-    "Show main goal in proof state display";
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_display
-    NONE
-    @{system_option eta_contract}
-    "eta-contract"
-    "Print terms eta-contracted";
-
-
-(* advanced display *)
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_advanced_display
-    NONE
-    @{system_option goals_limit}
-    "goals-limit"
-    "Setting for maximum number of subgoals to be printed";
-
-val _ =
-  ProofGeneral.preference ProofGeneral.category_advanced_display
-    NONE
-    (Markup.print_int o get_default_print_depth)
-    (default_print_depth o Markup.parse_int)
-    ProofGeneral.pgipint
-    "print-depth"
-    "Setting for the ML print depth";
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_advanced_display
-    NONE
-    @{system_option show_question_marks}
-    "show-question-marks"
-    "Show leading question mark of variable name";
-
-
-(* tracing *)
-
-val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_tracing
-    NONE
-    Raw_Simplifier.simp_trace_default
-    "trace-simplifier"
-    "Trace simplification rules";
-
-val _ =
-  ProofGeneral.preference_int ProofGeneral.category_tracing
-    NONE
-    Raw_Simplifier.simp_trace_depth_limit_default
-    "trace-simplifier-depth"
-    "Trace simplifier depth limit";
-
-val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_tracing
-    NONE
-    Pattern.unify_trace_failure_default
-    "trace-unification"
-    "Output error diagnostics during unification";
-
-val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_tracing
-    NONE
-    Toplevel.timing
-    "global-timing"
-    "Whether to enable timing in Isabelle";
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_tracing
-    NONE
-    @{system_option ML_exception_trace}
-    "debugging"
-    "Whether to enable exception trace for toplevel command execution";
-
-val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_tracing
-    NONE
-    ProofGeneral.thm_deps
-    "theorem-dependencies"
-    "Track theorem dependencies within Proof General";
-
-
-(* proof *)
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_proof
-    (SOME "true")
-    @{system_option quick_and_dirty}
-    "quick-and-dirty"
-    "Take a few short cuts";
-
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_proof
-    NONE
-    @{system_option skip_proofs}
-    "skip-proofs"
-    "Skip over proofs";
-
-val _ =
-  ProofGeneral.preference ProofGeneral.category_proof
-    NONE
-    (Markup.print_bool o Proofterm.proofs_enabled)
-    (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 0))
-    ProofGeneral.pgipbool
-    "full-proofs"
-    "Record full proof objects internally";
-
-val _ =
-  ProofGeneral.preference ProofGeneral.category_proof
-    NONE
-    (Markup.print_int o Multithreading.max_threads_value)
-    (Multithreading.max_threads_update o Markup.parse_int)
-    ProofGeneral.pgipint
-    "max-threads"
-    "Maximum number of threads";
-
-val _ =
-  ProofGeneral.preference ProofGeneral.category_proof
-    NONE
-    (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
-    (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
-    ProofGeneral.pgipint
-    "parallel-proofs"
-    "Check proofs in parallel";
-
-
-
-(** command syntax **)
-
-val _ =
-  Outer_Syntax.improper_command
-    @{command_spec "ProofGeneral.process_pgip"} "(internal)"
-    (Parse.text >> (fn str => Toplevel.imperative (fn () => ProofGeneral.process_pgip str)));
-
-val _ =
-  Outer_Syntax.improper_command
-    @{command_spec "ProofGeneral.pr"} "(internal)"
-    (Scan.succeed (Toplevel.keep (fn state =>
-      if Toplevel.is_toplevel state orelse Toplevel.is_theory state
-      then ProofGeneral.tell_clear_goals ()
-      else (Toplevel.quiet := false; Toplevel.print_state state))));
-
-val _ = (*undo without output -- historical*)
-  Outer_Syntax.improper_command
-    @{command_spec "ProofGeneral.undo"} "(internal)"
-    (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
-
-val _ =
-  Outer_Syntax.improper_command
-    @{command_spec "ProofGeneral.restart"} "(internal)"
-    (Parse.opt_unit >> (K (Toplevel.imperative ProofGeneral.restart)));
-
-val _ =
-  Outer_Syntax.improper_command
-    @{command_spec "ProofGeneral.kill_proof"} "(internal)"
-    (Scan.succeed (Toplevel.imperative (fn () =>
-      (Isar.kill_proof (); ProofGeneral.tell_clear_goals ()))));
-
-val _ =
-  Outer_Syntax.improper_command
-    @{command_spec "ProofGeneral.inform_file_processed"} "(internal)"
-    (Parse.name >> (fn file => Toplevel.imperative (fn () =>
-      ProofGeneral.inform_file_processed file)));
-
-val _ =
-  Outer_Syntax.improper_command
-    @{command_spec "ProofGeneral.inform_file_retracted"} "(internal)"
-    (Parse.name >> (fn file => Toplevel.imperative (fn () =>
-      ProofGeneral.inform_file_retracted file)));
-
-end;
-