--- a/NEWS Fri Oct 31 15:15:10 2014 +0100
+++ b/NEWS Fri Oct 31 16:03:45 2014 +0100
@@ -187,7 +187,8 @@
*** System ***
-* Proof General support has been discontinued. Minor INCOMPATIBILITY.
+* Support for Proof General and Isar TTY loop has been discontinued.
+Minor INCOMPATIBILITY.
* The Isabelle tool "update_cartouches" changes theory files to use
cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
--- a/bin/isabelle_process Fri Oct 31 15:15:10 2014 +0100
+++ b/bin/isabelle_process Fri Oct 31 16:03:45 2014 +0100
@@ -26,7 +26,6 @@
echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
echo
echo " Options are:"
- echo " -I startup Isar interaction mode"
echo " -O system options from given YXML file"
echo " -S secure mode -- disallow critical operations"
echo " -T ADDR startup process wrapper, with socket address"
@@ -57,7 +56,6 @@
# options
-ISAR=""
OPTIONS_FILE=""
SECURE=""
WRAPPER_SOCKET=""
@@ -69,12 +67,9 @@
READONLY=""
NOWRITE=""
-while getopts "IO:ST:W:e:m:o:qrw" OPT
+while getopts "O:ST:W:e:m:o:qrw" OPT
do
case "$OPT" in
- I)
- ISAR=true
- ;;
O)
OPTIONS_FILE="$OPTARG"
;;
@@ -208,8 +203,6 @@
[ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
-NICE="nice"
-
if [ -n "$WRAPPER_SOCKET" ]; then
MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
elif [ -n "$WRAPPER_FIFOS" ]; then
@@ -232,19 +225,14 @@
if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
fi
- if [ -n "$ISAR" ]; then
- MLTEXT="$MLTEXT; Isar.main ();"
- else
- NICE=""
- fi
fi
export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
- $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
+ "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
else
- $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
+ "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
fi
RC="$?"
--- a/src/Doc/System/Basics.thy Fri Oct 31 15:15:10 2014 +0100
+++ b/src/Doc/System/Basics.thy Fri Oct 31 16:03:45 2014 +0100
@@ -361,7 +361,6 @@
Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
Options are:
- -I startup Isar interaction mode
-O system options from given YXML file
-S secure mode -- disallow critical operations
-T ADDR startup process wrapper, with socket address
@@ -434,9 +433,6 @@
system options as a file in YXML format (according to the Isabelle/Scala
function @{verbatim isabelle.Options.encode}).
- \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
- interaction mode on startup, instead of the primitive ML top-level.
-
\medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
Isabelle enter a special process wrapper for interaction via
Isabelle/Scala, see also @{file
--- a/src/Pure/General/secure.ML Fri Oct 31 15:15:10 2014 +0100
+++ b/src/Pure/General/secure.ML Fri Oct 31 16:03:45 2014 +0100
@@ -13,7 +13,6 @@
val use_text: use_context -> int * string -> bool -> string -> unit
val use_file: use_context -> bool -> string -> unit
val toplevel_pp: string list -> string -> unit
- val commit: unit -> unit
end;
structure Secure: SECURE =
@@ -32,8 +31,6 @@
(** critical operations **)
-(* ML evaluation *)
-
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
val raw_use_text = use_text;
@@ -45,12 +42,5 @@
fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
-
-(* global evaluation *)
-
-val use_global = raw_use_text ML_Parse.global_context (0, "") false;
-
-fun commit () = use_global "commit();"; (*commit is dynamically bound!*)
-
end;
--- a/src/Pure/Isar/isar_syn.ML Fri Oct 31 15:15:10 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Oct 31 16:03:45 2014 +0100
@@ -919,84 +919,20 @@
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
-
-
-(** system commands (for interactive mode only) **)
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
- (Parse.position Parse.name >>
- (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "remove_thy"} "remove theory from loader database"
- (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "kill_thy"}
- "kill theory -- try to remove from loader database"
- (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "display_drafts"}
- "display raw source files with symbols"
- (Scan.repeat1 Parse.path >> (fn names =>
- Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
-
val _ =
Outer_Syntax.improper_command @{command_spec "print_state"}
"print current proof state (if present)"
(opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
val _ =
- Outer_Syntax.improper_command @{command_spec "commit"}
- "commit current session to ML session image"
- (Parse.opt_unit >> K (Toplevel.imperative Secure.commit));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle process"
- (Parse.opt_unit >> (K (Toplevel.imperative quit)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "exit"} "exit Isar loop"
- (Scan.succeed
- (Toplevel.keep (fn state =>
- (Context.set_thread_data (try Toplevel.generic_theory_of state);
- raise Runtime.TERMINATE))));
-
-val _ =
Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
(Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
-
-
-(** raw Isar read-eval-print loop **)
-
val _ =
- Outer_Syntax.improper_command @{command_spec "init_toplevel"} "init toplevel point-of-interest"
- (Scan.succeed (Toplevel.imperative Isar.init));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "linear_undo"} "undo commands"
- (Scan.optional Parse.nat 1 >>
- (fn n => Toplevel.imperative (fn () => Isar.linear_undo n)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "undo"} "undo commands (skipping closed proofs)"
- (Scan.optional Parse.nat 1 >>
- (fn n => Toplevel.imperative (fn () => Isar.undo n)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "undos_proof"}
- "undo commands (skipping closed proofs)"
- (Scan.optional Parse.nat 1 >> (fn n =>
- Toplevel.keep (fn state =>
- if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "kill"}
- "kill partial proof or theory development"
- (Scan.succeed (Toplevel.imperative Isar.kill));
+ Outer_Syntax.improper_command @{command_spec "display_drafts"}
+ "display raw source files with symbols"
+ (Scan.repeat1 Parse.path >> (fn names =>
+ Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
--- a/src/Pure/Pure.thy Fri Oct 31 15:15:10 2014 +0100
+++ b/src/Pure/Pure.thy Fri Oct 31 16:03:45 2014 +0100
@@ -88,11 +88,8 @@
"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" :: diag
- and "commit" "quit" "exit" :: control
and "welcome" :: diag
- and "init_toplevel" "linear_undo" "undo" "undos_proof" "kill" :: control
and "end" :: thy_end % "theory"
and "realizers" :: thy_decl == ""
and "realizability" :: thy_decl == ""
--- a/src/Pure/ROOT Fri Oct 31 15:15:10 2014 +0100
+++ b/src/Pure/ROOT Fri Oct 31 16:03:45 2014 +0100
@@ -196,7 +196,6 @@
"System/invoke_scala.ML"
"System/isabelle_process.ML"
"System/isabelle_system.ML"
- "System/isar.ML"
"System/message_channel.ML"
"System/options.ML"
"System/system_channel.ML"
--- a/src/Pure/ROOT.ML Fri Oct 31 15:15:10 2014 +0100
+++ b/src/Pure/ROOT.ML Fri Oct 31 16:03:45 2014 +0100
@@ -327,7 +327,6 @@
use "System/isabelle_process.ML";
use "System/invoke_scala.ML";
use "PIDE/protocol.ML";
-use "System/isar.ML";
(* miscellaneous tools and packages for Pure Isabelle *)
--- a/src/Pure/System/isar.ML Fri Oct 31 15:15:10 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,174 +0,0 @@
-(* Title: Pure/System/isar.ML
- Author: Makarius
-
-Global state of the raw Isar read-eval-print loop.
-*)
-
-signature ISAR =
-sig
- val init: unit -> unit
- val exn: unit -> (exn * string) option
- val state: unit -> Toplevel.state
- val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
- val print: unit -> unit
- val >> : Toplevel.transition -> bool
- val >>> : Toplevel.transition list -> unit
- val linear_undo: int -> unit
- val undo: int -> unit
- val kill: unit -> unit
- val kill_proof: unit -> unit
- val crashes: exn list Synchronized.var
- val toplevel_loop: TextIO.instream ->
- {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
- val loop: unit -> unit
- val main: unit -> unit
-end;
-
-structure Isar: ISAR =
-struct
-
-
-(** TTY model -- SINGLE-THREADED! **)
-
-(* the global state *)
-
-type history = (Toplevel.state * Toplevel.transition) list;
- (*previous state, state transition -- regular commands only*)
-
-local
- val global_history = Unsynchronized.ref ([]: history);
- val global_state = Unsynchronized.ref Toplevel.toplevel;
- val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
-in
-
-fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
- let
- fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
- | edit n (st, hist) = edit (n - 1) (f st hist);
- in edit count (! global_state, ! global_history) end);
-
-fun state () = ! global_state;
-
-fun exn () = ! global_exn;
-fun set_exn exn = global_exn := exn;
-
-end;
-
-
-fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
-
-fun goal () = Proof.goal (Toplevel.proof_of (state ()))
- handle Toplevel.UNDEF => error "No goal present";
-
-fun print () = Toplevel.print_state (state ());
-
-
-(* history navigation *)
-
-local
-
-fun find_and_undo _ [] = error "Undo history exhausted"
- | find_and_undo which ((prev, tr) :: hist) =
- if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist;
-
-in
-
-fun linear_undo n = edit_history n (K (find_and_undo (K true)));
-
-fun undo n = edit_history n (fn st => fn hist =>
- find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);
-
-fun kill () = edit_history 1 (fn st => fn hist =>
- find_and_undo
- (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);
-
-fun kill_proof () = edit_history 1 (fn st => fn hist =>
- if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist
- else raise Toplevel.UNDEF);
-
-end;
-
-
-(* interactive state transformations *)
-
-fun op >> tr =
- (case Toplevel.transition true tr (state ()) of
- NONE => false
- | SOME (_, SOME exn_info) =>
- (set_exn (SOME exn_info);
- Toplevel.setmp_thread_position tr
- Runtime.exn_error_message (Runtime.EXCURSION_FAIL exn_info);
- true)
- | SOME (st', NONE) =>
- let
- val name = Toplevel.name_of tr;
- val _ = if Keyword.is_theory_begin name then init () else ();
- val _ =
- if Keyword.is_regular name
- then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
- in true end);
-
-fun op >>> [] = ()
- | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
-
-
-(* toplevel loop -- uninterruptible *)
-
-val crashes = Synchronized.var "Isar.crashes" ([]: exn list);
-
-local
-
-fun protocol_message props output =
- (case props of
- function :: args =>
- if function = Markup.command_timing then
- let
- val name = the_default "" (Properties.get args Markup.nameN);
- val pos = Position.of_properties args;
- val timing = Markup.parse_timing_properties args;
- in
- if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing)
- andalso name <> "" andalso not (Keyword.is_control name)
- then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing)
- else ()
- end
- else raise Output.Protocol_Message props
- | [] => raise Output.Protocol_Message props);
-
-fun raw_loop secure src =
- let
- fun check_secure () =
- (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
- in
- (case Source.get_single (Source.set_prompt Source.default_prompt src) of
- NONE => if secure then quit () else ()
- | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
- handle exn =>
- (Runtime.exn_error_message exn
- handle crash =>
- (Synchronized.change crashes (cons crash);
- warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
- raw_loop secure src)
- end;
-
-in
-
-fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
- (Context.set_thread_data NONE;
- Multithreading.max_threads_update (Options.default_int "threads");
- if do_init then init () else ();
- Output.protocol_message_fn := protocol_message;
- if welcome then writeln (Session.welcome ()) else ();
- uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
-
-end;
-
-fun loop () =
- toplevel_loop TextIO.stdIn
- {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
-
-fun main () =
- toplevel_loop TextIO.stdIn
- {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
-
-end;