equal
deleted
inserted
replaced
982 val _ = (*Proof General legacy, e.g. for ProofGeneral-3.7.x*) |
982 val _ = (*Proof General legacy, e.g. for ProofGeneral-3.7.x*) |
983 Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)" |
983 Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)" |
984 (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) => |
984 (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) => |
985 Toplevel.keep (fn state => |
985 Toplevel.keep (fn state => |
986 (if Isabelle_Process.is_active () then error "Illegal TTY command" else (); |
986 (if Isabelle_Process.is_active () then error "Illegal TTY command" else (); |
987 case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n; |
987 case limit of NONE => () | SOME n => Options.default_put_int @{system_option goals_limit} n; |
988 Toplevel.quiet := false; |
988 Toplevel.quiet := false; |
989 Print_Mode.with_modes modes (Toplevel.print_state true) state)))); |
989 Print_Mode.with_modes modes (Toplevel.print_state true) state)))); |
990 |
990 |
991 val _ = (*Proof General legacy*) |
991 val _ = (*Proof General legacy*) |
992 Outer_Syntax.improper_command @{command_spec "disable_pr"} |
992 Outer_Syntax.improper_command @{command_spec "disable_pr"} |