--- 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));