# HG changeset patch # User wenzelm # Date 1414767825 -3600 # Node ID 98c03412079b6ec04beca6b7f62f23827b3c4c00 # Parent 8451eddc4d6727a346ae425839dc7a8f0d4d56eb discontinued Isar TTY loop; diff -r 8451eddc4d67 -r 98c03412079b NEWS --- 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. diff -r 8451eddc4d67 -r 98c03412079b bin/isabelle_process --- 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="$?" diff -r 8451eddc4d67 -r 98c03412079b src/Doc/System/Basics.thy --- 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 diff -r 8451eddc4d67 -r 98c03412079b src/Pure/General/secure.ML --- 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; diff -r 8451eddc4d67 -r 98c03412079b src/Pure/Isar/isar_syn.ML --- 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))))); diff -r 8451eddc4d67 -r 98c03412079b src/Pure/Pure.thy --- 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 == "" diff -r 8451eddc4d67 -r 98c03412079b src/Pure/ROOT --- 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" diff -r 8451eddc4d67 -r 98c03412079b src/Pure/ROOT.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 *) diff -r 8451eddc4d67 -r 98c03412079b src/Pure/System/isar.ML --- 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;