discontinued Isar TTY loop;
authorwenzelm
Fri Oct 31 16:03:45 2014 +0100 (2014-10-31)
changeset 5884698c03412079b
parent 58845 8451eddc4d67
child 58847 c44aff8ac894
discontinued Isar TTY loop;
NEWS
bin/isabelle_process
src/Doc/System/Basics.thy
src/Pure/General/secure.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/isar.ML
     1.1 --- a/NEWS	Fri Oct 31 15:15:10 2014 +0100
     1.2 +++ b/NEWS	Fri Oct 31 16:03:45 2014 +0100
     1.3 @@ -187,7 +187,8 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 -* Proof General support has been discontinued.  Minor INCOMPATIBILITY.
     1.8 +* Support for Proof General and Isar TTY loop has been discontinued.
     1.9 +Minor INCOMPATIBILITY.
    1.10  
    1.11  * The Isabelle tool "update_cartouches" changes theory files to use
    1.12  cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
     2.1 --- a/bin/isabelle_process	Fri Oct 31 15:15:10 2014 +0100
     2.2 +++ b/bin/isabelle_process	Fri Oct 31 16:03:45 2014 +0100
     2.3 @@ -26,7 +26,6 @@
     2.4    echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
     2.5    echo
     2.6    echo "  Options are:"
     2.7 -  echo "    -I           startup Isar interaction mode"
     2.8    echo "    -O           system options from given YXML file"
     2.9    echo "    -S           secure mode -- disallow critical operations"
    2.10    echo "    -T ADDR      startup process wrapper, with socket address"
    2.11 @@ -57,7 +56,6 @@
    2.12  
    2.13  # options
    2.14  
    2.15 -ISAR=""
    2.16  OPTIONS_FILE=""
    2.17  SECURE=""
    2.18  WRAPPER_SOCKET=""
    2.19 @@ -69,12 +67,9 @@
    2.20  READONLY=""
    2.21  NOWRITE=""
    2.22  
    2.23 -while getopts "IO:ST:W:e:m:o:qrw" OPT
    2.24 +while getopts "O:ST:W:e:m:o:qrw" OPT
    2.25  do
    2.26    case "$OPT" in
    2.27 -    I)
    2.28 -      ISAR=true
    2.29 -      ;;
    2.30      O)
    2.31        OPTIONS_FILE="$OPTARG"
    2.32        ;;
    2.33 @@ -208,8 +203,6 @@
    2.34  
    2.35  [ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
    2.36  
    2.37 -NICE="nice"
    2.38 -
    2.39  if [ -n "$WRAPPER_SOCKET" ]; then
    2.40    MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
    2.41  elif [ -n "$WRAPPER_FIFOS" ]; then
    2.42 @@ -232,19 +225,14 @@
    2.43    if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
    2.44      MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
    2.45    fi
    2.46 -  if [ -n "$ISAR" ]; then
    2.47 -    MLTEXT="$MLTEXT; Isar.main ();"
    2.48 -  else
    2.49 -    NICE=""
    2.50 -  fi
    2.51  fi
    2.52  
    2.53  export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
    2.54  
    2.55  if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
    2.56 -  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
    2.57 +  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
    2.58  else
    2.59 -  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
    2.60 +  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
    2.61  fi
    2.62  RC="$?"
    2.63  
     3.1 --- a/src/Doc/System/Basics.thy	Fri Oct 31 15:15:10 2014 +0100
     3.2 +++ b/src/Doc/System/Basics.thy	Fri Oct 31 16:03:45 2014 +0100
     3.3 @@ -361,7 +361,6 @@
     3.4  Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
     3.5  
     3.6    Options are:
     3.7 -    -I           startup Isar interaction mode
     3.8      -O           system options from given YXML file
     3.9      -S           secure mode -- disallow critical operations
    3.10      -T ADDR      startup process wrapper, with socket address
    3.11 @@ -434,9 +433,6 @@
    3.12    system options as a file in YXML format (according to the Isabelle/Scala
    3.13    function @{verbatim isabelle.Options.encode}).
    3.14  
    3.15 -  \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
    3.16 -  interaction mode on startup, instead of the primitive ML top-level.
    3.17 -
    3.18    \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
    3.19    Isabelle enter a special process wrapper for interaction via
    3.20    Isabelle/Scala, see also @{file
     4.1 --- a/src/Pure/General/secure.ML	Fri Oct 31 15:15:10 2014 +0100
     4.2 +++ b/src/Pure/General/secure.ML	Fri Oct 31 16:03:45 2014 +0100
     4.3 @@ -13,7 +13,6 @@
     4.4    val use_text: use_context -> int * string -> bool -> string -> unit
     4.5    val use_file: use_context -> bool -> string -> unit
     4.6    val toplevel_pp: string list -> string -> unit
     4.7 -  val commit: unit -> unit
     4.8  end;
     4.9  
    4.10  structure Secure: SECURE =
    4.11 @@ -32,8 +31,6 @@
    4.12  
    4.13  (** critical operations **)
    4.14  
    4.15 -(* ML evaluation *)
    4.16 -
    4.17  fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
    4.18  
    4.19  val raw_use_text = use_text;
    4.20 @@ -45,12 +42,5 @@
    4.21  
    4.22  fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
    4.23  
    4.24 -
    4.25 -(* global evaluation *)
    4.26 -
    4.27 -val use_global = raw_use_text ML_Parse.global_context (0, "") false;
    4.28 -
    4.29 -fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
    4.30 -
    4.31  end;
    4.32  
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Oct 31 15:15:10 2014 +0100
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Oct 31 16:03:45 2014 +0100
     5.3 @@ -919,23 +919,14 @@
     5.4      (Scan.succeed (Toplevel.unknown_theory o
     5.5        Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
     5.6  
     5.7 -
     5.8 -
     5.9 -(** system commands (for interactive mode only) **)
    5.10 +val _ =
    5.11 +  Outer_Syntax.improper_command @{command_spec "print_state"}
    5.12 +    "print current proof state (if present)"
    5.13 +    (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
    5.14  
    5.15  val _ =
    5.16 -  Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
    5.17 -    (Parse.position Parse.name >>
    5.18 -      (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name)));
    5.19 -
    5.20 -val _ =
    5.21 -  Outer_Syntax.improper_command @{command_spec "remove_thy"} "remove theory from loader database"
    5.22 -    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
    5.23 -
    5.24 -val _ =
    5.25 -  Outer_Syntax.improper_command @{command_spec "kill_thy"}
    5.26 -    "kill theory -- try to remove from loader database"
    5.27 -    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
    5.28 +  Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
    5.29 +    (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
    5.30  
    5.31  val _ =
    5.32    Outer_Syntax.improper_command @{command_spec "display_drafts"}
    5.33 @@ -943,61 +934,6 @@
    5.34      (Scan.repeat1 Parse.path >> (fn names =>
    5.35        Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
    5.36  
    5.37 -val _ =
    5.38 -  Outer_Syntax.improper_command @{command_spec "print_state"}
    5.39 -    "print current proof state (if present)"
    5.40 -    (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
    5.41 -
    5.42 -val _ =
    5.43 -  Outer_Syntax.improper_command @{command_spec "commit"}
    5.44 -    "commit current session to ML session image"
    5.45 -    (Parse.opt_unit >> K (Toplevel.imperative Secure.commit));
    5.46 -
    5.47 -val _ =
    5.48 -  Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle process"
    5.49 -    (Parse.opt_unit >> (K (Toplevel.imperative quit)));
    5.50 -
    5.51 -val _ =
    5.52 -  Outer_Syntax.improper_command @{command_spec "exit"} "exit Isar loop"
    5.53 -    (Scan.succeed
    5.54 -      (Toplevel.keep (fn state =>
    5.55 -        (Context.set_thread_data (try Toplevel.generic_theory_of state);
    5.56 -          raise Runtime.TERMINATE))));
    5.57 -
    5.58 -val _ =
    5.59 -  Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
    5.60 -    (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
    5.61 -
    5.62 -
    5.63 -
    5.64 -(** raw Isar read-eval-print loop **)
    5.65 -
    5.66 -val _ =
    5.67 -  Outer_Syntax.improper_command @{command_spec "init_toplevel"} "init toplevel point-of-interest"
    5.68 -    (Scan.succeed (Toplevel.imperative Isar.init));
    5.69 -
    5.70 -val _ =
    5.71 -  Outer_Syntax.improper_command @{command_spec "linear_undo"} "undo commands"
    5.72 -    (Scan.optional Parse.nat 1 >>
    5.73 -      (fn n => Toplevel.imperative (fn () => Isar.linear_undo n)));
    5.74 -
    5.75 -val _ =
    5.76 -  Outer_Syntax.improper_command @{command_spec "undo"} "undo commands (skipping closed proofs)"
    5.77 -    (Scan.optional Parse.nat 1 >>
    5.78 -      (fn n => Toplevel.imperative (fn () => Isar.undo n)));
    5.79 -
    5.80 -val _ =
    5.81 -  Outer_Syntax.improper_command @{command_spec "undos_proof"}
    5.82 -    "undo commands (skipping closed proofs)"
    5.83 -    (Scan.optional Parse.nat 1 >> (fn n =>
    5.84 -      Toplevel.keep (fn state =>
    5.85 -        if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
    5.86 -
    5.87 -val _ =
    5.88 -  Outer_Syntax.improper_command @{command_spec "kill"}
    5.89 -    "kill partial proof or theory development"
    5.90 -    (Scan.succeed (Toplevel.imperative Isar.kill));
    5.91 -
    5.92  
    5.93  
    5.94  (** extraction of programs from proofs **)
     6.1 --- a/src/Pure/Pure.thy	Fri Oct 31 15:15:10 2014 +0100
     6.2 +++ b/src/Pure/Pure.thy	Fri Oct 31 16:03:45 2014 +0100
     6.3 @@ -88,11 +88,8 @@
     6.4      "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
     6.5      "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
     6.6      "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
     6.7 -  and "use_thy" "remove_thy" "kill_thy" :: control
     6.8    and "display_drafts" "print_state" :: diag
     6.9 -  and "commit" "quit" "exit" :: control
    6.10    and "welcome" :: diag
    6.11 -  and "init_toplevel" "linear_undo" "undo" "undos_proof" "kill" :: control
    6.12    and "end" :: thy_end % "theory"
    6.13    and "realizers" :: thy_decl == ""
    6.14    and "realizability" :: thy_decl == ""
     7.1 --- a/src/Pure/ROOT	Fri Oct 31 15:15:10 2014 +0100
     7.2 +++ b/src/Pure/ROOT	Fri Oct 31 16:03:45 2014 +0100
     7.3 @@ -196,7 +196,6 @@
     7.4      "System/invoke_scala.ML"
     7.5      "System/isabelle_process.ML"
     7.6      "System/isabelle_system.ML"
     7.7 -    "System/isar.ML"
     7.8      "System/message_channel.ML"
     7.9      "System/options.ML"
    7.10      "System/system_channel.ML"
     8.1 --- a/src/Pure/ROOT.ML	Fri Oct 31 15:15:10 2014 +0100
     8.2 +++ b/src/Pure/ROOT.ML	Fri Oct 31 16:03:45 2014 +0100
     8.3 @@ -327,7 +327,6 @@
     8.4  use "System/isabelle_process.ML";
     8.5  use "System/invoke_scala.ML";
     8.6  use "PIDE/protocol.ML";
     8.7 -use "System/isar.ML";
     8.8  
     8.9  
    8.10  (* miscellaneous tools and packages for Pure Isabelle *)
     9.1 --- a/src/Pure/System/isar.ML	Fri Oct 31 15:15:10 2014 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,174 +0,0 @@
     9.4 -(*  Title:      Pure/System/isar.ML
     9.5 -    Author:     Makarius
     9.6 -
     9.7 -Global state of the raw Isar read-eval-print loop.
     9.8 -*)
     9.9 -
    9.10 -signature ISAR =
    9.11 -sig
    9.12 -  val init: unit -> unit
    9.13 -  val exn: unit -> (exn * string) option
    9.14 -  val state: unit -> Toplevel.state
    9.15 -  val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
    9.16 -  val print: unit -> unit
    9.17 -  val >> : Toplevel.transition -> bool
    9.18 -  val >>> : Toplevel.transition list -> unit
    9.19 -  val linear_undo: int -> unit
    9.20 -  val undo: int -> unit
    9.21 -  val kill: unit -> unit
    9.22 -  val kill_proof: unit -> unit
    9.23 -  val crashes: exn list Synchronized.var
    9.24 -  val toplevel_loop: TextIO.instream ->
    9.25 -    {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
    9.26 -  val loop: unit -> unit
    9.27 -  val main: unit -> unit
    9.28 -end;
    9.29 -
    9.30 -structure Isar: ISAR =
    9.31 -struct
    9.32 -
    9.33 -
    9.34 -(** TTY model -- SINGLE-THREADED! **)
    9.35 -
    9.36 -(* the global state *)
    9.37 -
    9.38 -type history = (Toplevel.state * Toplevel.transition) list;
    9.39 -  (*previous state, state transition -- regular commands only*)
    9.40 -
    9.41 -local
    9.42 -  val global_history = Unsynchronized.ref ([]: history);
    9.43 -  val global_state = Unsynchronized.ref Toplevel.toplevel;
    9.44 -  val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
    9.45 -in
    9.46 -
    9.47 -fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
    9.48 -  let
    9.49 -    fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
    9.50 -      | edit n (st, hist) = edit (n - 1) (f st hist);
    9.51 -  in edit count (! global_state, ! global_history) end);
    9.52 -
    9.53 -fun state () = ! global_state;
    9.54 -
    9.55 -fun exn () = ! global_exn;
    9.56 -fun set_exn exn =  global_exn := exn;
    9.57 -
    9.58 -end;
    9.59 -
    9.60 -
    9.61 -fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
    9.62 -
    9.63 -fun goal () = Proof.goal (Toplevel.proof_of (state ()))
    9.64 -  handle Toplevel.UNDEF => error "No goal present";
    9.65 -
    9.66 -fun print () = Toplevel.print_state (state ());
    9.67 -
    9.68 -
    9.69 -(* history navigation *)
    9.70 -
    9.71 -local
    9.72 -
    9.73 -fun find_and_undo _ [] = error "Undo history exhausted"
    9.74 -  | find_and_undo which ((prev, tr) :: hist) =
    9.75 -      if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist;
    9.76 -
    9.77 -in
    9.78 -
    9.79 -fun linear_undo n = edit_history n (K (find_and_undo (K true)));
    9.80 -
    9.81 -fun undo n = edit_history n (fn st => fn hist =>
    9.82 -  find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);
    9.83 -
    9.84 -fun kill () = edit_history 1 (fn st => fn hist =>
    9.85 -  find_and_undo
    9.86 -    (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);
    9.87 -
    9.88 -fun kill_proof () = edit_history 1 (fn st => fn hist =>
    9.89 -  if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist
    9.90 -  else raise Toplevel.UNDEF);
    9.91 -
    9.92 -end;
    9.93 -
    9.94 -
    9.95 -(* interactive state transformations *)
    9.96 -
    9.97 -fun op >> tr =
    9.98 -  (case Toplevel.transition true tr (state ()) of
    9.99 -    NONE => false
   9.100 -  | SOME (_, SOME exn_info) =>
   9.101 -     (set_exn (SOME exn_info);
   9.102 -      Toplevel.setmp_thread_position tr
   9.103 -        Runtime.exn_error_message (Runtime.EXCURSION_FAIL exn_info);
   9.104 -      true)
   9.105 -  | SOME (st', NONE) =>
   9.106 -      let
   9.107 -        val name = Toplevel.name_of tr;
   9.108 -        val _ = if Keyword.is_theory_begin name then init () else ();
   9.109 -        val _ =
   9.110 -          if Keyword.is_regular name
   9.111 -          then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
   9.112 -      in true end);
   9.113 -
   9.114 -fun op >>> [] = ()
   9.115 -  | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
   9.116 -
   9.117 -
   9.118 -(* toplevel loop -- uninterruptible *)
   9.119 -
   9.120 -val crashes = Synchronized.var "Isar.crashes" ([]: exn list);
   9.121 -
   9.122 -local
   9.123 -
   9.124 -fun protocol_message props output =
   9.125 -  (case props of
   9.126 -    function :: args =>
   9.127 -      if function = Markup.command_timing then
   9.128 -        let
   9.129 -          val name = the_default "" (Properties.get args Markup.nameN);
   9.130 -          val pos = Position.of_properties args;
   9.131 -          val timing = Markup.parse_timing_properties args;
   9.132 -        in
   9.133 -          if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing)
   9.134 -            andalso name <> "" andalso not (Keyword.is_control name)
   9.135 -          then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing)
   9.136 -          else ()
   9.137 -        end
   9.138 -      else raise Output.Protocol_Message props
   9.139 -  | [] => raise Output.Protocol_Message props);
   9.140 -
   9.141 -fun raw_loop secure src =
   9.142 -  let
   9.143 -    fun check_secure () =
   9.144 -      (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
   9.145 -  in
   9.146 -    (case Source.get_single (Source.set_prompt Source.default_prompt src) of
   9.147 -      NONE => if secure then quit () else ()
   9.148 -    | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
   9.149 -    handle exn =>
   9.150 -      (Runtime.exn_error_message exn
   9.151 -        handle crash =>
   9.152 -          (Synchronized.change crashes (cons crash);
   9.153 -            warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
   9.154 -        raw_loop secure src)
   9.155 -  end;
   9.156 -
   9.157 -in
   9.158 -
   9.159 -fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
   9.160 - (Context.set_thread_data NONE;
   9.161 -  Multithreading.max_threads_update (Options.default_int "threads");
   9.162 -  if do_init then init () else ();
   9.163 -  Output.protocol_message_fn := protocol_message;
   9.164 -  if welcome then writeln (Session.welcome ()) else ();
   9.165 -  uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
   9.166 -
   9.167 -end;
   9.168 -
   9.169 -fun loop () =
   9.170 -  toplevel_loop TextIO.stdIn
   9.171 -    {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
   9.172 -
   9.173 -fun main () =
   9.174 -  toplevel_loop TextIO.stdIn
   9.175 -    {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
   9.176 -
   9.177 -end;