# HG changeset patch
# User wenzelm
# Date 1414764910 -3600
# Node ID 8451eddc4d6727a346ae425839dc7a8f0d4d56eb
# Parent  d659a12f9b7f1ea8b39fe6fd67158f741fca4822
removed obsolete Proof General commands;

diff -r d659a12f9b7f -r 8451eddc4d67 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Oct 31 15:08:51 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Oct 31 15:15:10 2014 +0100
@@ -734,23 +734,6 @@
 
 
 
-(** nested commands **)
-
-val props_text =
-  Scan.optional Parse.properties [] -- Parse.position Parse.string
-  >> (fn (props, (str, pos)) =>
-      (Position.of_properties (Position.default_properties pos props), str));
-
-val _ =
-  Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command"
-    (props_text :|-- (fn (pos, str) =>
-      (case Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos str of
-        [tr] => Scan.succeed (K tr)
-      | _ => Scan.fail_with (K (fn () => "exactly one command expected")))
-      handle ERROR msg => Scan.fail_with (K (fn () => msg))));
-
-
-
 (** diagnostic commands (for interactive mode only) **)
 
 val opt_modes =
@@ -758,11 +741,6 @@
 
 val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
 
-val _ = (*Proof General legacy*)
-  Outer_Syntax.improper_command @{command_spec "pretty_setmargin"}
-    "change default margin for pretty printing"
-    (Parse.nat >> (fn n => Toplevel.imperative (fn () => Pretty.margin_default := n)));
-
 val _ =
   Outer_Syntax.improper_command @{command_spec "help"}
     "retrieve outer syntax commands according to name patterns"
@@ -890,13 +868,6 @@
     (Scan.succeed Isar_Cmd.locale_deps);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_binds"}
-    "print term bindings of proof context -- Proof General legacy"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep
-        (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
-
-val _ =
   Outer_Syntax.improper_command @{command_spec "print_term_bindings"}
     "print term bindings of proof context"
     (Scan.succeed (Toplevel.unknown_context o
@@ -966,7 +937,7 @@
     "kill theory -- try to remove from loader database"
     (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
 
-val _ = (*partial Proof General legacy*)
+val _ =
   Outer_Syntax.improper_command @{command_spec "display_drafts"}
     "display raw source files with symbols"
     (Scan.repeat1 Parse.path >> (fn names =>
@@ -977,25 +948,6 @@
     "print current proof state (if present)"
     (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
 
-val _ = (*Proof General legacy, e.g. for ProofGeneral-3.7.x*)
-  Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
-    (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
-      Toplevel.keep (fn state =>
-       (if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
-        case limit of NONE => () | SOME n => Options.default_put_int @{system_option goals_limit} n;
-        Toplevel.quiet := false;
-        Print_Mode.with_modes modes Toplevel.print_state state))));
-
-val _ = (*Proof General legacy*)
-  Outer_Syntax.improper_command @{command_spec "disable_pr"}
-    "disable printing of toplevel state"
-    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
-
-val _ = (*Proof General legacy*)
-  Outer_Syntax.improper_command @{command_spec "enable_pr"}
-    "enable printing of toplevel state"
-    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
-
 val _ =
   Outer_Syntax.improper_command @{command_spec "commit"}
     "commit current session to ML session image"
@@ -1042,13 +994,6 @@
         if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "cannot_undo"}
-    "partial undo -- Proof General legacy"
-    (Parse.name >>
-      (fn "end" => Toplevel.imperative (fn () => Isar.undo 1)
-        | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
-
-val _ =
   Outer_Syntax.improper_command @{command_spec "kill"}
     "kill partial proof or theory development"
     (Scan.succeed (Toplevel.imperative Isar.kill));
diff -r d659a12f9b7f -r 8451eddc4d67 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Oct 31 15:08:51 2014 +0100
+++ b/src/Pure/Pure.thy	Fri Oct 31 15:15:10 2014 +0100
@@ -79,21 +79,20 @@
   and "also" "moreover" :: prf_decl % "proof"
   and "finally" "ultimately" :: prf_chain % "proof"
   and "back" :: prf_script % "proof"
-  and "Isabelle.command" :: control
   and "help" "print_commands" "print_options" "print_context"
     "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
     "print_theorems" "print_locales" "print_classes" "print_locale"
     "print_interps" "print_dependencies" "print_attributes"
     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
     "print_antiquotations" "print_ML_antiquotations" "thy_deps"
-    "locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings"
+    "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
     "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
     "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
   and "use_thy" "remove_thy" "kill_thy" :: control
-  and "display_drafts" "print_state" "pr" :: diag
-  and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
+  and "display_drafts" "print_state" :: diag
+  and "commit" "quit" "exit" :: control
   and "welcome" :: diag
-  and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
+  and "init_toplevel" "linear_undo" "undo" "undos_proof" "kill" :: control
   and "end" :: thy_end % "theory"
   and "realizers" :: thy_decl == ""
   and "realizability" :: thy_decl == ""